{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T13:41:17Z","timestamp":1777902077068,"version":"3.51.4"},"reference-count":21,"publisher":"SAGE Publications","issue":"2","license":[{"start":{"date-parts":[[2005,2,1]],"date-time":"2005-02-01T00:00:00Z","timestamp":1107216000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SIMULATION"],"published-print":{"date-parts":[[2005,2]]},"abstract":"<jats:p>This article presents an application of the Discrete Event System Specification (DEVS) framework to the design and safety analysis of a real-time embedded control system, a railroad crossing control system. The authors employ an extension of the DEVS formalism, real-time DEVS (RT-DEVS), which has a sound semantics for the specification of real-time systems in a hierarchical modular fashion. The notion of a clock matrix for communicating RT-DEVS models is proposed, which represents a global time between the models. Based on the composition rules and the clock matrix, an algorithm for the generation of a timed reachability tree is developed that can be used for safety analysis at two phases: an untimed and timed analysis phase. A railroad crossing control example demonstrates that the proposed analysis for RT-DEVS models would be effective to verify the safety property of real-time control systems.<\/jats:p>","DOI":"10.1177\/0037549705052229","type":"journal-article","created":{"date-parts":[[2005,5,18]],"date-time":"2005-05-18T10:09:10Z","timestamp":1116410950000},"page":"119-136","source":"Crossref","is-referenced-by-count":25,"title":["Application of Real-Time DEVS to Analysis of Safety-Critical Embedded Control                 Systems: Railroad Crossing Control Example"],"prefix":"10.1177","volume":"81","author":[{"given":"Hae Sang","family":"Song","sequence":"first","affiliation":[{"name":"Department of Computer Information & Communication, Seowon University, Cheongju, Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tag Gon","family":"Kim","sequence":"additional","affiliation":[{"name":"Department of Electrical Engineering & Computer Science, KAIST, Taejon, Korea,"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2005,2,1]]},"reference":[{"key":"atypb1","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(92)90045-L"},{"key":"atypb2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008262409521"},{"key":"atypb3","doi-asserted-by":"publisher","DOI":"10.1137\/0325013"},{"key":"atypb4","doi-asserted-by":"publisher","DOI":"10.1109\/9.654883"},{"key":"atypb5","doi-asserted-by":"publisher","DOI":"10.1109\/37.56284"},{"key":"atypb6","doi-asserted-by":"publisher","DOI":"10.1137\/S0363012992239600"},{"key":"atypb7","doi-asserted-by":"publisher","DOI":"10.1109\/9.272327"},{"key":"atypb8","doi-asserted-by":"publisher","DOI":"10.1109\/71.80145"},{"key":"atypb9","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"atypb10","doi-asserted-by":"publisher","DOI":"10.1109\/32.846302"},{"key":"atypb11","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805820"},{"key":"atypb12","volume-title":"DEVSim++ user\u2019s manual","author":"Kim, T. G.","year":"1994"},{"issue":"4","key":"atypb13","first-page":"178","volume":"18","author":"Cho, S. M.","year":"2001","journal-title":"Transactions of the Society for Modeling and Simulation International"},{"issue":"1","key":"atypb14","first-page":"19","volume":"13","author":"Hong, G. P.","year":"1996","journal-title":"Transactions of the Society for Computer Simulation International"},{"key":"atypb15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60472-3_27"},{"key":"atypb16","first-page":"228","volume-title":"Proceedings of AI, Simulation and Planning in High Autonomy Systems","author":"Song, H. S."},{"key":"atypb17","volume-title":"Communicating sequential processes","author":"Hoare, C. A. R.","year":"1985"},{"key":"atypb18","volume-title":"Timed reachability analysis of real-time DEVS models using clock matrix","author":"Song, H. S."},{"key":"atypb19","volume-title":"Introduction to interval computations","author":"Alefeld, G.","year":"1983"},{"key":"atypb20","unstructured":"Song, H. S. 2000. A DEVS framework for analysis and design of discrete event                 systems control. Ph.D. diss., KAIST, Taejon, Korea."},{"key":"atypb21","doi-asserted-by":"publisher","DOI":"10.1109\/21.199467"}],"container-title":["SIMULATION"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0037549705052229","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0037549705052229","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T11:19:02Z","timestamp":1777634342000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.1177\/0037549705052229"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,2]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,2]]}},"alternative-id":["10.1177\/0037549705052229"],"URL":"https:\/\/doi.org\/10.1177\/0037549705052229","relation":{},"ISSN":["0037-5497","1741-3133"],"issn-type":[{"value":"0037-5497","type":"print"},{"value":"1741-3133","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,2]]}}}