{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:37:10Z","timestamp":1761323830494,"version":"3.40.3"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2012,6,12]],"date-time":"2012-06-12T00:00:00Z","timestamp":1339459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,11]]},"DOI":"10.1007\/s10009-012-0237-y","type":"journal-article","created":{"date-parts":[[2012,7,9]],"date-time":"2012-07-09T01:33:51Z","timestamp":1341797631000},"page":"703-720","source":"Crossref","is-referenced-by-count":14,"title":["Compositional verification of real-time systems using Ecdar"],"prefix":"10.1007","volume":"14","author":[{"given":"Alexandre","family":"David","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim. G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mikael H.","family":"M\u00f8ller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ulrik","family":"Nyman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anders P.","family":"Ravn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arne","family":"Skou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"W\u0105sowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,6,12]]},"reference":[{"issue":"1","key":"237_CR1","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"Abadi M., Lamport L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73\u2013132 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"237_CR2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur R., Dill D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"237_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: CONCUR\u201998. LNCS, vol. 1466. Springer, Berlin (1998)","DOI":"10.1007\/BFb0055622"},{"key":"237_CR4","first-page":"24","volume-title":"CAV. Lecture Notes in Computer Science, vol. 575","author":"H.R. Andersen","year":"1991","unstructured":"Andersen H.R., Winskel G.: Compositional checking of satisfaction. In: Larsen, K.G., Skou, A. (eds.) CAV. Lecture Notes in Computer Science, vol. 575, pp. 24\u201336. Springer, Berlin (1991)"},{"issue":"2\u20133","key":"237_CR5","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/j.tcs.2004.07.036","volume":"335","author":"J.C.M. Baeten","year":"2005","unstructured":"Baeten J.C.M.: A brief history of process algebra. Theor. Comput. Sci. 335(2\u20133), 131\u2013146 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"237_CR6","unstructured":"Barnett, M., Rustan, K., Leino, M., Schulte, W.: The Spec# programming system: an overview. In: CASSIS 2004. LNCS, vol. 3362. Springer, Berlin (2004)"},{"key":"237_CR7","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: Uppaal-tiga: time for playing games! In: CAV. LNCS, vol. 4590. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"237_CR8","doi-asserted-by":"crossref","unstructured":"Bulychev, P., Chatain, T., David, A., Larsen, K.G.: Efficient on-the-fly algorithm for checking alternating timed simulation. In: FORMATS. LNCS, vol. 5813, pp. 73\u201387. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04368-0_8"},{"key":"237_CR9","doi-asserted-by":"crossref","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Legay, A.: Distributed parametric and statistical model checking. In: Barnat, J., Heljanko, K. (eds.) PDMC. EPTCS, vol. 72, pp. 30\u201342 (2011)","DOI":"10.4204\/EPTCS.72.4"},{"key":"237_CR10","doi-asserted-by":"crossref","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: CONCUR (2005)","DOI":"10.1007\/11539452_9"},{"key":"237_CR11","first-page":"80","volume-title":"FORMATS. Lecture Notes in Computer Science, vol. 6919","author":"A. David","year":"2011","unstructured":"David A., Larsen K.G., Legay A., Mikucionis M., Poulsen D.B., van Vliet J., Wang Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS. Lecture Notes in Computer Science, vol. 6919, pp. 80\u201396. Springer, Berlin (2011)"},{"key":"237_CR12","first-page":"349","volume-title":"CAV. Lecture Notes in Computer Science, vol. 6806","author":"A. David","year":"2011","unstructured":"David A., Larsen K.G., Legay A., Mikucionis M., Wang Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. Lecture Notes in Computer Science, vol. 6806, pp. 349\u2013355. Springer, Berlin (2011)"},{"key":"237_CR13","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1145\/1755952.1755967","volume-title":"HSCC","author":"A. David","year":"2010","unstructured":"David A., Larsen K.G., Legay A., Nyman U., Wasowski A.: Timed i\/o automata: a complete specification theory for real-time systems. In: Johansson, K.H., Yi, W. (eds.) HSCC, pp. 91\u2013100. ACM, New York (2010)"},{"key":"237_CR14","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: FSE, Vienna, Austria, September 2001. pp. 109\u2013120. ACM Press, New York","DOI":"10.1145\/503271.503226"},{"key":"237_CR15","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface-based design. In: In Engineering Theories of Software Intensive Systems, Marktoberdorf Summer School. Kluwer Academic Publishers, Dordrecht (2004)"},{"key":"237_CR16","first-page":"108","volume-title":"EMSOFT. LNCS, vol. 2491","author":"L. de Alfaro","year":"2002","unstructured":"de Alfaro L., Henzinger T.A., Stoelinga M.I.A.: Timed interfaces. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT. LNCS, vol. 2491, pp. 108\u2013122. Springer, Berlin (2002)"},{"key":"237_CR17","doi-asserted-by":"crossref","unstructured":"De Nicola, R., Segala, R.: A process algebraic view of input\/output automata. Theor. Comput. Sci. 138 (1995)","DOI":"10.1016\/0304-3975(95)92307-J"},{"key":"237_CR18","first-page":"490","volume-title":"MoDELS. Lecture Notes in Computer Science, vol. 6981","author":"U. Fahrenberg","year":"2011","unstructured":"Fahrenberg U., Legay A., Wasowski A.: Vision paper: make a difference! (semantically). In: Whittle, J., Clark, T., K\u00fchne, T. (eds.) MoDELS. Lecture Notes in Computer Science, vol. 6981, pp. 490\u2013500. Springer, Berlin (2011)"},{"key":"237_CR19","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"R.W. Floyd","year":"1967","unstructured":"Floyd R.W.: Assigning meanings to programs. Proceedings of the American Mathematical Society Symposia on Applied Mathematics 19, 19\u201331 (1967)","journal-title":"Proceedings of the American Mathematical Society Symposia on Applied Mathematics"},{"key":"237_CR20","unstructured":"Garland, S.J., Lynch, N.A.: The IOA language and toolset: support for designing, analyzing, and building distributed systems. Technical report, Massachusetts Institute of Technology, Cambridge (1998)"},{"issue":"10","key":"237_CR21","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"237_CR22","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/0020-0190(87)90106-2","volume":"24","author":"C.A.R. Hoare","year":"1987","unstructured":"Hoare C.A.R., He J.: The weakest prespecification. Inf. Process. Lett. 24, 127\u2013132 (1987)","journal-title":"Inf. Process. Lett."},{"key":"237_CR23","volume-title":"Communicating Sequential Processes. International Series in Computer Science","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice Hall, Upper Saddle River (1985)"},{"key":"237_CR24","first-page":"103","volume-title":"ECI. Lecture Notes in Computer Science, vol. 123","author":"C.B. Jones","year":"1981","unstructured":"Jones C.B.: Specification as a design base (extended abstract). In: Duijvestijn, A.J.W., Lockemann, P.C. (eds.) ECI. Lecture Notes in Computer Science, vol. 123, pp. 103\u2013105. Springer, Berlin (1981)"},{"key":"237_CR25","volume-title":"Systematic Software Development using VDM. Series in Computer Science","author":"C.B. Jones","year":"1986","unstructured":"Jones C.B.: Systematic Software Development using VDM. Series in Computer Science. Prentice-Hall, Upper Saddle River (1986)"},{"key":"237_CR26","doi-asserted-by":"crossref","unstructured":"Kaynar, D.K., Lynch, N.A., Segala, R., Vaandrager, F.W.: Timed i\/o automata: A mathematical framework for modeling and analyzing real-time systems. In: RTSS, pp. 166\u2013177. IEEE Computer Society, New York (2003)","DOI":"10.1109\/REAL.2003.1253264"},{"key":"237_CR27","unstructured":"Larsen, K.G.: Context-Dependent Bisimulation Between Processes. PhD thesis, Department of Computer Science, University of Edinburgh (1986)"},{"key":"237_CR28","first-page":"526","volume-title":"ICALP. Lecture Notes in Computer Science, vol. 443","author":"K.G. Larsen","year":"1990","unstructured":"Larsen K.G., Xinxin L.: Compositionality through an operational semantics of contexts. In: Paterson, M. (ed.) ICALP. Lecture Notes in Computer Science, vol. 443, pp. 526\u2013539. Springer, Berlin (1990)"},{"key":"237_CR29","doi-asserted-by":"crossref","first-page":"1087","DOI":"10.1007\/3-540-48118-4_8","volume-title":"FM\u201999\u2014Formal Methods: World Congress on Formal Methods in Development of Computer Systems. Lecture Notes in Computer Science, vol. 1709","author":"G.T. Leavens","year":"1999","unstructured":"Leavens G.T., Baker A.L.: Enhancing the pre- and postcondition technique for more expressive specifications. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM\u201999\u2014Formal Methods: World Congress on Formal Methods in Development of Computer Systems. Lecture Notes in Computer Science, vol. 1709, pp. 1087\u20131106. Springer, Berlin (1999)"},{"key":"237_CR30","doi-asserted-by":"crossref","unstructured":"Lynch, N.: I\/O automata: a model for discrete event systems. In: Annual Conference on Information Sciences and Systems, pp. 29\u201338. Princeton University, Princeton (1988)","DOI":"10.21236\/ADA196047"},{"key":"237_CR31","unstructured":"Lynch, N.A., Tuttle, M.R.: An introduction to input\/output automata. Technical Report MIT\/LCS\/TM-373. The MIT Press, Cambridge (1988)"},{"key":"237_CR32","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S.S. Owicki","year":"1976","unstructured":"Owicki S.S., Gries D.: An axiomatic proof technique for parallel programs i. Acta Inf. 6, 319\u2013340 (1976)","journal-title":"Acta Inf."},{"key":"237_CR33","doi-asserted-by":"crossref","unstructured":"Stark, E.W., Cleavland, R., Smolka, S.A.: A process-algebraic language for probabilistic I\/O automata. In: CONCUR. LNCS, pp. 189\u2013203. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45187-7_13"},{"key":"237_CR34","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S.: Model checking csp revisited: Introducing a process analysis toolkit. In: Proceedings of the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008). Communications in Computer and Information Science, vol. 17, pp. 307\u2013322. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-88479-8_22"},{"key":"237_CR35","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., Etienne, A.: Modeling and verifying hierarchical real-time systems using stateful timed csp. ACM Trans. Softw. Eng. Methodol. (2012, Accepted)","DOI":"10.1145\/2430536.2430537"},{"key":"237_CR36","volume-title":"Component Software, Beyond Object-Oriented Programming","author":"C. Szyperski","year":"1997","unstructured":"Szyperski C.: Component Software, Beyond Object-Oriented Programming. Addison-Wesley, Boston (1997)"},{"key":"237_CR37","doi-asserted-by":"crossref","unstructured":"Vaandrager, F.W.: On the relationship between process algebra and input\/output automata. In: LICS. pp. 387\u2013398 (1991)","DOI":"10.1109\/LICS.1991.151662"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0237-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0237-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0237-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T16:21:14Z","timestamp":1743697274000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0237-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,12]]},"references-count":37,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2012,11]]}},"alternative-id":["237"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0237-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2012,6,12]]}}}