{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T04:16:14Z","timestamp":1746159374977,"version":"3.40.4"},"reference-count":65,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,2,20]],"date-time":"2014-02-20T00:00:00Z","timestamp":1392854400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2016,2]]},"DOI":"10.1007\/s10270-014-0399-z","type":"journal-article","created":{"date-parts":[[2014,2,19]],"date-time":"2014-02-19T08:11:35Z","timestamp":1392797495000},"page":"179-217","source":"Crossref","is-referenced-by-count":27,"title":["An executable formal semantics for UML-RT"],"prefix":"10.1007","volume":"15","author":[{"given":"Ernesto","family":"Posse","sequence":"first","affiliation":[]},{"given":"Juergen","family":"Dingel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,2,20]]},"reference":[{"key":"399_CR1","doi-asserted-by":"crossref","unstructured":"Benghazi Akhlaki, K., Capel Tu\u00f1\u00f3n, M.I., Holgado Terriza, J.A., Mendoza Morales, L.E.: A methodological approach to the formal specification of real-time systems by transformation of UML-RT design models. Sci. Comput. Program. 65, 41\u201356 (2007)","DOI":"10.1016\/j.scico.2006.08.005"},{"issue":"1\u20133","key":"399_CR2","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","volume":"60","author":"JA Bergstra","year":"1984","unstructured":"Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1\u20133), 109\u2013137 (1984)","journal-title":"Inf. Control"},{"key":"399_CR3","doi-asserted-by":"crossref","unstructured":"Bertolino, A., De Angelis, G., Bartolini, C., Lipari, G.: A UML Profile and a Methodology for Real-Time Systems Design. Technical Report, Istituto di Scienza e Tecnologie dell\u2019Informazione \u201cA. Faedo\u201d (2005)","DOI":"10.1109\/EUROMICRO.2006.14"},{"key":"399_CR4","doi-asserted-by":"crossref","unstructured":"de Melo Bezerra, J., Hirata, C.M.: A Semantics for UML-RT Using $$\\pi $$ \u03c0 -Calculus. In: Proceedings of International Workshop on Rapid System Prototyping (RSP\u201907) (2007)","DOI":"10.1109\/RSP.2007.9"},{"key":"399_CR5","doi-asserted-by":"crossref","unstructured":"de Melo Bezerra, J., Hirata, C.M.: A polyadic pi-calculus approach for the formal specification of UML-RT. Adv. Softw. Eng. 2009, (2009). doi: 10.1155\/2009\/656810","DOI":"10.1155\/2009\/656810"},{"key":"399_CR6","unstructured":"Boudol, G.: Asynchrony and the $$\\pi $$ \u03c0 -Calculus (Note). Technical Report 1702, INRIA-Sophia Antipolis (1992)"},{"key":"399_CR7","unstructured":"Capel, M.I., Mendoza, L.E., Akhlaki, K.B., Holgado, J.A.: A semantic formalization of UML-RT models with CSP+T processes applicable to real-time systems verification. In: Proceedings of Jornadas de Ingenier\u00eda del Software y Bases de Datos (JISBD\u201906), pp. 283\u2013292 (2006)"},{"issue":"3","key":"399_CR8","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/S0020-0190(02)00270-3","volume":"84","author":"SM Cho","year":"2002","unstructured":"Cho, S.M., Kim, H.-H., Cha, S.D., Bae, D.-H.: A semantics of sequence diagrams. Inf. Process. Lett. 84(3), 125\u2013130 (2002)","journal-title":"Inf. Process. Lett."},{"key":"399_CR9","doi-asserted-by":"crossref","unstructured":"Damm, W., Josko, B., Pnueli, A., Votintseva, A.: Understanding UML: a formal semantics of concurrency and communication in real-time UML. In: Proceedings of FMCO\u201902. LNCS, pp. 71\u201398. Springer, Berlin (2002)","DOI":"10.1007\/978-3-540-39656-7_3"},{"key":"399_CR10","doi-asserted-by":"crossref","unstructured":"Dingel, J., Paen, E., Posse, E., Rahman, R., Zurowska, K.: Definition and implementation of a semantic mapping for UML-RT using a timed pi-calculus. In: Proceedings of the Second International Workshop on Behaviour Modelling: Foundation and Applications, BM-FA \u201910, pp. 1:1\u20131:8. ACM, New York, NY (2010)","DOI":"10.1145\/1811147.1811148"},{"key":"399_CR11","doi-asserted-by":"crossref","unstructured":"Douglass, B.P.: Real-time UML. Formal Techniques in Real-Time and Fault-Tolerant Systems, Volume 2469 of LNCS, pp. 53\u201370. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45739-9_4"},{"key":"399_CR12","doi-asserted-by":"crossref","unstructured":"Engels, G., Heckel, R., K\u00fcster, J.M., Groenewegen, L.: Consistency-preserving model evolution through transformations. In: Proceedings of the Fifth International Conference on the Unified Modeling Language\u2014The Language and its Applications, pp. 212\u2013227. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45800-X_18"},{"key":"399_CR13","doi-asserted-by":"crossref","unstructured":"Eshuis, R., Wieringa, R.: A Formal Semantics for UML Activity Diagrams\u2014Formalising Workflow Models. Technical Report. University of Twente (2001)","DOI":"10.1007\/3-540-45314-8_7"},{"key":"399_CR14","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/j.entcs.2005.08.008","volume":"156","author":"H Fecher","year":"2006","unstructured":"Fecher, H., Kyas, M., De Roever, W.-P., De Boer, F.S.: Compositional operational semantics of a UML-Kernel-model language. Electron. Notes Theor. Comput. Sci. 156, 79\u201396 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"399_CR15","doi-asserted-by":"crossref","unstructured":"Ferreira, P., Sampaio, A., Mota, A.: Viewing CSP specifications with UML-RT diagrams. Electron. Notes Theor. Comput. Sci. 195(0), 57\u201374 (2008). Proceedings of the Brazilian Symposium on Formal Methods (SBMF 2006)","DOI":"10.1016\/j.entcs.2007.08.026"},{"key":"399_CR16","doi-asserted-by":"crossref","unstructured":"Fischer, C., Olderog, E.-R., Wehrheim, H.: A CSP view on UML-RT structure diagrams. In: Proceedings Fundamental Approaches to Software Engineering (FASE\u201901), Volume 2029 of LNCS, pp. 91\u2013108. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45314-8_8"},{"key":"399_CR17","unstructured":"Garlan, D., Monroe, R.T., Wile, D.: Acme: architectural description of component-based systems. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems, Chapter 3, pp. 47\u201367. Cambridge University Press, New York, NY (2000)"},{"key":"399_CR18","doi-asserted-by":"crossref","unstructured":"Grosu, R., Broy, M., Selic, B., Stefanescu, G.: Behavioral Specifications of Businesses and Systems, Chapter 6: What is Behind UML-RT?, pp. 73\u201388. Kluwer, Dordrecht (1999)","DOI":"10.1007\/978-1-4615-5229-1_6"},{"issue":"8","key":"399_CR19","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"399_CR20","doi-asserted-by":"crossref","unstructured":"Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: Proceedings of ECOOP \u201991, Volume 512 of LNCS, pp. 133\u2013147. Springer, Berlin (1991)","DOI":"10.1007\/BFb0057019"},{"key":"399_CR21","unstructured":"IBM: General Description Language. IBM, 9 March (2005)"},{"key":"399_CR22","unstructured":"IBM: IBM Rational Rose Technical Developer, Version 7.0. IBM, (2010) http:\/\/www-01.ibm.com\/software\/awdtools\/developer\/technical"},{"key":"399_CR23","unstructured":"IBM: IBM Rational Software Architect, RealTime Edition, Version 7.5.2. IBM (2010) http:\/\/publib.boulder.ibm.com\/infocenter\/rsarthlp\/v7r5m1\/index.jsp"},{"key":"399_CR24","unstructured":"IEEE Computer Society: IEEE Standard $$\\text{ Verilog }^{\\textregistered }$$ Verilog \u00ae Hardware Description Language, IEEE Standard $$1364^{{\\rm TM}}$$ 1364 TM -2001, 28 September (2001)"},{"key":"399_CR25","unstructured":"IEEE Computer Society: IEEE Standard VHDL Language Reference Manual, IEEE Standard $$1076^{{\\rm TM}}$$ 1076 TM -2008, 26 January (2009)"},{"key":"399_CR26","unstructured":"IEEE Computer Society: IEEE Standard for the SystemC Language, IEEE Standard $$1666^{\\rm TM}$$ 1666 TM -2011, January (2012)"},{"key":"399_CR27","unstructured":"IEEE Computer Society: IEEE Standard for SystemVerilog\u2014Unified Hardware Design, Specification, and Verification Language, IEEE Standard $$1800^{\\rm TM}$$ 1800 TM -2012, 21 February (2013)"},{"key":"399_CR28","unstructured":"International Telecommunications Union: Specification and description language (SDL). ITU-T Recommendation Z.100., November (1999)"},{"issue":"3","key":"399_CR29","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1145\/3916.3988","volume":"7","author":"DR Jefferson","year":"1985","unstructured":"Jefferson, D.R.: Virtual time. ACM-TOPLAS 7(3), 404\u2013425 (1985)","journal-title":"ACM-TOPLAS"},{"key":"399_CR30","doi-asserted-by":"crossref","unstructured":"Lano, K., Clark, D.: UML 2 Semantics and Applications. Chapter Ch. 8\u2014Axiomatic Semantics of State Machines, pp. 179\u2013204. Wiley, New York (2009)","DOI":"10.1002\/9780470522622"},{"key":"399_CR31","doi-asserted-by":"crossref","unstructured":"Leue, S., Stefanescu, A., Wei, W.: An AsmL semantics for dynamic structures and run time schedulability in UML-RT. In: Paige, R.F., Meyer, B. (eds.) Proceedings of Objects, Components, Models and Patterns (TOOLS EUROPE 2008), Volume 11 of Lecture Notes in Business Information Processing, pp. 238\u2013257. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-69824-1_14"},{"key":"399_CR32","doi-asserted-by":"crossref","unstructured":"Li, X., Liu, Z., Jifeng, H.: A formal semantics of UML sequence diagrams. In: Proceedings of the 2004 Australian Software Engineering Conference, pp. 168\u2013177 (2004)","DOI":"10.1109\/ASWEC.2004.1290469"},{"key":"399_CR33","doi-asserted-by":"crossref","unstructured":"Merseguer, J., Bernardi, S., Campos, J., Donatelli, S.: A compositional semantics for UML state machines aimed at performance evaluation. In: Proceedings of the 6th International Workshop on Discrete Event Systems, pp. 295\u2013302. IEEE Computer Society Press (2002)","DOI":"10.1109\/WODES.2002.1167702"},{"key":"399_CR34","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communicating Systems. Springer, Berlin (1980)"},{"key":"399_CR35","unstructured":"Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Parts I and II. Reports ECS-LFCS-89-85 and ECS-LFCS-89-86 86. Computer Science Dept., University of Edinburgh (1989)"},{"key":"399_CR36","doi-asserted-by":"crossref","unstructured":"M\u00f6ller, M.O., David, A., Yi, W.: Verification of UML statechart with real-time extensions. In: Fundamental Approaches to Software Engineering (FASE\u20192002), Volume 2306 of LNCS, pp. 218\u2013232. Springer, Berlin (2003)","DOI":"10.1007\/3-540-45923-5_15"},{"key":"399_CR37","doi-asserted-by":"crossref","unstructured":"Mrowka, R., Szmuc, T.: UML Statecharts Compositional Semantics in LOTOS. In: 2008 International Symposium on Parallel and Distributed Computing, pp. 459\u2013463. IEEE Computer Society Press (2008)","DOI":"10.1109\/ISPDC.2008.60"},{"key":"399_CR38","unstructured":"Muthiayen, D.: Real-Time Reactive System Development: A Formal Approach Based on UML and PVS. PhD thesis. Concordia University (2000)"},{"key":"399_CR39","doi-asserted-by":"crossref","unstructured":"Ng, M.Y., Butler, M.: Towards formalizing UML state diagrams in CSP. In: Proceedings of SEFM\u201903, pp. 138\u2013147. IEEE Computer Society (2003)","DOI":"10.1109\/SEFM.2003.1236215"},{"key":"399_CR40","unstructured":"Object Management Group: UML Profile For Schedulability, Performance, And Time v1.1. http:\/\/www.omg.org\/spec\/SPTP\/ , January (2005)"},{"key":"399_CR41","unstructured":"Object Management Group: UML Profile For MARTE: Modeling And Analysis Of Real-Time Embedded Systems v1.1. http:\/\/www.omg.org\/spec\/MARTE\/ , June (2011)"},{"key":"399_CR42","unstructured":"Object Management Group: UML Superstructure Specification v2.4.1. http:\/\/www.omg.org\/spec\/UML\/2.4.1\/ , August (2011)"},{"key":"399_CR43","unstructured":"Object Management Group: OMG Systems Modeling Language (OMG $$\\text{ SysML }^{\\rm TM}$$ SysML TM ). http:\/\/www.omg.org\/spec\/SysML\/1.3\/ June (2012)"},{"key":"399_CR44","unstructured":"Object Management Group: UML Superstructure Specification v2.5. http:\/\/www.omg.org\/spec\/UML\/2.5\/ September (2012)"},{"key":"399_CR45","unstructured":"Paltor, I.: The Semantics of UML State Machines. Technical report (1999)"},{"key":"399_CR46","unstructured":"Posse, E.: Modelling and Simulation of Dynamic Structure, Discrete-Event Systems. Ph.D. Thesis. School of Computer Science, McGill University (2008)"},{"key":"399_CR47","unstructured":"Posse, E.: A Real-Time Extension to the $$\\pi $$ \u03c0 -calculus. Technical Report 2009-557. School of Computing, Queen\u2019s University, http:\/\/www.cs.queensu.ca (2009)"},{"key":"399_CR48","unstructured":"Posse, E.: The $$\\pi _{klt}$$ \u03c0 k l t -Calculus: Formal Definition. Technical Report 2012-591, School of Computing, Queen\u2019s University, http:\/\/www.cs.queensu.ca , July (2012)"},{"key":"399_CR49","doi-asserted-by":"crossref","unstructured":"Posse, E., Dingel, J.: kiltera: a language for timed, event-driven, mobile and distributed simulation. In: Proceedings of the 14th IEEE\/ACM International Symposium on Distributed Simulation and Real Time Applications (DS-RT 2010) (2010)","DOI":"10.1109\/DS-RT.2010.19"},{"key":"399_CR50","doi-asserted-by":"crossref","unstructured":"Posse, E., Dingel, J.: Theory and implementation of a real-time extension to the $$\\pi $$ \u03c0 -calculus. In: Proceedings of the International Conference on Formal Techniques for Distributed Systems (FMOODS & FORTE\u201910), LNCS (2010)","DOI":"10.1007\/978-3-642-13464-7_11"},{"key":"399_CR51","doi-asserted-by":"crossref","unstructured":"Posse, E., Vangheluwe, H.: kiltera: a simulation language for timed, dynamic structure systems. In: Proceedings of the 40th Annual Simulation Symposium (ANSS\u201907) (2007)","DOI":"10.1109\/ANSS.2007.25"},{"key":"399_CR52","doi-asserted-by":"crossref","unstructured":"Ramos, R., Sampaio, A., Mota, A.: A semantics for UML-RT active classes via mapping into Circus. In: Proceedings of the International Conference on Formal Methods for Open Object-Based Distributed Systems FMOODS\u201905, Volume 3535 of LNCS, pp. 99\u2013114. Springer, Berlin (2005)","DOI":"10.1007\/11494881_7"},{"key":"399_CR53","unstructured":"SAE International: Architecture Analysis & Design Language (AADL). SAE Standard AS5506b, 10 September (2012)"},{"key":"399_CR54","doi-asserted-by":"crossref","unstructured":"Selic, B.: Using UML for modeling complex real-time systems. In: Mueller, F., Bestavros, A. (eds.) Languages, Compilers, and Tools for Embedded Systems (LCTES\u201998), Volume 1474 of LNCS, pp. 250\u2013260. Springer, Berlin (1998)","DOI":"10.1007\/BFb0057795"},{"key":"399_CR55","unstructured":"Selic, B.: Personal Communication, 1 February (2012)"},{"key":"399_CR56","volume-title":"Real-Time Object Oriented Modeling","author":"B Selic","year":"1994","unstructured":"Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object Oriented Modeling. Wiley, New York (1994)"},{"key":"399_CR57","doi-asserted-by":"crossref","unstructured":"Selic, B., Rumbaugh, J.: Using UML for Modeling Complex Real-Time Systems. Whitepaper, Rational Software Corp (1998)","DOI":"10.1007\/BFb0057795"},{"key":"399_CR58","doi-asserted-by":"crossref","unstructured":"Shankar, S., Asa, S.: Formal semantics of UML with real-time constructs. In: UML, Volume 2863 of LNCS, pp. 60\u201375. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45221-8_6"},{"key":"399_CR59","unstructured":"St\u00f6rrle, H., Hausmann, J.H.: Towards a formal semantics of UML 2.0 activities. In: Proceedings German Software Engineering Conference, Volume 65 of LNI, pp. 117\u2013128 (2005)"},{"issue":"2","key":"399_CR60","first-page":"130","volume":"1","author":"M Beeck von der","year":"2002","unstructured":"von der Beeck, M.: A structured operational semantics for UML-statecharts. SoSyM 1(2), 130\u2013141 (2002)","journal-title":"SoSyM"},{"key":"399_CR61","doi-asserted-by":"crossref","unstructured":"von der Beeck, M.: A formal semantics of UML-RT. In: Proceedings of MoDELS\u201906, pp. 768\u2013782 (2006)","DOI":"10.1007\/11880240_53"},{"key":"399_CR62","doi-asserted-by":"crossref","unstructured":"Yeung, W.L., Leung, K.R.P.H., Wang, J., Dong, W.: Improvements towards formalizing UML state diagrams in CSP. In: Proceedings of APSEC-\u201905, pp. 176\u2013184. IEEE Computer Society (2005)","DOI":"10.1109\/APSEC.2005.70"},{"key":"399_CR63","volume-title":"Theory of Modeling and Simulation","author":"BP Zeigler","year":"1976","unstructured":"Zeigler, B.P., Praehofer, H., Kim, T.G.: Theory of Modeling and Simulation, 1st edn. Academic Press, New York (1976)","edition":"1"},{"key":"399_CR64","volume-title":"Theory of Modeling and Simulation","author":"BP Zeigler","year":"2000","unstructured":"Zeigler, B.P., Praehofer, H., Kim, T.G.: Theory of Modeling and Simulation, 2nd edn. Academic Press, New York (2000)","edition":"2"},{"key":"399_CR65","doi-asserted-by":"crossref","unstructured":"Zhang, T., Huang, S., Huang, H.: An operational semantics for UML RT-statechart in model checking context. In: Proceedings of the 4th International Conference on Internet Computing for Science and Engineering (ICICSE), pp. 12\u201318 (2009)","DOI":"10.1109\/ICICSE.2009.15"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-014-0399-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-014-0399-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-014-0399-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T21:53:07Z","timestamp":1746136387000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-014-0399-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2,20]]},"references-count":65,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,2]]}},"alternative-id":["399"],"URL":"https:\/\/doi.org\/10.1007\/s10270-014-0399-z","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2014,2,20]]}}}