{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:54:19Z","timestamp":1791460459055,"version":"4.3.4"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,8,29]],"date-time":"2018-08-29T00:00:00Z","timestamp":1535500800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Jiangxi Province Major Project","award":["20171ACE50025"],"award-info":[{"award-number":["20171ACE50025"]}]},{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"crossref","award":["61303014, 61202010 and 91218302"],"award-info":[{"award-number":["61303014, 61202010 and 91218302"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS 13-30077, 13-29886 and 15-45002"],"award-info":[{"award-number":["CNS 13-30077, 13-29886 and 15-45002"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2019,1,31]]},"abstract":"<jats:p>Simulink is widely used for model-driven development (MDD) of cyber-physical systems. Typically, the Simulink-based development starts with Stateflow modeling, followed by simulation, validation, and code generation mapped to physical execution platforms. However, recent trends have raised the demands of rigorous verification on safety-critical applications to prevent intrinsic development faults and improve the system dependability, which is unfortunately challenging. Even though the constructed Stateflow model and the generated code pass the validation of Simulink Design Verifier and Simulink Polyspace, respectively, the system may still fail due to some implicit defects contained in the design model (design defect) and the generated code (implementation defects).<\/jats:p>\n                  <jats:p>In this article, we bridge the Stateflow-based MDD and a well-defined rigorous verification to reduce development faults. First, we develop a self-contained toolkit to translate a Stateflow model into timed automata, where major advanced modeling features in Stateflow are supported. Taking advantage of the strong verification capability of Uppaal, we can not only find bugs in Stateflow models that are missed by Simulink Design Verifier but also check more important temporal properties. Next, we customize a runtime verifier for the generated non-intrusive VHDL and C code of a Stateflow model for monitoring. The major strength of the customization is the flexibility to collect and analyze runtime properties with a pure software monitor, which offers more opportunities for engineers to achieve high reliability of the target system compared with the traditional act that only relies on Simulink Polyspace. In this way, safety-critical properties are both verified at the model level and at the consistent system implementation level with physical execution environment in consideration. We apply our approach to the development of a typical cyber-physical system-train communication controller based on the IEC standard 61375. Experiments show that more ambiguousness in the standard are detected and confirmed and more development faults and those corresponding errors that would lead to system failure have been removed. Furthermore, the verified implementation has been deployed on real trains.<\/jats:p>","DOI":"10.1145\/3078623","type":"journal-article","created":{"date-parts":[[2018,8,30]],"date-time":"2018-08-30T09:45:11Z","timestamp":1535622311000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["Dependable Model-driven Development of CPS"],"prefix":"10.1145","volume":"3","author":[{"given":"Yu","family":"Jiang","sequence":"first","affiliation":[{"name":"Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Houbing","family":"Song","sequence":"additional","affiliation":[{"name":"Embry-Riddle Aeronautical University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yixiao","family":"Yang","sequence":"additional","affiliation":[{"name":"Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Han","family":"Liu","sequence":"additional","affiliation":[{"name":"Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ming","family":"Gu","sequence":"additional","affiliation":[{"name":"Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[{"name":"Capital Normal University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jiaguang","family":"Sun","sequence":"additional","affiliation":[{"name":"Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lui","family":"Sha","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, IL"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,8,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Syed Hassan Ahmed Gwanghyeon Kim and Dongkyun Kim. 2013. Cyber physical system: Architecture applications and research challenges. In Wireless Days. 1--5. Syed Hassan Ahmed Gwanghyeon Kim and Dongkyun Kim. 2013. Cyber physical system: Architecture applications and research challenges. In Wireless Days. 1--5.","DOI":"10.1109\/WD.2013.6686528"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/647768.733787"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1450058.1450071"},{"key":"e_1_2_1_4_1","volume-title":"Building the Information Society","author":"Avi\u017eienis Algirdas","unstructured":"Algirdas Avi\u017eienis , Jean-Claude Laprie , and Brian Randell . 2004. Dependability and its threats: A taxonomy . In Building the Information Society . Springer , 91--120. Algirdas Avi\u017eienis, Jean-Claude Laprie, and Brian Randell. 2004. Dependability and its threats: A taxonomy. In Building the Information Society. Springer, 91--120."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2004.2"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10702-8_9"},{"key":"e_1_2_1_7_1","volume-title":"Larsen","author":"Behrmann Gerd","year":"2004","unstructured":"Gerd Behrmann , Alexandre David , and Kim G . Larsen . 2004 . A tutorial on uppaal. In Formal Methods for the Design of Real-time Systems. Springer , 200--236. Gerd Behrmann, Alexandre David, and Kim G. Larsen. 2004. A tutorial on uppaal. In Formal Methods for the Design of Real-time Systems. Springer, 200--236."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1793603.1793606"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 11th Conference on Computer Assurance, Systems Integrity, Software Safety, and Process Security (Compass\u201996)","author":"Blackburn M. R.","unstructured":"M. R. Blackburn and R. D. Busser . 1996. T-VEC: A tool for developing critical systems . In Proceedings of the 11th Conference on Computer Assurance, Systems Integrity, Software Safety, and Process Security (Compass\u201996) . 237--249. M. R. Blackburn and R. D. Busser. 1996. T-VEC: A tool for developing critical systems. In Proceedings of the 11th Conference on Computer Assurance, Systems Integrity, Software Safety, and Process Security (Compass\u201996). 237--249."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/646732.701281"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/780731.780754"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0235-0"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_36"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297105.1297069"},{"key":"e_1_2_1_15_1","volume-title":"Transactions on","author":"Douence R\u00e9mi","unstructured":"R\u00e9mi Douence , Thomas Fritz , Nicolas Loriant , Jean-Marc Menaud , Marc S\u00e9gura-Devillechaise , and Mario S\u00fcdholt . 2006. An expressive aspect language for system applications with Arachne . In Transactions on Aspect-Oriented Software Development I. Springer , 174--213. R\u00e9mi Douence, Thomas Fritz, Nicolas Loriant, Jean-Marc Menaud, Marc S\u00e9gura-Devillechaise, and Mario S\u00fcdholt. 2006. An expressive aspect language for system applications with Arachne. In Transactions on Aspect-Oriented Software Development I. Springer, 174--213."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_19"},{"key":"e_1_2_1_17_1","unstructured":"S. Jeschke H. Song D. Rawat and C. Brecher. 2016. Cyber-Physical Systems: Foundations Principles and Applications. S. Jeschke H. Song D. Rawat and C. Brecher. 2016. Cyber-Physical Systems: Foundations Principles and Applications."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68524-1_3"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2889160.2889233"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_47"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2016.7461337"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIE.2014.2316234"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2013.89"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIE.2012.2225393"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2014.2346171"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/646158.680006"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664573"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"e_1_2_1_30_1","unstructured":"The MathWorks. 2017a. SimulinkDesignVerifier. Retrieved from http:\/\/www.mathworks.com. The MathWorks. 2017a. SimulinkDesignVerifier. Retrieved from http:\/\/www.mathworks.com."},{"key":"e_1_2_1_31_1","unstructured":"The MathWorks. 2017b. SimulinkPolySpace. Retrieved from http:\/\/www.mathworks.com. The MathWorks. 2017b. SimulinkPolySpace. Retrieved from http:\/\/www.mathworks.com."},{"key":"e_1_2_1_32_1","unstructured":"The MathWorks. 2017c. Stateflow user guide. Retrieved from http:\/\/www.mathworks.com. The MathWorks. 2017c. Stateflow user guide. Retrieved from http:\/\/www.mathworks.com."},{"key":"e_1_2_1_33_1","volume-title":"The SMV System","author":"Mcmillan Kenneth L.","unstructured":"Kenneth L. Mcmillan . 1993. The SMV System . Springer US. 161--165. Kenneth L. Mcmillan. 1993. The SMV System. Springer US. 161--165."},{"key":"e_1_2_1_34_1","volume-title":"Syed Hassan Ahmed, and Mahasweta Sarkar","author":"Mehmood Amjad","year":"2017","unstructured":"Amjad Mehmood , Syed Hassan Ahmed, and Mahasweta Sarkar . 2017 . Cyber-Physical Systems in Vehicular Communications . Amjad Mehmood, Syed Hassan Ahmed, and Mahasweta Sarkar. 2017. Cyber-Physical Systems in Vehicular Communications."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2012.25"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2584651"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2008.43"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 2015 IEEE\/ACM 1st International Workshop on Complex Faults and Failures in Large Software Systems (COUFLESS\u201915)","author":"Qian J.","unstructured":"J. Qian , J. Liu , X. Chen , and J. Sun . 2015. Modeling and verification of zone controller: The SCADE experience in china\u2019s railway systems . In Proceedings of the 2015 IEEE\/ACM 1st International Workshop on Complex Faults and Failures in Large Software Systems (COUFLESS\u201915) . 48--54. J. Qian, J. Liu, X. Chen, and J. Sun. 2015. Modeling and verification of zone controller: The SCADE experience in china\u2019s railway systems. In Proceedings of the 2015 IEEE\/ACM 1st International Workshop on Complex Faults and Failures in Large Software Systems (COUFLESS\u201915). 48--54."},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the IEEE 51st Vehicular Technology Conference Proceedings (VTC\u201900)","volume":"2","author":"Schifers C.","unstructured":"C. Schifers and G. Hans . 2000. IEC 61375-1 and UIC 556-international standards for train communication . In Proceedings of the IEEE 51st Vehicular Technology Conference Proceedings (VTC\u201900) , Vol. 2 . 1581--1585. C. Schifers and G. Hans. 2000. IEC 61375-1 and UIC 556-international standards for train communication. In Proceedings of the IEEE 51st Vehicular Technology Conference Proceedings (VTC\u201900), Vol. 2. 1581--1585."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2001.936213"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291220.1291172"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"e_1_2_1_43_1","unstructured":"Tester. 2017. Applied dynamics international. Retrieved from http:\/\/www.adi.com. Tester. 2017. Applied dynamics international. Retrieved from http:\/\/www.adi.com."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1175\/2008MWR2415.1"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970293"},{"key":"e_1_2_1_46_1","unstructured":"Yu. 2017. Uiuc. Retrieved from https:\/\/sites.google.com\/site\/jiangyu198964\/home. Yu. 2017. Uiuc. Retrieved from https:\/\/sites.google.com\/site\/jiangyu198964\/home."}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3078623","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3078623","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3078623","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T14:18:12Z","timestamp":1751811492000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3078623"}},"subtitle":["From Stateflow Simulation to Verified Implementation"],"short-title":[],"issued":{"date-parts":[[2018,8,29]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,1,31]]}},"alternative-id":["10.1145\/3078623"],"URL":"https:\/\/doi.org\/10.1145\/3078623","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,8,29]]},"assertion":[{"value":"2017-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-08-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}