{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T20:23:36Z","timestamp":1791231816048,"version":"4.1.0"},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2021,11,21]],"date-time":"2021-11-21T00:00:00Z","timestamp":1637452800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,11,21]],"date-time":"2021-11-21T00:00:00Z","timestamp":1637452800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2021,12]]},"DOI":"10.1007\/s10270-021-00923-9","type":"journal-article","created":{"date-parts":[[2021,11,21]],"date-time":"2021-11-21T14:02:17Z","timestamp":1637503337000},"page":"1825-1855","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Unified verification and monitoring of executable UML specifications"],"prefix":"10.1007","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6744-4149","authenticated-orcid":false,"given":"Valentin","family":"Besnard","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ciprian","family":"Teodorov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Jouault","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthias","family":"Brun","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philippe","family":"Dhaussy","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,11,21]]},"reference":[{"issue":"3","key":"923_CR1","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10515-007-0012-6","volume":"14","author":"M Autili","year":"2007","unstructured":"Autili, M., Inverardi, P., Pelliccione, P.: Graphical scenarios for specifying temporal properties: an automated approach. Autom. Softw. Eng. 14(3), 293\u2013340 (2007). https:\/\/doi.org\/10.1007\/s10515-007-0012-6","journal-title":"Autom. Softw. Eng."},{"key":"923_CR2","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Babiak","year":"2012","unstructured":"Babiak, T., K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: LTL to B\u00fcchi automata translation: fast and more deterministic. In: Flanagan, C., K\u00f6nig, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 95\u2013109. Springer, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/3-540-44585-4_6"},{"key":"923_CR3","doi-asserted-by":"publisher","DOI":"10.5555\/1373322","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). MIT Press, Cambridge (2008). https:\/\/doi.org\/10.5555\/1373322"},{"key":"923_CR4","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: EAGLE Does Space Efficient LTL Monitoring. Pre-Print CSPP-25 (2003)"},{"issue":"4","key":"923_CR5","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1-14:64 (2011). https:\/\/doi.org\/10.1145\/2000799.2000800","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"923_CR6","unstructured":"Besnard, V., Brun, M., Dhaussy, P., Jouault, F., Olivier, D., Teodorov, C.: Towards one model interpreter for both design and deployment. In: 3rd International Workshop on Executable Modeling (EXE 2017). Austin, United States (2017)"},{"key":"923_CR7","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-030-04771-9_38","volume-title":"Software Technologies: Applications and Foundations","author":"V Besnard","year":"2018","unstructured":"Besnard, V., Brun, M., Jouault, F., Teodorov, C., Dhaussy, P.: Embedded UML model execution to bridge the gap between design and runtime. In: Mazzara, M., Ober, I., Sala\u00fcn, G. (eds.) Software Technologies: Applications and Foundations, pp. 519\u2013528. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-04771-9_38"},{"key":"923_CR8","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: ACM\/IEEE 21th International Conference on Model Driven Engineering Languages and Systems (MODELS \u201918). Copenhagen, Denmark (2018). https:\/\/doi.org\/10.1145\/3239372.3239395","DOI":"10.1145\/3239372.3239395"},{"key":"923_CR9","doi-asserted-by":"crossref","unstructured":"Besnard, V., Teodorov, C., Jouault, F., Brun, M., Dhaussy, P.: A model checkable UML soccer player. In: 3rd Workshop on Model-Driven Engineering Tools, pp. 211\u2013220. Munich, Germany (2019)","DOI":"10.1109\/MODELS-C.2019.00035"},{"key":"923_CR10","doi-asserted-by":"publisher","unstructured":"Besnard, V., Teodorov, C., Jouault, F., Brun, M., Dhaussy, P.: Verifying and monitoring uml models with observer automata. In: ACM\/IEEE 22th International Conference on Model Driven Engineering Languages and Systems (MODELS \u201919), pp. 161\u2013171. Munich, Germany (2019). https:\/\/doi.org\/10.1109\/MODELS.2019.000-5","DOI":"10.1109\/MODELS.2019.000-5"},{"key":"923_CR11","doi-asserted-by":"publisher","unstructured":"Bochot, T., Virelizier, P., Waeselynck, H., Wiels, V.: Model checking flight control systems: the Airbus experience. In: 2009 31st International Conference on Software Engineering\u2014Companion Volume, pp. 18\u201327 (2009). https:\/\/doi.org\/10.1109\/ICSE-COMPANION.2009.5070960","DOI":"10.1109\/ICSE-COMPANION.2009.5070960"},{"key":"923_CR12","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-16612-9_15","volume-title":"Runtime Verification","author":"E Bodden","year":"2010","unstructured":"Bodden, E., Lam, P., Hendren, L.: Clara: a framework for partially evaluating finite-state runtime monitors ahead of time. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) Runtime Verification, pp. 183\u2013197. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_15"},{"key":"923_CR13","doi-asserted-by":"crossref","unstructured":"Boniol, F., Wiels, V.: The landing gear system case study. In: ABZ 2014: The Landing Gear Case Study, pp. 1\u201318. Springer, Cham (2014)","DOI":"10.1007\/978-3-319-07512-9_1"},{"key":"923_CR14","unstructured":"Brumbulli, M., Gaudin, E., Teodorov, C.: Automatic verification of BPMN models. In: 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020). Toulouse, France (2020)"},{"key":"923_CR15","doi-asserted-by":"publisher","unstructured":"Chen, F., D\u2019Amorim, M., Ro\u015fu, G.: A formal monitoring-based framework for software development and analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) Formal Methods and Software Engineering, pp. 357\u2013372. Springer, Berlin, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30482-1_31","DOI":"10.1007\/978-3-540-30482-1_31"},{"key":"923_CR16","unstructured":"Ciccozzi, F.: From models to code and back: a round-trip approach for model-driven engineering of embedded systems. M\u00e4lardalen University, Embedded Systems. Ph.D. thesis (2014)"},{"key":"923_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-018-0675-4","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. Model. (2018). https:\/\/doi.org\/10.1007\/s10270-018-0675-4","journal-title":"Softw. Syst. Model."},{"key":"923_CR18","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction\u2014CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction\u2014CADE-25, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"923_CR19","unstructured":"Dhaussy, P., Le Roux, L., Teodorov, C.: V\u00e9rification formelle de propri\u00e9t\u00e9s : Application de l\u2019outil OBP au cas d\u2019\u00e9tude CCS. G\u00e9nie logiciel 109 (2014)"},{"key":"923_CR20","unstructured":"Diot, C., de\u00a0Simone, R., Huitema, C.: Communication Protocols Development Using ESTEREL (1994)"},{"key":"923_CR21","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/10722468_19","volume-title":"SPIN Model Checking and Software Verification","author":"D Drusinsky","year":"2000","unstructured":"Drusinsky, D.: The temporal rover and the ATG rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN Model Checking and Software Verification, pp. 323\u2013330. Springer, Berlin, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722468_19"},{"key":"923_CR22","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized B\u00fcchi automata. In: Proceedings of The IEEE Computer Society\u2019s 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems, MASCOTS \u201904, pp. 76\u201383. IEEE Computer Society, Washington, DC, USA (2004). https:\/\/doi.org\/10.1109\/MASCOT.2004.1348184","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"923_CR23","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.ohx.2017.09.001","volume":"2","author":"J Ferretti","year":"2017","unstructured":"Ferretti, J., Di Pietro, L., De Maria, C.: Open-source automated external defibrillator. HardwareX 2, 61\u201370 (2017). https:\/\/doi.org\/10.1016\/j.ohx.2017.09.001","journal-title":"HardwareX"},{"key":"923_CR24","doi-asserted-by":"publisher","unstructured":"Gaiser, A., Schwoon, S.: Comparison of algorithms for checking emptiness on B\u00fcchi automata. In: Hlinen\u00fd, P., Maty\u00e1\u0161, V., Vojnar, T. (eds.) Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS\u201909), OpenAccess Series in Informatics (OASIcs), vol. 13, pp. 18\u201326. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2009). https:\/\/doi.org\/10.4230\/DROPS.MEMICS.2009.2349","DOI":"10.4230\/DROPS.MEMICS.2009.2349"},{"key":"923_CR25","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification, pp. 53\u201365. Springer, Berlin, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_6"},{"key":"923_CR26","doi-asserted-by":"publisher","unstructured":"Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) Algebraic Methodology and Software Technology, vol. AMAST\u201993, pp. 83\u201396. Springer, London (1994). https:\/\/doi.org\/10.1007\/978-1-4471-3227-1_8","DOI":"10.1007\/978-1-4471-3227-1_8"},{"key":"923_CR27","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.P., Stevens, P. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 342\u2013356. Springer, Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_24"},{"issue":"2","key":"923_CR28","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/s10009-003-0117-6","volume":"6","author":"K Havelund","year":"2004","unstructured":"Havelund, K., Ro\u015fu, G.: Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Transf. 6(2), 158\u2013173 (2004). https:\/\/doi.org\/10.1007\/s10009-003-0117-6","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"923_CR29","doi-asserted-by":"publisher","unstructured":"Havelund, K., Ro\u015fu, G.: Monitoring Java programs with Java pathexplorer. Electronic Notes in Theoretical Computer Science 55(2), 200\u2013217 (2001). https:\/\/doi.org\/10.1016\/S1571-0661(04)00253-1. RV\u20192001, Runtime Verification (in connection with CAV \u201901)","DOI":"10.1016\/S1571-0661(04)00253-1"},{"key":"923_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-020-00780-y","author":"N Hili","year":"2020","unstructured":"Hili, N., Bagherzadeh, M., Jahed, K., Dingel, J.: A model-based architecture for interactive run-time monitoring. Softw. Syst. Model. (2020). https:\/\/doi.org\/10.1007\/s10270-020-00780-y","journal-title":"Softw. Syst. Model."},{"key":"923_CR31","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-540-24732-6_6","volume-title":"Model Checking Software","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J., Joshi, R.: Model-driven software verification. In: Graf, S., Mounier, L. (eds.) Model Checking Software, pp. 76\u201391. Springer, Berlin, Heidelberg (2004)"},{"key":"923_CR32","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-1-4614-2266-2_5","volume-title":"Model-Based Debugging of Embedded Software Systems","author":"P Iyenghar","year":"2017","unstructured":"Iyenghar, P., Pulvermueller, E., Westerkamp, C., Wuebbelmann, J., Uelschen, M.: Model-Based Debugging of Embedded Software Systems, pp. 107\u2013132. Springer, New York (2017). https:\/\/doi.org\/10.1007\/978-1-4614-2266-2_5"},{"key":"923_CR33","doi-asserted-by":"publisher","unstructured":"Jouault, F., Besnard, V., Le\u00a0Calvar, T., Teodorov, C., Brun, M., Delatour, J.: Designing, animating, and verifying partial UML models. In: ACM\/IEEE 23rd International Conference on Model Driven Engineering Languages and Systems (MODELS \u201920), MODELS \u201920. Virtual Event, Canada (2020). https:\/\/doi.org\/10.1145\/3365438.3410967","DOI":"10.1145\/3365438.3410967"},{"key":"923_CR34","unstructured":"Jouault, F., Delatour, J.: Towards fixing sketchy UML models by leveraging textual notations: application to real-time embedded systems. In: Brucker, A.D., Dania, C., Georg, G., Gogolla, M. (eds.) OCL 2014, OCL and Textual Modeling: Applications and Case Studies, vol. 1285, pp. 73\u201382. Valencia, Spain (2014)"},{"key":"923_CR35","first-page":"21","volume":"109","author":"F Jouault","year":"2014","unstructured":"Jouault, F., Teodorov, C., Delatour, J., Le Roux, L., Dhaussy, P.: Transformation de mod\u00e8les UML vers Fiacre, via les langages interm\u00e9diaires tUML et ABCD. G\u00e9nie Logiciel 109, 21\u201327 (2014)","journal-title":"G\u00e9nie Logiciel"},{"key":"923_CR36","doi-asserted-by":"publisher","unstructured":"Kane, A.: Runtime Monitoring for Safety-Critical Embedded Systems (2015). https:\/\/doi.org\/10.1184\/R1\/6721376.v1","DOI":"10.1184\/R1\/6721376.v1"},{"issue":"2","key":"923_CR37","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/B:FORM.0000017719.43755.7c","volume":"24","author":"M Kim","year":"2004","unstructured":"Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance approach for Java programs. Form. Methods Syst. Des. 24(2), 129\u2013155 (2004)","journal-title":"Form. Methods Syst. Des."},{"key":"923_CR38","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, Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45739-9_23"},{"key":"923_CR39","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-540-69489-2_6","volume-title":"Models in Software Engineering","author":"A Knapp","year":"2007","unstructured":"Knapp, A., Wuttke, J.: Model checking of UML 2.0 interactions. In: K\u00fchne, T. (ed.) Models in Software Engineering, pp. 42\u201351. Springer, Berlin, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69489-2_6"},{"issue":"5\u20136","key":"923_CR40","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"SA Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical analysis of modal logic i normal modal propositional calculi. Math. Logic Q. 9(5\u20136), 67\u201396 (1963). https:\/\/doi.org\/10.1002\/malq.19630090502","journal-title":"Math. Logic Q."},{"key":"923_CR41","unstructured":"Leroux, L., Delatour, J., Dhaussy, P.: Mod\u00e9lisation UML d\u2019un r\u00e9gulateur de vitesse automobile. G\u00e9nie Logiciel 109, (2014)"},{"key":"923_CR42","doi-asserted-by":"publisher","unstructured":"Liu, S., Liu, Y., Sun, J., Zheng, M., Wadhwa, B., Dong, J.S.: USMMC: a self-contained model checker for UML state machines. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2013, pp. 623\u2013626. ACM, New York, NY, USA (2013). https:\/\/doi.org\/10.1145\/2491411.2494595","DOI":"10.1145\/2491411.2494595"},{"key":"923_CR43","doi-asserted-by":"crossref","unstructured":"Mekki, A., Ghazel, M., Toguyeni, A.: Validating Time-constrained Systems Using UML Statecharts Patterns and Timed Automata Observers, vol. VECoS\u201909, pp. 112\u2013124. BCS Learning & Development Ltd., Swindon, UK (2009)","DOI":"10.14236\/ewic\/VECOS2009.11"},{"key":"923_CR44","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-540-24732-6_9","volume-title":"Model Checking Software","author":"I Ober","year":"2004","unstructured":"Ober, I., Graf, S., Ober, I.: Validation of UML models via a mapping to communicating extended timed automata. In: Graf, S., Mounier, L. (eds.) Model Checking Software, pp. 127\u2013145. Springer, Berlin, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24732-6_9"},{"issue":"2","key":"923_CR45","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/s10009-005-0205-x","volume":"8","author":"I Ober","year":"2006","unstructured":"Ober, I., Graf, S., Ober, I.: Validating timed UML models by simulation and verification. Int. J. Softw. Tools Technol. Transf. 8(2), 128\u2013145 (2006). https:\/\/doi.org\/10.1007\/s10009-005-0205-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"923_CR46","unstructured":"OMG: Action Language for Foundational UML (Alf) (2017). www.omg.org\/spec\/ALF\/1.1\/PDF"},{"key":"923_CR47","unstructured":"OMG: Precise Semantics of UML State Machines (2017). https:\/\/www.omg.org\/spec\/PSSM\/1.0\/Beta1\/PDF"},{"key":"923_CR48","unstructured":"OMG: Semantics of a Foundational Subset for Executable UML Models (2017). https:\/\/www.omg.org\/spec\/FUML\/1.3\/PDF"},{"key":"923_CR49","unstructured":"OMG: Unified Modeling Language (2017). https:\/\/www.omg.org\/spec\/UML\/2.5.1\/PDF"},{"key":"923_CR50","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-16612-9_26","volume-title":"Runtime Verification","author":"L Pike","year":"2010","unstructured":"Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) Runtime Verification, pp. 345\u2013359. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_26"},{"key":"923_CR51","first-page":"216","volume-title":"Specification and Verification of Concurrent Systems in CESAR","author":"JP Queille","year":"2008","unstructured":"Queille, J.P., Sifakis, J.: Specification and Verification of Concurrent Systems in CESAR, pp. 216\u2013230. Springer, Berlin, Heidelberg (2008)"},{"key":"923_CR52","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/978-3-662-46681-0_55","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Reger","year":"2015","unstructured":"Reger, G., Cruz, H.C., Rydeheard, D.: MarQ: monitoring at runtime with QEA. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 596\u2013610. Springer, Berlin, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_55"},{"key":"923_CR53","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/11817963_25","volume-title":"Computer Aided Verification","author":"G Ro\u015fu","year":"2006","unstructured":"Ro\u015fu, G., Bensalem, S.: Allen linear (interval) temporal logic\u2014translation to LTL and monitor synthesis. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification, pp. 263\u2013277. Springer, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_25"},{"key":"923_CR54","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-89247-2_4","volume-title":"Runtime Verification","author":"G Ro\u015fu","year":"2008","unstructured":"Ro\u015fu, G., Chen, F., Ball, T.: Synthesizing monitors for safety properties: this time with calls and returns. In: Leucker, M. (ed.) Runtime Verification, pp. 51\u201368. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89247-2_4"},{"key":"923_CR55","unstructured":"Tan, L., Kim, J., Sokolsky, O., Lee, I.: Model-based testing and monitoring for hybrid embedded systems. In: Proceedings of the 2004 IEEE International Conference on Information Reuse and Integration, 2004. IRI 2004, pp. 487\u2013492 (2004)"},{"issue":"2","key":"923_CR56","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10009-015-0401-2","volume":"19","author":"C Teodorov","year":"2017","unstructured":"Teodorov, C., Dhaussy, P., Le Roux, L.: Environment-driven reachability for timed systems. Int. J. Softw. Tools Technol. Transf. 19(2), 229\u2013245 (2017). https:\/\/doi.org\/10.1007\/s10009-015-0401-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"7","key":"923_CR57","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1002\/stvr.1611.Stvr.1611","volume":"26","author":"C Teodorov","year":"2016","unstructured":"Teodorov, C., Le Roux, L., Drey, Z., Dhaussy, P.: Past-Free[ze] reachability analysis: reaching further with DAG-directed exhaustive state-space analysis. Softw. Test. Verif. Reliab. 26(7), 516\u2013542 (2016). https:\/\/doi.org\/10.1002\/stvr.1611.Stvr.1611","journal-title":"Softw. Test. Verif. Reliab."},{"key":"923_CR58","doi-asserted-by":"publisher","unstructured":"Torres Lopez, C., Gurdeep Singh, R., Marr, S., Gonzalez Boix, E., Scholliers, C.: Multiverse Debugging: Non-deterministic Debugging for Non-deterministic Programs. ECOOP. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2019.27","DOI":"10.4230\/LIPIcs.ECOOP.2019.27"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-021-00923-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-021-00923-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-021-00923-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,6]],"date-time":"2021-12-06T03:14:09Z","timestamp":1638760449000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-021-00923-9"}},"subtitle":["A transformation-free approach"],"short-title":[],"issued":{"date-parts":[[2021,11,21]]},"references-count":58,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["923"],"URL":"https:\/\/doi.org\/10.1007\/s10270-021-00923-9","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,11,21]]},"assertion":[{"value":"10 May 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 August 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 August 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 November 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}