{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T20:10:06Z","timestamp":1759695006608,"version":"build-2065373602"},"reference-count":64,"publisher":"SAGE Publications","issue":"10","license":[{"start":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T00:00:00Z","timestamp":1751587200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["SIMULATION"],"published-print":{"date-parts":[[2025,10]]},"abstract":"<jats:p>Real-time DEVS (RT-DEVS) can model systems with quantitative temporal requirements. Ensuring that such models verify that kind of temporal properties requires to use something beyond simulation. In this work, we use the model checker Uppaal to verify a class of recurrent quantitative temporal properties appearing in RT-DEVS models, even though Uppaal cannot deal in general with this kind of properties. In order to overcome these limitations, we use the technique known as automata observer. Second, by introducing mutations to quantitative temporal properties, we are able to find errors in RT-DEVS models and their implementations. A case study from the railway domain is presented.<\/jats:p>","DOI":"10.1177\/00375497251340070","type":"journal-article","created":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T04:37:29Z","timestamp":1751603849000},"page":"1057-1076","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":0,"title":["Verification of quantitative temporal properties in RealTime-DEVS"],"prefix":"10.1177","volume":"101","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-7502-2847","authenticated-orcid":false,"given":"Ariel","family":"Gonz\u00e1lez","sequence":"first","affiliation":[{"name":"Universidad Nacional de R\u00edo Cuarto, Argentina"}]},{"given":"Maximiliano","family":"Cristi\u00e1","sequence":"additional","affiliation":[{"name":"Universidad Nacional de Rosario and CIFASIS, Argentina"}]},{"given":"Carlos","family":"Luna","sequence":"additional","affiliation":[{"name":"Universidad de la Rep\u00fablica, Uruguay"}]}],"member":"179","published-online":{"date-parts":[[2025,7,4]]},"reference":[{"key":"e_1_3_4_2_2","doi-asserted-by":"publisher","DOI":"10.1155\/2018\/7284815"},{"key":"e_1_3_4_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2017.01.011"},{"key":"e_1_3_4_4_2","unstructured":"Zeigler B Praehofer H Kim T. Theory of modeling and simulation: integrating discrete event and continuous complex dynamic systems. Cambridge MA: Academic Press 2000 http:\/\/books.google.com.uy\/books?id=REzmYOQmHuQC"},{"key":"e_1_3_4_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35746-6_1"},{"key":"e_1_3_4_6_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008262409521"},{"key":"e_1_3_4_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_3_4_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.24271"},{"key":"e_1_3_4_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-658-00397-5_2"},{"key":"e_1_3_4_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_4_11_2","unstructured":"Lamport L. Specifying systems: the TLA+ language and tools for hardware and software engineers. Boston MA: Addison-Wesley 2002 http:\/\/research.microsoft.com\/users\/lamport\/tla\/book.html"},{"key":"e_1_3_4_12_2","first-page":"46","volume-title":"18th annual symposium on foundations of computer science","author":"Pnueli A","unstructured":"Pnueli A. The temporal logic of programs. In: 18th annual symposium on foundations of computer science, Providence, RI, 31 October\u20131 November 1977. New York: IEEE Computer Society, pp. 46\u201357."},{"key":"e_1_3_4_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_4_14_2","first-page":"359","volume-title":"Proceedings of the 14th international conference on computer aided verification, CAV \u201902","author":"Cimatti A","unstructured":"Cimatti A, Clarke EM, Giunchiglia E, et al. NuSMV 2: an opensource tool for symbolic model checking. In: Proceedings of the 14th international conference on computer aided verification, CAV \u201902, Berlin, 27\u201331 July 2002, pp. 359\u2013364. New York: Springer."},{"key":"e_1_3_4_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_4_16_2","first-page":"414","volume-title":"Proceedings of the Fifth annual symposium on logic in computer science (LICS \u201990)","author":"Alur R","unstructured":"Alur R, Courcoubetis C, Dill DL. Model-checking for real-time systems. In: Proceedings of the Fifth annual symposium on logic in computer science (LICS \u201990), Philadelphia, PA, 4\u20137 June 1990. New York: IEEE, pp. 414\u2013425."},{"key":"e_1_3_4_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_3_4_18_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(1:8)2007"},{"key":"e_1_3_4_19_2","doi-asserted-by":"crossref","unstructured":"Mekki A Ghazel M Toguyeni A. Validating time-constrained systems using UML Statecharts patterns and timed automata observers 2009 https:\/\/www.scienceopen.com\/hosted-document?doi=10.14236\/ewic\/VECOS2009.11","DOI":"10.14236\/ewic\/VECOS2009.11"},{"key":"e_1_3_4_20_2","first-page":"19","volume-title":"NASA formal methods","author":"Backes JD","unstructured":"Backes JD, Whalen MW, Gacek A, et al. On implementing real-time specification patterns using observers. In: Rayadurgam S, Tkachuk O (eds.) NASA formal methods. Cham: Springer, pp. 19\u201333."},{"key":"e_1_3_4_21_2","volume-title":"Techniques for automatic verification of real-time systems","author":"Alur R.","year":"1992","unstructured":"Alur R. Techniques for automatic verification of real-time systems. PhD thesis, Stanford University, Stanford, CA, 1992."},{"key":"e_1_3_4_22_2","first-page":"349","volume-title":"Proceedings of the XXII IberoAmerican Conference on Software Engineering, CIbSE 2019","author":"Gonzalez A","unstructured":"Gonzalez A, Cristi\u00e1 M, Luna C. Mutants for metric temporal logic formulas. In: Mar\u00edn B, Brito IS, Mora MK, et al. (eds) Proceedings of the XXII IberoAmerican Conference on Software Engineering, CIbSE 2019, La Habana, Cuba, 22\u201326 April 2019, pp. 349\u2013362. Newry, Northern Ireland: Curran Associates."},{"key":"e_1_3_4_23_2","doi-asserted-by":"publisher","DOI":"10.1177\/0037549705052229"},{"key":"e_1_3_4_24_2","first-page":"601","volume-title":"2008 international multiconference on computer science and information technology","author":"Furfaro A","unstructured":"Furfaro A, Nigro L. Embedded control systems design based on RT-DEVS and temporal analysis using Uppaal. In: 2008 international multiconference on computer science and information technology, Wisla, 20\u201322 October 2008, pp. 601\u2013608. New York: IEEE."},{"key":"e_1_3_4_25_2","first-page":"229","volume-title":"41st annual simulation symposium (anss-41 2008)","author":"Cicirelli F","unstructured":"Cicirelli F, Furfaro A, Nigro L. Actor-based simulation of PDEVS systems over HLA. In: 41st annual simulation symposium (anss-41 2008), Ottawa, ON, Canada, 13\u201316 April 2008, pp. 229\u2013236. New York: IEEE."},{"key":"e_1_3_4_26_2","first-page":"312","volume-title":"Proceedings of the 2007 summer computer simulation conference. SCSC \u201907","author":"Dacharry HP","unstructured":"Dacharry HP, Giambiasi N. A formal verification approach for DEVS. In: Proceedings of the 2007 summer computer simulation conference. SCSC \u201907, San Diego, CA, 16\u201319 July 2007, pp. 312\u2013319. New York: ACM."},{"key":"e_1_3_4_27_2","doi-asserted-by":"publisher","DOI":"10.4067\/S0718-33052019000400682"},{"key":"e_1_3_4_28_2","first-page":"147","volume-title":"Proceedings of the 2014 ACM SIGMOD international conference on management of data, SIGMOD \u201914","author":"Toshniwal A","unstructured":"Toshniwal A, Taneja S, Shukla A, et al. Storm@twitter. In: Proceedings of the 2014 ACM SIGMOD international conference on management of data, SIGMOD \u201914, Snowbird, UT, 22\u201327 June 2014, pp. 147\u2013156. New York: Association for Computing Machinery."},{"key":"e_1_3_4_29_2","doi-asserted-by":"publisher","DOI":"10.1177\/0037549711424424"},{"key":"e_1_3_4_30_2","doi-asserted-by":"publisher","DOI":"10.1201\/b12667-5"},{"volume-title":"Proceedings of the symposium on theory of modeling & simulation, TMS\/DEVS \u201917","author":"Gholami S","key":"e_1_3_4_31_2","unstructured":"Gholami S, Sarjoughian HS. Modeling and verification of network-on-chip using constrained-DEVS. In: Proceedings of the symposium on theory of modeling & simulation, TMS\/DEVS \u201917, Virginia Beach, VI, 23\u201326 April 2017. San Diego, CA: Society for Computer Simulation International."},{"key":"e_1_3_4_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21768-5_6"},{"key":"e_1_3_4_33_2","first-page":"493","volume-title":"Proceedings of the 2004 IEEE international conference on information reuse and integration","author":"Tan L","unstructured":"Tan L, Sokolsky O, Lee I. Specification-based testing with linear temporal logic. In: Proceedings of the 2004 IEEE international conference on information reuse and integration, Las Vegas, NV, 8\u201310 November 2004, pp. 493\u2013498. New York: IEEE."},{"key":"e_1_3_4_34_2","first-page":"116","volume-title":"2017 IEEE international conference on software testing, verification and validation workshops (ICSTW)","author":"Trakhtenbrot MB","unstructured":"Trakhtenbrot MB. Mutation patterns for temporal requirements of reactive systems. In: 2017 IEEE international conference on software testing, verification and validation workshops (ICSTW), Tokyo, Japan, 13\u201317 March 2017, pp.116\u2013121. New York: IEEE."},{"key":"e_1_3_4_35_2","first-page":"11","volume-title":"Proceedings of the 1993 international symposium on software testing and analysis, ISSTA 1993","author":"Stocks P","unstructured":"Stocks P, Carrington DA. Test template framework: a specification-based testing case study. In: Ostrand TJ, Weyuker EJ (eds.) Proceedings of the 1993 international symposium on software testing and analysis, ISSTA 1993, Cambridge, MA, 28\u201330 June 1993, pp. 11\u201318. New York: ACM."},{"key":"e_1_3_4_36_2","first-page":"1","volume-title":"2021 40th international conference of the Chilean computer science society (SCCC)","author":"Gonzalez A","unstructured":"Gonzalez A, Cristi\u00e1 M, Luna C. Error finding in real-time systems using mutants of temporal properties. In: 2021 40th international conference of the Chilean computer science society (SCCC), La Serena, Chile, 15\u201319 November 2021, pp. 1\u20138. New York: IEEE."},{"key":"e_1_3_4_37_2","first-page":"177","volume-title":"2018 Winter simulation conference (WSC)","author":"Wainer GA","unstructured":"Wainer GA, Goldstein R, Khan A. Introduction to the discrete event system specification formalism and its application for modeling and simulating cyber-physical systems. In: 2018 Winter simulation conference (WSC), Gothenburg, 9\u201312 December, pp. 177\u2013191. New York: IEEE."},{"key":"e_1_3_4_38_2","first-page":"87","volume-title":"Timed automata: semantics, algorithms and tools","author":"Bengtsson J","year":"2004","unstructured":"Bengtsson J, Yi W. Timed automata: semantics, algorithms and tools. Berlin: Springer, 2004, pp. 87\u2013124."},{"key":"e_1_3_4_39_2","doi-asserted-by":"crossref","unstructured":"Gonz\u00e1lez A. Experimental data for verification of quantitative temporal properties in RealTime-DEVS with Uppaal 2024 https:\/\/github.com\/agonzalez2020\/Train-Controller-Alarm-Rtdevs","DOI":"10.2139\/ssrn.4974377"},{"volume-title":"Proceedings of the 2009 spring simulation multiconference, SpringSim \u201909","author":"Saadawi H","key":"e_1_3_4_40_2","unstructured":"Saadawi H, Wainer G. Verification of real-time DEVS models. In: Proceedings of the 2009 spring simulation multiconference, SpringSim \u201909, San Diego, CA, 22\u201327 March. San Diego, CA: Society for Computer Simulation International."},{"key":"e_1_3_4_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2003.1231146"},{"key":"e_1_3_4_42_2","first-page":"334","article-title":"Towards an automatic model transformation mechanism from UML state machines to DEVS models","volume":"18","author":"Gonz\u00e1lez A","year":"2015","unstructured":"Gonz\u00e1lez A, Luna C, Daniele M, et al. Towards an automatic model transformation mechanism from UML state machines to DEVS models. CLEI Electron J 2015; 18: 334.","journal-title":"CLEI Electron J"},{"key":"e_1_3_4_43_2","doi-asserted-by":"crossref","unstructured":"Gonz\u00e1lez A Luna CD Abella R. UML state machine as modeling language for DEVS formalism. In: XLII Latin American computing conference CLEI 2016 Valpara\u00edso Chile 14\u201316 October 2016 pp. 1\u201312. New York: IEEE http:\/\/ieeexplore.ieee.org\/xpl\/mostRecentIssue.jsp?punumber=7814932","DOI":"10.1109\/CLEI.2016.7833350"},{"key":"e_1_3_4_44_2","doi-asserted-by":"publisher","DOI":"10.1177\/0037549710368029"},{"key":"e_1_3_4_45_2","doi-asserted-by":"crossref","unstructured":"Dwyer MB Avrunin GS Corbett JC. Patterns in property specifications for finite-state verification. In: Boehm BW Garlan D Kramer J (eds) Proceedings of the 1999 International Conference on Software Engineering ICSE\u201999 Los Angeles CA 16\u201322 May 1999 pp. 411\u2013420. New York: ACM http:\/\/dblp.uni-trier.de\/db\/conf\/icse\/icse99.html#DwyerAC99","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_4_46_2","first-page":"372","volume-title":"Proceedings of the 27th international conference on software engineering. ICSE \u201905","author":"Konrad S","unstructured":"Konrad S, Cheng BHC. Real-time specification patterns. In: Proceedings of the 27th international conference on software engineering. ICSE \u201905, St. Louis, MO, 15\u201321 May 2205, pp. 372\u2013381. New York: ACM."},{"key":"e_1_3_4_47_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.035"},{"key":"e_1_3_4_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32469-7_1"},{"key":"e_1_3_4_49_2","first-page":"411","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"Ouaknine J","unstructured":"Ouaknine J, Worrell J. Safety metric temporal logic is fully decidable. In: Hermanns H, Palsberg J (eds) Tools and algorithms for the construction and analysis of systems. Berlin: Springer, pp. 411\u2013425."},{"key":"e_1_3_4_50_2","first-page":"1","volume-title":"Proceedings of the 6th international conference on formal modeling and analysis of timed systems, FORMATS \u201908","author":"Ouaknine J","unstructured":"Ouaknine J, Worrell J. Some recent results in metric temporal logic. In: Proceedings of the 6th international conference on formal modeling and analysis of timed systems, FORMATS \u201908, Saint Malo, 15\u201317 September 2008. Berlin: Springer, pp. 1\u201313."},{"key":"e_1_3_4_51_2","first-page":"263","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"Aceto L","unstructured":"Aceto L, Burgue\u00f1o A, Larsen KG. Model checking via reachability testing for timed automata. In: Steffen B (ed.) Tools and algorithms for the construction and analysis of systems (Lecture notes in computer science), Vol. 1384. New York: Springer, pp. 263\u2013280."},{"key":"e_1_3_4_52_2","first-page":"94","volume-title":"Computer aided verification","author":"Beer I","unstructured":"Beer I, Ben-David S, Chockler H, et al. Explaining counterexamples using causality. In: Bouajjani A, Maler O (eds) Computer aided verification. Berlin: Springer, pp. 94\u2013108."},{"key":"e_1_3_4_53_2","unstructured":"Debbi H. Counterexamples in model checking\u2014a survey. Informatica 2018; 42 https:\/\/api.semanticscholar.org\/CorpusID:51874797"},{"key":"e_1_3_4_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2021.106800"},{"key":"e_1_3_4_55_2","first-page":"288","volume-title":"International conference on tools and algorithms for the construction and analysis of systems","author":"Lima L","unstructured":"Lima L, Huerta y, Munive JJ, Traytel D. Explainable online monitoring of metric first-order temporal logic. In: International conference on tools and algorithms for the construction and analysis of systems, Hamilton, ON, Canada, 3\u20138 May. New York: Springer, pp. 288\u2013307."},{"key":"e_1_3_4_56_2","first-page":"178","volume-title":"Runtime verification","author":"Ho HM","unstructured":"Ho HM, Ouaknine J, Worrell J. Online monitoring of metric temporal logic. In: Bonakdarpour B, Smolka SA (eds) Runtime verification. Cham: Springer, pp. 178\u2013192."},{"key":"e_1_3_4_57_2","doi-asserted-by":"crossref","unstructured":"Gunadi H Tiu A. Efficient runtime monitoring with metric temporal logic: a case study in the android operating system. arXiv:1311.2362 2013 https:\/\/api.semanticscholar.org\/CorpusID:17902855","DOI":"10.1007\/978-3-319-06410-9_21"},{"volume-title":"Formal modeling and analysis of timed systems: 20th international conference, FORMATS 2022","author":"Bouyer P","key":"e_1_3_4_58_2","unstructured":"Bouyer P, Gastin P, Herbreteau F, et al. Zone-based verification of timed automata: extrapolations, simulations and what next. In: Formal modeling and analysis of timed systems: 20th international conference, FORMATS 2022, Warsaw, 13\u201315 September 2022. Berlin: Springer."},{"key":"e_1_3_4_59_2","first-page":"3","volume-title":"Formal techniques in real-time and fault-tolerant systems","author":"Behrmann G","unstructured":"Behrmann G, Bengtsson J, David A, et al. Uppaal implementation secrets. In: Vytopil J (ed.) Formal techniques in real-time and fault-tolerant systems. Berlin: Springer, pp. 3\u201322."},{"key":"e_1_3_4_60_2","first-page":"281","volume-title":"Proceedings of the 4th international conference on tools and algorithms for construction and analysis of systems, TACAS \u201998","author":"Lindahl M","unstructured":"Lindahl M, Pettersson P, Yi W. Formal design and analysis of a gear controller. In: Proceedings of the 4th international conference on tools and algorithms for construction and analysis of systems, TACAS \u201998, Lisbon, 28 March\u20134 April, pp. 281\u2013297. Berlin: Springer."},{"key":"e_1_3_4_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050032"},{"key":"e_1_3_4_62_2","first-page":"357","volume-title":"Modelling and verification of web services business activity protocol","author":"Ravn AP","unstructured":"Ravn AP, Srba J, Vighio S. Modelling and verification of web services business activity protocol. In: Abdulla PA, Leino KRM (eds) Modelling and verification of web services business activity protocol. Berlin: Springer, pp. 357\u2013371."},{"volume-title":"2021 26th IEEE international conference on emerging technologies and factory automation (ETFA)","author":"Bakhshi Z","key":"e_1_3_4_63_2","unstructured":"Bakhshi Z, Rodriguez- Navas G, Hansson H. Using UPPAAL to verify recovery in a fault-tolerant mechanism providing persistent state at the edge. In: 2021 26th IEEE international conference on emerging technologies and factory automation (ETFA), Vasteras, 7\u201310 September 2021. New York: IEEE."},{"key":"e_1_3_4_64_2","unstructured":"OMG. Meta object facility (MOF) 2.0 query\/view\/transformation specification version 1.1 2011 http:\/\/www.omg.org\/spec\/QVT\/1.1\/"},{"key":"e_1_3_4_65_2","unstructured":"ATL Transformation Language. ATL\u2014a model transformation technology May 2015 http:\/\/www.eclipse.org\/atl"}],"container-title":["SIMULATION"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/00375497251340070","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.1177\/00375497251340070","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/00375497251340070","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T19:38:47Z","timestamp":1759693127000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.1177\/00375497251340070"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,4]]},"references-count":64,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2025,10]]}},"alternative-id":["10.1177\/00375497251340070"],"URL":"https:\/\/doi.org\/10.1177\/00375497251340070","relation":{},"ISSN":["0037-5497","1741-3133"],"issn-type":[{"type":"print","value":"0037-5497"},{"type":"electronic","value":"1741-3133"}],"subject":[],"published":{"date-parts":[[2025,7,4]]}}}