{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:24:22Z","timestamp":1725791062961},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548611"},{"type":"electronic","value":"9783642548628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54862-8_18","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T09:33:34Z","timestamp":1395394414000},"page":"263-278","source":"Crossref","is-referenced-by-count":11,"title":["Compositional Invariant Generation for Timed Systems"],"prefix":"10.1007","author":[{"given":"Lacramioara","family":"A\u015ftef\u0103noaei","sequence":"first","affiliation":[]},{"given":"Souha","family":"Ben Rayana","sequence":"additional","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[]},{"given":"Jacques","family":"Combaz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Abdellatif, T., Combaz, J., Sifakis, J.: Model-based implementation of real-time applications. In: EMSOFT (2010)","DOI":"10.1145\/1879021.1879052"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45828-X_9","volume-title":"Embedded Software","author":"L. Alfaro de","year":"2002","unstructured":"de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Timed interfaces. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol.\u00a02491, pp. 108\u2013122. Springer, Heidelberg (2002)"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Astefanoaei, L., Rayana, S.B., Bensalem, S., Bozga, M., Combaz, J.: Compositional invariant generation for timed systems. Technical Report TR-2013-5, Verimag Research Report (2013)","DOI":"10.1007\/978-3-642-54862-8_18"},{"key":"18_CR5","unstructured":"Badban, B., Leue, S., Smaus, J.-G.: Automated invariant generation for the verification of real-time systems. In: WING@ETAPS\/IJCAR (2010)"},{"key":"18_CR6","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: SEFM (2006)"},{"key":"18_CR7","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST (2006)"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/BFb0055643","volume-title":"CONCUR \u201998 Concurrency Theory","author":"J. Bengtsson","year":"1998","unstructured":"Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 485\u2013500. Springer, Heidelberg (1998)"},{"key":"18_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.\u00a05311, pp. 64\u201379. Springer, Heidelberg (2008)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-85778-5_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J. Berendsen","year":"2008","unstructured":"Berendsen, J., Vaandrager, F.W.: Compositional abstraction in real-time model checking. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol.\u00a05215, pp. 233\u2013249. Springer, Heidelberg (2008)"},{"key":"18_CR11","unstructured":"Bornot, S., Sifakis, J.: An algebraic framework for urgency. Information and Computation (1998)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Bouyer, P.: Forward analysis of updatable timed automata. Form. Methods Syst. Des. (2004)","DOI":"10.1016\/S0304-3975(04)00265-8"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Computer Aided Verification","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: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 546\u2013550. Springer, Heidelberg (1998)"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. Formal Methods in System Design (1992)","DOI":"10.1007\/BF00709157"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., M\u00f8ller, M.H., Nyman, U., Ravn, A.P., Skou, A., Wasowski, A.: Compositional verification of real-time systems using Ecdar. STTT (2012)","DOI":"10.1007\/s10009-012-0237-y"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/BFb0058036","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"F.S. Boer de","year":"1997","unstructured":"de Boer, F.S., Hannemann, U., de Roever, W.-P.: Hoare-style compositional proof systems for reactive shared variable concurrency. In: Ramesh, S., Sivakumar, G. (eds.) FSTTCS 1997. LNCS, vol.\u00a01346, pp. 267\u2013283. Springer, Heidelberg (1997)"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Fietzke, A., Weidenbach, C.: Superposition as a decision procedure for timed automata. Mathematics in Computer Science (2012)","DOI":"10.1007\/s11786-012-0134-5"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/11513988_41","volume-title":"Computer Aided Verification","author":"G. Gardey","year":"2005","unstructured":"Gardey, G., Lime, D., Magnin, M., Roux, O(H.): Romeo: A tool for analyzing time petri nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 418\u2013423. Springer, Heidelberg (2005)"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. (1994)","DOI":"10.1006\/inco.1994.1045"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. (1987)","DOI":"10.1145\/7351.7352"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Legay, A., Bensalem, S., Boyer, B., Bozga, M.: Incremental generation of linear invariants for component-based systems. In: ACSD (2013)","DOI":"10.1109\/ACSD.2013.11"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-34281-3_17","volume-title":"Formal Methods and Software Engineering","author":"S.-W. Lin","year":"2012","unstructured":"Lin, S.-W., Liu, Y., Hsiung, P.-A., Sun, J., Dong, J.S.: Automatic generation of provably correct embedded systems. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol.\u00a07635, pp. 214\u2013229. Springer, Heidelberg (2012)"},{"key":"18_CR23","unstructured":"Salah, R.B., Bozga, M., Maler, O.: Compositional timing analysis. In: EMSOFT (2009)"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-48778-6_18","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"S. Tripakis","year":"1999","unstructured":"Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol.\u00a01601, pp. 299\u2013314. Springer, Heidelberg (1999)"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Wang, F.: Redlib for the formal verification of embedded systems. In: ISoLA (2006)","DOI":"10.1109\/ISoLA.2006.68"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54862-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T14:37:15Z","timestamp":1648651035000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54862-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548611","9783642548628"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54862-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}