{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:20:26Z","timestamp":1762521626218},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,8,6]],"date-time":"2013-08-06T00:00:00Z","timestamp":1375747200000},"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":[[2015,2]]},"DOI":"10.1007\/s10009-013-0286-x","type":"journal-article","created":{"date-parts":[[2013,8,5]],"date-time":"2013-08-05T16:47:50Z","timestamp":1375721270000},"page":"17-45","source":"Crossref","is-referenced-by-count":15,"title":["Real-time specifications"],"prefix":"10.1007","volume":"17","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":"Ulrik","family":"Nyman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Louis-Marie","family":"Traonouez","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":[[2013,8,6]]},"reference":[{"key":"286_CR1","doi-asserted-by":"crossref","unstructured":"Abdellatif, T., Combaz, J., Sifakis, J.: Model-based implementation of real-time applications. In: EMSOFT, pp. 229\u2013238. ACM, New York (2010)","DOI":"10.1145\/1879021.1879052"},{"key":"286_CR2","doi-asserted-by":"crossref","unstructured":"Adler, B.T, de Alfaro, L., Dias, L., de Silva, F.M., Legay, A., Raman, V., Ticc, P.R.: A tool for interface compatibility and composition. In: CAV, vol. 4144 of LNCS, pp. 59\u201362. Springer, Berlin (2006)","DOI":"10.1007\/11817963_8"},{"issue":"2","key":"286_CR3","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":"286_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: CONCUR, vol. 1466 of LNCS. Springer, Berlin (1998)","DOI":"10.1007\/BFb0055622"},{"key":"286_CR5","doi-asserted-by":"crossref","unstructured":"Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Times, W.Y.: A tool for schedulability analysis and code generation of real-time systems. In: FORMATS, vol. 2791 of LNCS, pp. 60\u201372. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-40903-8_6"},{"issue":"1","key":"286_CR6","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1017\/S0960129509990260","volume":"20","author":"A Antonik","year":"2010","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowsk, A.: Modal and mixed specifications: key decision problems and their complexities. Math Struct Comput Sci 20(1), 75\u2013103 (2010)","journal-title":"Math Struct Comput Sci"},{"key":"286_CR7","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"issue":"4","key":"286_CR8","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1017\/S0960129511000697","volume":"22","author":"SS Bauer","year":"2012","unstructured":"Bauer, S.S., Juhl, L., Larsen, K.G., Legay, A., Srba, J.: Extending modal transition systems with structured labels. Math Struct Comput Sci 22(4), 581\u2013617 (2012)","journal-title":"Math Struct Comput Sci"},{"key":"286_CR9","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, vol. 4590 of LNCS. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"286_CR10","unstructured":"Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing uppaal over 15 years. Softw. Pract. Exper. 41(2), 133\u2013142 (2011)"},{"key":"286_CR11","unstructured":"Berendsen, J., Vaandrager, F.W.: Compositional abstraction in real-time model checking. In: FORMATS, vol. 5215 of LNCS. Springer, Berlin (2008)"},{"key":"286_CR12","doi-asserted-by":"crossref","unstructured":"Bertrand, N., Legay, A., Pinchinat, S., Raclet, J.-B.: A compositional approach on modal specifications for timed systems. In ICFEM, LNCS. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-10373-5_35"},{"key":"286_CR13","doi-asserted-by":"crossref","unstructured":"Bourke, T., Sowmya, A.: Automatically transforming and relating uppaal models of embedded systems. In EMSOFT, pp. 59\u201368. ACM, New York (2008)","DOI":"10.1145\/1450058.1450068"},{"key":"286_CR14","doi-asserted-by":"crossref","unstructured":"Bourke, T., David, A., Larsen, K.G., Legay, A., Lime, D., Nyman, U., Wasowski, A.: New results on timed specifications. In: WADT, vol. 7137 of LNCS, pp. 175\u2013192. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-28412-0_12"},{"key":"286_CR15","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, vol. 5813 of LNCS, pp. 73\u201387. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04368-0_8"},{"key":"286_CR16","doi-asserted-by":"crossref","unstructured":"Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., W\u0105sowski, A.: Compositional design methodology with constraint Markov chains. In: QEST, pp. 123\u2013132. IEEE Press, USA (2010)","DOI":"10.1109\/QEST.2010.23"},{"key":"286_CR17","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":"286_CR18","doi-asserted-by":"crossref","unstructured":"Cassez, F., David, A., Larsen, K.G., Lime, D., Raskin, J.-F.: Timed control with observation based and stuttering invariant strategies. In: ATVA, vol. 4762 of LNCS, pp. 192\u2013206. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-75596-8_15"},{"key":"286_CR19","doi-asserted-by":"crossref","unstructured":"Cerans, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification\u2014theory and tools. In: CAV, pp. 253\u2013267. Springer, Berlin (1993)","DOI":"10.1007\/3-540-56922-7_21"},{"key":"286_CR20","doi-asserted-by":"crossref","unstructured":"Chakabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.I.A.: Resource interfaces. In: Alur. R., Lee, I., (eds) EMSOFT 03: 3rd International Workshop on Embedded Software, LNCS. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45212-6_9"},{"key":"286_CR21","doi-asserted-by":"crossref","unstructured":"Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Mang, F.Y.C.: Synchronous and bidirectional component interfaces. In: CAV, vol. 2404 of LNCS, pp. 414\u2013427 (2002)","DOI":"10.1007\/3-540-45657-0_34"},{"key":"286_CR22","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Orna, G.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"286_CR23","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Methodologies for specification of real-time systems using timed i\/o automata. In: FMCO, vol. 6286 of LNCS, pp. 290\u2013310. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-17071-3_15"},{"key":"286_CR24","doi-asserted-by":"crossref","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: HSCC, pp. 91\u2013100. ACM, USA (2010)","DOI":"10.1145\/1755952.1755967"},{"key":"286_CR25","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 14(6), 703\u2013720 (2012)","DOI":"10.1007\/s10009-012-0237-y"},{"key":"286_CR26","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Ecdar: An environment for compositional design and analysis of real time systems. In: ATVA, vol. 6252 of LNCS, pp. 365\u2013370. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-15643-4_29"},{"key":"286_CR27","doi-asserted-by":"crossref","unstructured":"de Alfaro, L.: Game models for open systems. In: Proceedings of the International Symposium on Verification (Theory in Practice), vol. 2772 of LNCS. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-39910-0_12"},{"key":"286_CR28","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Roy, P., Sorea, Ma.: Sociable interfaces. In: FroCos, vol. 3717 of LNCS, pp. 81\u2013105. Springer, Berlin (2005)","DOI":"10.1007\/11559306_5"},{"key":"286_CR29","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Faella, M.: An accelerated algorithm for 3-color parity games with an application to timed games. In: CAV, vol. 4590 of LNCS. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_13"},{"key":"286_CR30","doi-asserted-by":"crossref","unstructured":"de Alfaro, L, Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: CONCUR, vol. 2761 of LNCS, pp. 142\u2013156. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45187-7_9"},{"key":"286_CR31","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: FSE, pp. 109\u2013120, Austria, September 2001. ACM Press, New York (2001)","DOI":"10.1145\/503271.503226"},{"key":"286_CR32","unstructured":"de Alfaro, L., Henzinger, T.A.: Interfacebased design. In: In Engineering Theories of Software Intensive Systems, Marktoberdorf Summer School. Kluwer Academic Publishers, Dordrecht (2004)"},{"key":"286_CR33","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A., Majumdar, R.: Symbolic algorithms for infinite-state games. In: CONCUR, vol 2154 of LNCS, pp. 536\u2013550. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44685-0_36"},{"key":"286_CR34","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A., Stoelinga, M.I.A.: Timed interfaces. In: EMSOFT, vol. 2491 of LNCS, pp. 108\u2013122. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45828-X_9"},{"key":"286_CR35","doi-asserted-by":"crossref","unstructured":"Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wasowski, A.: Abstract probabilistic automata. In: VMCAI, pp. 324\u2013339. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-18275-4_23"},{"key":"286_CR36","unstructured":"Fiadeiro, J., Andrade, L.F.: Interconnecting objects via contracts. In: Proceedings of the 38th International Conference on Technology of Object-Oriented Languages and Systems, Components for Mobile Computing (TOOLS\u201938), pp. 182\u2013183. IEEE Computer Society, USA (2001)"},{"key":"286_CR37","doi-asserted-by":"crossref","unstructured":"Fiadeiro, J.L., Maibaum, T.S.E.: Interconnecting formalisms: Supporting modularity, reuse and incrementality. In: Proceedings of the 3rd ACM SIGSOFT Symposium on Foundations of Software Engineering (SIGSOFT FSE\u201995), pp. 72\u201380. ACM, New York (1995)","DOI":"10.1145\/222124.222141"},{"key":"286_CR38","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)"},{"key":"286_CR39","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: Timed transition systems. In: REX Workshop, vol. 600 of LNCS, pp. 226\u2013251. Springer, Berlin (1991)","DOI":"10.1007\/BFb0031995"},{"key":"286_CR40","unstructured":"Henzinger, T.A., Matic, S.: An interface algebra for real-time components. In: IEEE Real Time Technology and Applications Symposium, pp. 253\u2013266. IEEE Computer Society, USA (2006)"},{"key":"286_CR41","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: FM, vol. 4085 of LNCS, pp. 1\u201315. Springer, Berlin (2006)","DOI":"10.1007\/11813040_1"},{"key":"286_CR42","doi-asserted-by":"crossref","unstructured":"Kaynar, D.K., Lynch, N.A., Segala, R., Vaandrager, F.W.: The Theory of Timed I\/O Automata, 2nd edn. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2010)","DOI":"10.2200\/S00310ED1V01Y201011DCT005"},{"key":"286_CR43","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. In: FORMATS, vol. 3253 of LNCS, pp. 293\u2013308. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30206-3_21"},{"issue":"7","key":"286_CR44","doi-asserted-by":"crossref","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"MZ Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027\u20131077 (2007)","journal-title":"Inf. Comput."},{"key":"286_CR45","doi-asserted-by":"crossref","unstructured":"Larsen, K.G.: Modal specifications. In: Sifakis, J., (ed) Automatic Verification Methods for Finite State Systems, vol. 407 of LNCS, pp. 232\u2013246. Springer, Berlin (1989)","DOI":"10.1007\/3-540-52148-8_19"},{"key":"286_CR46","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Legay, A., Traonouez, L.-M., Wasowski, A.: Robust specification of real time components. In: FORMATS 2011, vol. 6919 of LNCS. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24310-3_10"},{"key":"286_CR47","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Nyman, U., Wasowski, A.: Modal I\/O automata for interface and product line theories. In: De Nicola, R., (ed) ESOP, vol. 4421 of LNCS, pp. 64\u201379. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-71316-6_6"},{"key":"286_CR48","doi-asserted-by":"crossref","unstructured":"Larsen, Kim G., Pettersson, Paul, Yi, Wang: Model-Checking for Real-Time Systems. In Proc. of Fundamentals of Computation Theory, volume 965 of LNCS, pages 62\u201388, August (1995)","DOI":"10.1007\/3-540-60249-6_41"},{"key":"286_CR49","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":"286_CR50","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":"286_CR51","doi-asserted-by":"crossref","unstructured":"Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (an extended abstract). In: STACS, pp. 229\u2013242 (1995)","DOI":"10.1007\/3-540-59042-0_76"},{"key":"286_CR52","volume-title":"Communication and Concurrency","author":"M Robin","year":"1988","unstructured":"Robin, M.: Communication and Concurrency. Prentice Hall, New York (1988)"},{"key":"286_CR53","unstructured":"De Nicola, R., Segala, R.: A process algebraic view of input\/output automata. Theor. Comput. Sci. 138(2), 391\u2013423 (1995)"},{"key":"286_CR54","doi-asserted-by":"crossref","unstructured":"Post, A., Hoenicke, J., Podelski, A.: rt-inconsistency: a new property for real-time requirements. In: FASE, vol. 6603 of LNCS, pp. 34\u201349. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-19811-3_4"},{"key":"286_CR55","unstructured":"Raclet, J.-B., Caillaud, B., Nickovic, D., Passerone, R., Sangiovanni-Vincentelli, A., Henzinger, T., Larsen, K.G.: Contracts for the design of embedded systems part i: Methodology and use cases. Technical report. Submitted, http:\/\/www.irisa.fr\/distribcom\/benveniste\/pub\/ProcIEEE_contractsPart1.pdf"},{"key":"286_CR56","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\u20132003. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45187-7_13"},{"key":"286_CR57","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S.: Model checking csp revisited: Introducing a process analysis toolkit. In: ISoLA, vol. 17 of Communications in Computer and Information Science, pp. 307\u2013322. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-88479-8_22"},{"key":"286_CR58","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., \u00c9tienne, A.: Modeling and verifying hierarchical real-time systems using stateful timed csp. ACM Trans. Softw. Eng. Methodol. 22(1), 3.1\u20133.29 (2013)","DOI":"10.1145\/2430536.2430537"},{"key":"286_CR59","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5, 285\u2013309 (1955)","journal-title":"Pac. J. Math."},{"key":"286_CR60","doi-asserted-by":"crossref","unstructured":"Traonouez, L.-M.: A parametric counterexample refinement approach for robust timed specifications. In: FIT, vol. 87 of EPTCS, pp. 17\u201333 (2012)","DOI":"10.4204\/EPTCS.87.3"},{"key":"286_CR61","unstructured":"Vaandrager, F.W.: On the relationship between process algebra and input\/output automata. In: LICS, pp. 387\u2013398 (1991)"},{"key":"286_CR62","unstructured":"Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robust safety of timed automata. Formal Methods Syst. Design 33, 45\u201384 (2008)"},{"key":"286_CR63","unstructured":"Yi, W.: Real-time behaviour of asynchronous agents. In: Baeten, J.C.M., Klop, J.W., (eds) CONCUR, vol. 458 of LNCS, pp. 502\u2013520. Springer, Berlin (1990)"}],"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-013-0286-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0286-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0286-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,3]],"date-time":"2022-03-03T00:03:19Z","timestamp":1646265799000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0286-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,8,6]]},"references-count":63,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["286"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0286-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,8,6]]}}}