{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T14:25:16Z","timestamp":1774103116418,"version":"3.50.1"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030674441","type":"print"},{"value":"9783030674458","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","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":[[2021]]},"DOI":"10.1007\/978-3-030-67445-8_10","type":"book-chapter","created":{"date-parts":[[2021,2,1]],"date-time":"2021-02-01T04:28:24Z","timestamp":1612153704000},"page":"225-249","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Verification and Simulation of Time-Domain Properties for Models of Behaviour"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2105-3075","authenticated-orcid":false,"given":"Miguel","family":"Carrillo","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7775-0780","authenticated-orcid":false,"given":"Vladimir","family":"Estivill-Castro","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8933-8267","authenticated-orcid":false,"given":"David A.","family":"Rosenblueth","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,2,2]]},"reference":[{"key":"10_CR1","unstructured":"Alhaj, M.: UML modeling using Eclipse Papyrus (2018). https:\/\/www.youtube.com\/watch?v=aMiqJXWfAtQ. Accessed 26 May 2020"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, P., El Amin Tebib, M.: Refining automation system control with MDE. In: Hammoudi, S., Ferreira Pires, L., Selic, B. (eds.) Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2020, pp. 425\u2013432. SCITEPRESS (2020). https:\/\/doi.org\/10.5220\/0009147804250432","DOI":"10.5220\/0009147804250432"},{"key":"10_CR3","doi-asserted-by":"publisher","unstructured":"Besnard, V., Brun, M., Jouault, F., Teodorov, C., Dhaussy, P.: Unified LTL verification and embedded execution of UML models. In: Proceedings of the 21th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2018, pp. 112\u2013122. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3239372.3239395","DOI":"10.1145\/3239372.3239395"},{"key":"10_CR4","unstructured":"Bhaduri, P., Ramesh, S.: Model checking of statechart models: Survey and research directions (2004)"},{"key":"10_CR5","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-642-23391-3_9","volume-title":"Evaluation of Novel Approaches to Software Engineering","author":"D Billington","year":"2011","unstructured":"Billington, D., Estivill-Castro, V., Hexel, R., Rock, A.: Requirements engineering via non-monotonic logics and state diagrams. In: Maciaszek, L.A., Loucopoulos, P. (eds.) ENASE 2010. CCIS, vol. 230, pp. 121\u2013135. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23391-3_9"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Birta, L.G., Arbez, G.: Modelling and Simulation \u2013 Exploring Dynamic System Behaviour. Springer, Heidelberg (2019)","DOI":"10.1007\/978-3-030-18869-6"},{"issue":"1","key":"10_CR7","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/JRA.1986.1087032","volume":"2","author":"R Brooks","year":"1986","unstructured":"Brooks, R.: A robust layered control system for a mobile robot. IEEE J. Robot. Autom. 2(1), 14\u201323 (1986). https:\/\/doi.org\/10.1109\/JRA.1986.1087032","journal-title":"IEEE J. Robot. Autom."},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Brooks, R.: The behavior language; user\u2019s guide. Technical report AIM-1227, Massachusetts Institute of Technology - MIT, Artificial Intelligence Lab Publications, Department of Electronics and Computer Science (1990)","DOI":"10.21236\/ADA225808"},{"issue":"2","key":"10_CR9","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1109\/MC.2014.45","volume":"47","author":"CR Bryce","year":"2014","unstructured":"Bryce, C.R., Kuhn, R.: Software testing [guest editors\u2019 introduction]. IEEE Comput. 47(2), 21\u201322 (2014)","journal-title":"IEEE Comput."},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Caltais, G., Leue, S., Singh, H.: Correctness of an ATL model transformation from sysml state machine diagrams to promela. In: Hammoudi, S., Ferreira Pires, L., Selic, B. (eds.) Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development, MODELSWARD, pp. 360\u2013372. SCITEPRESS (2020). https:\/\/doi.org\/10.5220\/0008968303600372","DOI":"10.5220\/0008968303600372"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Carrillo, M., Estivill-Castro, V., Rosenblueth, D.A.: Model-to-model transformations for efficient time-domain verification of concurrent models by NuSMV modules. In: Hammoudi, S., Ferreira Pires, L., Selic, B. (eds.) Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2020, pp. 287\u2013298. SCITEPRESS (2020). https:\/\/doi.org\/10.5220\/0008910202870298","DOI":"10.5220\/0008910202870298"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9","DOI":"10.1007\/978-3-319-08867-9"},{"issue":"3","key":"10_CR13","doi-asserted-by":"publisher","first-page":"2313","DOI":"10.1007\/s10270-018-0675-4","volume":"18","author":"F Ciccozzi","year":"2018","unstructured":"Ciccozzi, F., Malavolta, I., Selic, B.: Execution of UML models: a systematic review of research and practice. Softw. Syst. Modeling 18(3), 2313\u20132360 (2018). https:\/\/doi.org\/10.1007\/s10270-018-0675-4","journal-title":"Softw. Syst. Modeling"},{"issue":"4","key":"10_CR14","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2(4), 410\u2013425 (2000). https:\/\/doi.org\/10.1007\/s100090050046","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H.: Introduction to model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 1\u201326. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_1","DOI":"10.1007\/978-3-319-10575-8_1"},{"key":"10_CR16","unstructured":"Clarke, E., Heinle, W.: Modular translation of statecharts to SMV. Technical report, School of Computer Science, Carnegie Mellon University, Pittsburg, PA 15213 (2000). Sponsored by General Motors Corp"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/3-540-45739-9_22","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"W Damm","year":"2002","unstructured":"Damm, W., Jonsson, B.: Eliminating queues from RT UML model representations. In: Damm, W., Olderog, E.R. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 375\u2013393. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45739-9_22"},{"issue":"10","key":"10_CR18","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1145\/355604.361591","volume":"15","author":"EW Dijkstra","year":"1972","unstructured":"Dijkstra, E.W.: The humble programmer. Commun. ACM 15(10), 859\u2013866 (1972). https:\/\/doi.org\/10.1145\/355604.361591","journal-title":"Commun. ACM"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Drusinsky, D.: Modeling and Verification Using UML Statecharts: A Working Guide to Reactive System Design. Runtime Monitoring and Execution-based Model Checking. Newnes, Newton, MA, USA (2006)","DOI":"10.1016\/B978-075067949-7\/50004-0"},{"key":"10_CR20","unstructured":"Eriksson, H.E., Penker, M., Lyons, B., Fado, D.: UML 2 Toolkit. Wiley, Hoboken (2003)"},{"key":"10_CR21","unstructured":"Evans, A., Bruel, J.M., France, R., Lano, K., Rumpe, B.: Making UML precise. In: Andrade, L., Moreira, A., Deshpande, A., Kent, S. (eds.) OOPSLA 1998 Workshop on \u201cFormalizing UML. Why and How?\u201d, October 1998. www.se-rwth.de\/publications"},{"key":"10_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-658-19938-8","volume-title":"Future-Proof Software-Systems: A Sustainable Evolution Strategy","author":"F Furrer","year":"2019","unstructured":"Furrer, F.: Future-Proof Software-Systems: A Sustainable Evolution Strategy. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-658-19938-8"},{"key":"10_CR23","unstructured":"Grischa, L.: Papyrus 2.0: State machine diagrams (2016). www.youtube.com\/watch?v=xEC8bQ27lBk. Accessed 26 May 2020"},{"key":"10_CR24","unstructured":"Group, T.O.M.: Precise Semantics of UML State Machines (PSSM). OMG, May 2019"},{"key":"10_CR25","unstructured":"Group, T.O.M.: Precise Semantics of UML Structure (PSCS). OMG, June 2019"},{"key":"10_CR26","unstructured":"Guermazi, S., Tatibouet, J., Cuccuru, A., Seidewitz, e., Dhouib, S., G\u00e9rard, S.: Executable modeling with fUML and Alf in Papyrus: tooling and experiments. In: Mayerhofer, T., Langer, P., Seidewitz, E., Gray, J. (eds.) Proceedings of the 1st International Workshop on Executable Modeling co-located with ACM\/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (MODELS 2015). CEUR Workshop Proceedings, vol. 1560, pp. 3\u20138. CEUR-WS.org (2015)"},{"key":"10_CR27","unstructured":"Kang, I., Lee, I.: A state minimization algorithm for communicating state machines with arbitrary data space. Technical report MS-CIS-93-07, Department of Computer & Information Science, University of Pennsylvania, January 1993"},{"key":"10_CR28","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-45739-9_23","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"A Knapp","year":"2002","unstructured":"Knapp, A., Merz, S., Rauh, C.: Model checking timed UML state machines and collaborations. In: Damm, W., Olderog, E.R. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 395\u2013414. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45739-9_23"},{"key":"10_CR29","doi-asserted-by":"publisher","unstructured":"Kopetz, H.: Real-Time Systems: Design Principles for Distributed Embedded Applications, 2nd edn. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-1-4419-8237-7","DOI":"10.1007\/978-1-4419-8237-7"},{"key":"10_CR30","unstructured":"Lamport, L.: The $$\\text{TLA}^{+}$$ home page, 6th December 2018. lamport.azurewebsites.net\/tla\/tla.html. Accessed 20 Apr 2020"},{"key":"10_CR31","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997). https:\/\/doi.org\/10.1007\/s100090050010, https:\/\/doi.org\/10.1007\/s100090050010","DOI":"10.1007\/s100090050010"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Mataric, M.: Integration of representation into goal-driven behavior-based robots. IEEE Trans. Robot. Autom. 8(3), 304\u2013312 (1992). https:\/\/doi.org\/10.1109\/70.143349","DOI":"10.1109\/70.143349"},{"key":"10_CR33","unstructured":"McColl, C., Estivill-Castro, V. Hexel, R.: An OO and functional framework for versatile semantics of logic-labelled finite state machines. In: Lavazza, L. (ed.) ICSEA : The Twelfth International Conference on Software Engineering Advances, pp. 238\u2013243. Int. Academy, Research, and Industry Association (IARIA), Curran, 8th\u201312th October 2017"},{"key":"10_CR34","unstructured":"McMillan, K.L.: Symbolic Model Checking \u2013 An approach to the state explosion problem. Ph.D. thesis, Carnegie Mellon University, 5000 Forbes Ave, Pittsburgh, PA 15213, United States, May 1992. cMU-CS-92-131"},{"key":"10_CR35","doi-asserted-by":"publisher","DOI":"10.1201\/9781315217512","volume-title":"Time-Triggered Communication","author":"R Obermaisser","year":"2011","unstructured":"Obermaisser, R., Kopetz, H.: Chapter 3: properties of time-triggered communication systems. In: Obermaisser, R. (ed.) Time-Triggered Communication. CRC Press Inc., USA (2011)"},{"key":"10_CR36","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-319-94764-8_13","volume-title":"Model-Driven Engineering and Software Development","author":"VC Pham","year":"2018","unstructured":"Pham, V.C., Radermacher, A., G\u00e9rard, S., Li, S.: A framework for UML-based component-based design and code generation for reactive systems. In: Pires, L.F., Hammoudi, S., Selic, B. (eds.) MODELSWARD 2017. CCIS, vol. 880, pp. 300\u2013327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94764-8_13"},{"issue":"5","key":"10_CR37","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1109\/32.815324","volume":"25","author":"JM Rushby","year":"1999","unstructured":"Rushby, J.M.: Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Trans. Softw. Eng. 25(5), 651\u2013660 (1999). https:\/\/doi.org\/10.1109\/32.815324","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/3-540-45449-7_22","volume-title":"Embedded Software","author":"J Rushby","year":"2001","unstructured":"Rushby, J.: Bus architectures for safety-critical embedded systems. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 306\u2013323. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45449-7_22"},{"key":"10_CR39","doi-asserted-by":"publisher","DOI":"10.1201\/b16463","volume-title":"Practical UML Statecharts in C\/C++, Second Edition: Event-Driven Programming for Embedded Systems","author":"M Samek","year":"2008","unstructured":"Samek, M.: Practical UML Statecharts in C\/C++, Second Edition: Event-Driven Programming for Embedded Systems, 2nd edn. Newnes, Newton (2008)","edition":"2"},{"key":"10_CR40","doi-asserted-by":"publisher","unstructured":"Seshia, S.A., Sharygina, N., Tripakis, S.: Modeling for verification. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 1\u201326. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_1","DOI":"10.1007\/978-3-319-10575-8_1"},{"key":"10_CR41","unstructured":"Weise, C.: An incremental formal semantics for PROMELA. In: Proceedings of the Third SPIN Workshop, SPIN 1997 (1997)"},{"key":"10_CR42","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages: An Introduction","author":"G Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)"}],"container-title":["Communications in Computer and Information Science","Model-Driven Engineering and Software Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-67445-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,1]],"date-time":"2021-02-01T04:31:27Z","timestamp":1612153887000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-67445-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030674441","9783030674458"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-67445-8_10","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"value":"1865-0929","type":"print"},{"value":"1865-0937","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 February 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MODELSWARD","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Model-Driven Engineering and Software Development","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Valletta","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Malta","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 February 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 February 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"modelsward2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.modelsward.org\/?y=2020","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"PRIMORIS","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"66","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}