{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:40:46Z","timestamp":1761324046454,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496732"},{"type":"electronic","value":"9783662496749"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_23","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"394-406","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["RTD-Finder: A Tool for Compositional Verification of Real-Time Component-Based Systems"],"prefix":"10.1007","author":[{"given":"Souha","family":"Ben-Rayana","sequence":"first","affiliation":[]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"Jacques","family":"Combaz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Abdellatif, T., Combaz, J., Sifakis, J.: Model-based implementation of real-time applications. In: Proceedings of the 10th International Conference on Embedded Software, EMSOFT, pp. 229\u2013238 (2010)","DOI":"10.1145\/1879021.1879052"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-24288-5_5","volume-title":"Reachability Problems","author":"\u00c9 Andr\u00e9","year":"2011","unstructured":"Andr\u00e9, \u00c9., Soulat, R.: Synthesis of timing parameters satisfying safety properties. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 31\u201344. Springer, Heidelberg (2011)"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/10722167_32","volume-title":"Computer Aided Verification","author":"A Annichini","year":"2000","unstructured":"Annichini, A., Asarin, E., Bouajjani, A.: Symbolic techniques for parametric reasoning about counter and clock systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 419\u2013434. Springer, Heidelberg (2000)"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-54862-8_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L A\u015ftef\u0103noaei","year":"2014","unstructured":"A\u015ftef\u0103noaei, L., Ben Rayana, S., Bensalem, S., Bozga, M., Combaz, J.: Compositional invariant generation for timed systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 263\u2013278. Springer, Heidelberg (2014)"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/978-3-319-17524-9_6","volume-title":"NASA Formal Methods","author":"L A\u015ftef\u0103noaei","year":"2015","unstructured":"A\u015ftef\u0103noaei, L., Ben Rayana, S., Bensalem, S., Bozga, M., Combaz, J.: Compositional verification of parameterised timed systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 66\u201381. Springer, Heidelberg (2015)"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Fourth IEEE International Conference on Software Engineering and Formal Methods, SEFM, pp. 3\u201312 (2006)","DOI":"10.1109\/SEFM.2006.27"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: Third International Conference on the Quantitative Evaluation of Systems, QEST, pp. 125\u2013126 (2006)","DOI":"10.1109\/QEST.2006.59"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1007\/978-3-642-02658-4_45","volume-title":"Computer Aided Verification","author":"S Bensalem","year":"2009","unstructured":"Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-Finder: a tool for compositional deadlock detection and verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 614\u2013619. Springer, Heidelberg (2009)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-88387-6_7","volume-title":"Automated Technology for Verification and Analysis","author":"S Bensalem","year":"2008","unstructured":"Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.-H.: Compositional verification for component-based systems and application. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 64\u201379. Springer, Heidelberg (2008)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Proceedings of Computer Aided Verification, CAV 1998","author":"M Bozga","year":"1998","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 546\u2013550. Springer, Heidelberg (1998)"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"International Workshop on Automatic Verification Methods for Finite State Systems","author":"DL Dill","year":"1989","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 197\u2013212. Springer, Heidelberg (1989)"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Heidelberg (2014)"},{"key":"23_CR13","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver. Technical report, SRI International (2006)"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-540-40903-8_5","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"H Hendriks","year":"2004","unstructured":"Hendriks, H., Behrmann, G., Larsen, K.G., Niebert, P., Vaandrager, F.W.: Adding symmetry reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 46\u201359. Springer, Heidelberg (2004)"},{"key":"23_CR15","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S1567-8326(02)00037-1","volume":"52\u201353","author":"T Hune","year":"2002","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52\u201353, 183\u2013220 (2002)","journal-title":"J. Log. Algebr. Program."},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-28756-5_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Z Jiang","year":"2012","unstructured":"Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification of a dual chamber implantable pacemaker. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 188\u2013203. Springer, Heidelberg (2012)"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-642-36742-7_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Jovanovi\u0107","year":"2013","unstructured":"Jovanovi\u0107, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 401\u2013415. Springer, Heidelberg (2013)"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/3-540-49213-5_14","volume-title":"Compositionality: The Significant Difference","author":"O Kupferman","year":"1998","unstructured":"Kupferman, O., Vardi, M.Y.: Modular model checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 381\u2013401. Springer, Heidelberg (1998)"},{"key":"23_CR19","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)"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/BFb0054178","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Lindahl","year":"1998","unstructured":"Lindahl, M., Pettersson, P., Yi, W.: Formal design and analysis of a gear controller. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 281\u2013297. Springer, Heidelberg (1998)"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Wang, F.: Redlib for the formal verification of embedded systems. In: Second International Symposium on Leveraging Applications of Formal Methods, ISoLA, pp. 341\u2013346 (2006)","DOI":"10.1109\/ISoLA.2006.68"},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-65193-4_20","volume-title":"Lectures on Embedded Systems, European Educational Forum, School on Embedded Systems","author":"S Yovine","year":"1996","unstructured":"Yovine, S.: Model checking timed automata. In: Rozenberg, G., Vaandrager, F.W. (eds.) Lectures on Embedded Systems. LNCS, vol. 1494, pp. 114\u2013152. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T08:27:18Z","timestamp":1748852838000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}