{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T11:44:47Z","timestamp":1790509487977,"version":"4.1.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319539454","type":"print"},{"value":"9783319539461","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-53946-1_8","type":"book-chapter","created":{"date-parts":[[2017,2,15]],"date-time":"2017-02-15T12:42:51Z","timestamp":1487162571000},"page":"129-144","source":"Crossref","is-referenced-by-count":5,"title":["Applying Parametric Model-Checking Techniques for Reusing Real-Time Critical Systems"],"prefix":"10.1007","author":[{"given":"Baptiste","family":"Parquier","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laurent","family":"Rioux","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rafik","family":"Henia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Romain","family":"Soulat","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Olivier H.","family":"Roux","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Didier","family":"Lime","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,2,16]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-49382-2_22","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"L Aceto","year":"1998","unstructured":"Aceto, L., Bouyer, P., Burgue\u00f1o, A., Larsen, K.G.: The power of reachability testing for timed automata. In: Arvind, V., Ramanujam, S. (eds.) FSTTCS 1998. LNCS, vol. 1530, pp. 245\u2013256. Springer, Heidelberg (1998). doi: 10.1007\/978-3-540-49382-2_22"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/BFb0054177","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Aceto","year":"1998","unstructured":"Aceto, L., Burgue\u00f1o, A., Larsen, K.G.: Model checking via reachability testing for timed automata. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 263\u2013280. Springer, Heidelberg (1998). doi: 10.1007\/BFb0054177"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592\u2013601. ACM (1993)","DOI":"10.1145\/167088.167242"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, \u00c9.: Observer patterns for real-time systems. In: ICECCS, pp. 125\u2013134. IEEE Computer Society (2013)","DOI":"10.1109\/ICECCS.2013.26"},{"key":"8_CR5","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-319-29510-7_3","volume-title":"Formal Techniques for Safety-Critical Systems","author":"\u00c9 Andr\u00e9","year":"2016","unstructured":"Andr\u00e9, \u00c9.: What\u2019s decidable about parametric timed automata? In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 52\u201368. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-29510-7_3"},{"issue":"5","key":"8_CR6","doi-asserted-by":"crossref","first-page":"819","DOI":"10.1142\/S0129054109006905","volume":"20","author":"\u00c9 Andr\u00e9","year":"2009","unstructured":"Andr\u00e9, \u00c9., Chatain, T., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. Int. J. Found. Comput. Sci. 20(5), 819\u2013836 (2009)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-32759-9_6","volume-title":"FM 2012: Formal Methods","author":"\u00c9 Andr\u00e9","year":"2012","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., K\u00fchne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33\u201336. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-32759-9_6"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-319-24537-9_2","volume-title":"Reachability Problems","author":"\u00c9 Andr\u00e9","year":"2015","unstructured":"Andr\u00e9, \u00c9., Lime, D., Roux, O.H.: Integer-complete synthesis for bounded parametric timed automata. In: Boja\u0144czyk, M., Lasota, S., Potapov, I. (eds.) RP 2015. LNCS, vol. 9328, pp. 7\u201319. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-24537-9_2"},{"issue":"1\u20132","key":"8_CR9","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"key":"8_CR10","unstructured":"Bini, E.: The design domain of real-time systems. PhD thesis, Scuola Superiore Sant\u2019Anna (2004)"},{"issue":"6","key":"8_CR11","doi-asserted-by":"crossref","first-page":"1509","DOI":"10.1093\/logcom\/exp036","volume":"19","author":"H Boucheneb","year":"2009","unstructured":"Boucheneb, H., Gardey, G., Roux, O.H.: TCTL model checking of time Petri nets. J. Logic Comput. 19(6), 1509\u20131540 (2009)","journal-title":"J. Logic Comput."},{"issue":"5","key":"8_CR12","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1016\/j.ipl.2006.11.018","volume":"102","author":"L Doyen","year":"2007","unstructured":"Doyen, L.: Robust parametric reachability for timed automata. Inf. Process. Lett. 102(5), 208\u2013213 (2007)","journal-title":"Inf. Process. Lett."},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Gonz\u00e1lez Harbour, M., Guti\u00e9rrez Garc\u00eda, J.J., Palencia Guti\u00e9rrez, J.C., Drake Moyano, J.M.: MAST: modeling and analysis suite for real time applications. In: ECRTS, pp. 125\u2013134. IEEE Computer Society (2001)","DOI":"10.1109\/EMRTS.2001.934015"},{"issue":"2","key":"8_CR14","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1049\/ip-cdt:20045088","volume":"152","author":"R Henia","year":"2005","unstructured":"Henia, R., Hamann, A., Jersak, M., Racu, R., Richter, K., Ernst, R.: System level performance analysis - the SymTA\/S approach. IEE Proc. Comput. Digital Tech. 152(2), 148\u2013166 (2005)","journal-title":"IEE Proc. Comput. Digital Tech."},{"issue":"5","key":"8_CR15","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1109\/TSE.2014.2357445","volume":"41","author":"A Jovanovi\u0107","year":"2015","unstructured":"Jovanovi\u0107, A., Lime, D., Roux, O.H.: Integer parameter synthesis for real-time systems. IEEE Trans. Softw. Eng. 41(5), 445\u2013461 (2015)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"8_CR16","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/s10009-012-0245-y","volume":"15","author":"TTH Le","year":"2013","unstructured":"Le, T.T.H., Palopoli, L., Passerone, R., Ramadian, Y.: Timed-automata based schedulability analysis for distributed firm real-time systems: a case study. Int. J. Softw. Tools Technol. Transf. 15(3), 211\u2013228 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-00768-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Lime","year":"2009","unstructured":"Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54\u201357. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-00768-2_6"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-46430-1_26","volume-title":"Hybrid Systems: Computation and Control","author":"JS Miller","year":"2000","unstructured":"Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 296\u2013310. Springer, Heidelberg (2000). doi: 10.1007\/3-540-46430-1_26"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Palencia Guti\u00e9rrez, J.C., Gonz\u00e1lez Harbour, M.: Schedulability analysis for tasks with static and dynamic offsets. In: IEEE Real-Time Systems Symposium, pp. 26\u201337. IEEE Computer Society (1998)","DOI":"10.1109\/REAL.1998.739728"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Richter, K., Ernst, R.: Event model interfaces for heterogeneous system analysis. In: DATE, pp. 506\u2013513. IEEE Computer Society (2002)","DOI":"10.1109\/DATE.2002.998348"},{"key":"8_CR21","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-319-05416-2_14","volume-title":"Formal Techniques for Safety-Critical Systems","author":"Y Sun","year":"2014","unstructured":"Sun, Y., Soulat, R., Lipari, G., Andr\u00e9, \u00c9., Fribourg, L.: Parametric schedulability analysis of fixed priority real-time distributed systems. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2013. CCIS, vol. 419, pp. 212\u2013228. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-05416-2_14"},{"issue":"17","key":"8_CR22","first-page":"3273","volume":"15","author":"L-M Traonouez","year":"2009","unstructured":"Traonouez, L.-M., Lime, D., Roux, O.H.: Parametric model-checking of stopwatch Petri nets. J. Univ. Comput. Sci. 15(17), 3273\u20133304 (2009)","journal-title":"J. Univ. Comput. Sci."},{"issue":"6","key":"8_CR23","doi-asserted-by":"crossref","first-page":"649","DOI":"10.1007\/s10009-006-0019-5","volume":"8","author":"E Wandeler","year":"2006","unstructured":"Wandeler, E., Thiele, L., Verhoef, M., Lieverse, P.: System architecture evaluation using modular performance analysis: a case study. Int. J. Softw. Tools Technol. Transf. 8(6), 649\u2013667 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-53946-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T11:20:36Z","timestamp":1749986436000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-53946-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319539454","9783319539461"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-53946-1_8","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"value":"1865-0929","type":"print"},{"value":"1865-0937","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}