{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T02:20:21Z","timestamp":1779330021883,"version":"3.51.4"},"reference-count":47,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2011,10,23]],"date-time":"2011-10-23T00:00:00Z","timestamp":1319328000000},"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":[[2013,1]]},"abstract":"<jats:p>Real-time systems modeling and verification is a complex task. In many cases, formal methods have been employed to deal with the complexity of these systems, but checking those models is usually unfeasible. Modeling and simulation methods introduce a means of validating these model\u2019s specifications. In particular, Discrete Event System Specification (DEVS) models can be used for this purpose. Here, we introduce a new extension to the DEVS formalism, called the Rational Time-Advance DEVS (RTA-DEVS), which permits modeling the behavior of real-time systems that can be modeled by the classical DEVS; however, RTA-DEVS models can be formally checked with standard model-checking algorithms and tools. In order to do so, we introduce a procedure to create timed automata (TA) models that are behaviorally equivalent to the original RTA-DEVS models. This enables the use of the available TA tools and theories for formal model checking. Further, we introduce a methodology to transform classic DEVS models to RTA-DEVS models, thus enabling formal verification of classic DEVS with an acceptable accuracy.<\/jats:p>","DOI":"10.1177\/0037549711424424","type":"journal-article","created":{"date-parts":[[2011,10,24]],"date-time":"2011-10-24T20:25:19Z","timestamp":1319487919000},"page":"41-67","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":14,"title":["Principles of Discrete Event System Specification model verification"],"prefix":"10.1177","volume":"89","author":[{"given":"Hesham","family":"Saadawi","sequence":"first","affiliation":[{"name":"School of Computer Science, Carleton University, Ottawa, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriel","family":"Wainer","sequence":"additional","affiliation":[{"name":"Department of Systems and Computer Engineering, Carleton University, Ottawa, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2011,10,23]]},"reference":[{"key":"bibr1-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.357"},{"key":"bibr2-0037549711424424","volume-title":"Proceedings of the 2nd international Workshop on Random Testing: Co-Located with the 22nd IEEE\/ACM international Conference on Automated Software Engineering (ASE 2007)","author":"Gerlich R"},{"key":"bibr3-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1177\/0037549709102850"},{"key":"bibr4-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1177\/0037549709104482"},{"key":"bibr5-0037549711424424","first-page":"120","volume-title":"Proceedings of the 2007 Future of Software Engineering (FOSE \u201907)","author":"Dwyer MB"},{"key":"bibr6-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"bibr7-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1177\/0037549709345997"},{"key":"bibr8-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1177\/0037549710373909"},{"key":"bibr9-0037549711424424","volume-title":"Theory of modeling and simulation: integrating discrete event and continuous complex dynamic systems","author":"Zeigler B","year":"2000","edition":"2"},{"key":"bibr10-0037549711424424","first-page":"33","volume-title":"Proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT\u201904), Formal Methods for the Design of Real-Time Systems 2004","volume":"3185","author":"Behrmann G"},{"key":"bibr11-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"bibr12-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1201\/9781420053371"},{"key":"bibr13-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1002\/spe.482"},{"key":"bibr14-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1177\/0037549710395649"},{"key":"bibr15-0037549711424424","volume-title":"Proceedings of MGA, Advanced Simulation Technologies Conference","author":"Christen G"},{"key":"bibr16-0037549711424424","first-page":"595","volume-title":"WSC\u201993: Proceedings of the 25th Conference on Winter Simulation","author":"Praehofer H"},{"key":"bibr17-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1177\/0037549710368029"},{"key":"bibr18-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1177\/0037549705052229"},{"key":"bibr19-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1201\/b10412-13"},{"key":"bibr20-0037549711424424","first-page":"163","volume":"25","author":"Pace DK","year":"2004","journal-title":"Johns Hopkins APL Tech Digest"},{"key":"bibr21-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1049\/ip-sen:20041006"},{"key":"bibr22-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-007-9013-6"},{"key":"bibr23-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.105"},{"key":"bibr24-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1177\/0037549710364204"},{"key":"bibr25-0037549711424424","first-page":"312","volume-title":"Proceedings of the 2007 Summer Computer Simulation Conference","author":"Dacharry HP"},{"key":"bibr26-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008262409521"},{"key":"bibr27-0037549711424424","first-page":"601","volume-title":"Proceedings of Computer Science and Information Technology (IMCSIT 2008)","author":"Furfaro A"},{"key":"bibr28-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-009-0085-4"},{"key":"bibr29-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2009.2021352"},{"key":"bibr30-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72584-8_162"},{"key":"bibr31-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1109\/WSC.2003.1261512"},{"key":"bibr32-0037549711424424","first-page":"267","volume-title":"Proceedings of Argentine Symposium on Software Engineering","author":"Hern\u00e1ndez A","year":"2005"},{"key":"bibr33-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30583-5_30"},{"key":"bibr34-0037549711424424","first-page":"295","volume-title":"Proceedings of the 1st Open International Conference on Modeling & Simulation","author":"Labiche Y","year":"2005"},{"key":"bibr35-0037549711424424","volume-title":"Proceedings of SpringSim\u201909","author":"Saadawi H"},{"key":"bibr36-0037549711424424","volume-title":"Proceedings of 2010 Symposium on Theory of Modeling and Simulation (DEVS\u201910)","author":"Saadawi H"},{"key":"bibr37-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46430-1_26"},{"key":"bibr38-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814105"},{"key":"bibr39-0037549711424424","volume-title":"Concurrency theory: calculi and automata for modelling untimed and timed concurrent systems","author":"Bowman H","year":"2006","edition":"1"},{"key":"bibr40-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014736"},{"key":"bibr41-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_20"},{"key":"bibr42-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008387132377"},{"key":"bibr43-0037549711424424","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_10"},{"key":"bibr44-0037549711424424","first-page":"323","volume-title":"Proceedings of the 2007 Summer Computer Simulation Conference","author":"Yu YH"},{"key":"bibr45-0037549711424424","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1998-36233"},{"key":"bibr46-0037549711424424","first-page":"393","volume":"10","author":"Bouyer P","year":"2005","journal-title":"J Automata Lang Combinatorics"},{"key":"bibr47-0037549711424424","unstructured":"Wikipedia. \u2018DEVS Behavior\u2019, http:\/\/en.wikipedia.org\/wiki\/Behavior_of_Coupled_DEVS (accessed August 2009)."}],"container-title":["SIMULATION"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0037549711424424","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.1177\/0037549711424424","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0037549711424424","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T11:23:27Z","timestamp":1777634607000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.1177\/0037549711424424"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,10,23]]},"references-count":47,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["10.1177\/0037549711424424"],"URL":"https:\/\/doi.org\/10.1177\/0037549711424424","relation":{},"ISSN":["0037-5497","1741-3133"],"issn-type":[{"value":"0037-5497","type":"print"},{"value":"1741-3133","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,10,23]]}}}