{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T06:56:56Z","timestamp":1760597816501,"version":"3.41.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2018,7,5]],"date-time":"2018-07-05T00:00:00Z","timestamp":1530748800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Air Force Office of Scientific Research (AFOSR) through AFOSR's Summer Faculty Fellowship Program","award":["FA9550-15-F-0001, FA9550-15-1-0258 and FA9550-16-1-0246"],"award-info":[{"award-number":["FA9550-15-F-0001, FA9550-15-1-0258 and FA9550-16-1-0246"]}]},{"name":"Air Force Research Laboratory (AFRL) through the AFRL's Visiting Faculty Research Program","award":["FA8750-13-2-0115, FA8750-15-1-0105, FA8650-12-3-7255 and WBSC 7255 SOI VU 0001"],"award-info":[{"award-number":["FA8750-13-2-0115, FA8750-15-1-0105, FA8650-12-3-7255 and WBSC 7255 SOI VU 0001"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS 1464311, CNS 1713253, EPCN 1509804, SHF 1527398 and SHF 1736323"],"award-info":[{"award-number":["CNS 1464311, CNS 1713253, EPCN 1509804, SHF 1527398 and SHF 1736323"]}],"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":[[2018,10,31]]},"abstract":"<jats:p>Embedded systems use increasingly complex software and are evolving into cyber-physical systems (CPS) with sophisticated interaction and coupling between physical and computational processes. Many CPS operate in safety-critical environments and have stringent certification, reliability, and correctness requirements. These systems undergo changes throughout their lifetimes, where either the software or physical hardware is updated in subsequent design iterations. One source of failure in safety-critical CPS is when there are unstated assumptions in either the physical or cyber parts of the system, and new components do not match those assumptions. In this work, we present an automated method toward identifying unstated assumptions in CPS. Dynamic specifications in the form of candidate invariants of both the software and physical components are identified using dynamic analysis (executing and\/or simulating the system implementation or model thereof). A prototype tool called Hynger (for HYbrid iNvariant GEneratoR) was developed that instruments Simulink\/Stateflow (SLSF) model diagrams to generate traces in the input format compatible with the Daikon invariant inference tool, which has been extensively applied to software systems. Hynger, in conjunction with Daikon, is able to detect candidate invariants of several CPS case studies. We use the running example of a DC-to-DC power converter and demonstrate that Hynger can detect a specification mismatch where a tolerance assumed by the software is violated due to a plant change. Another case study of an automotive control system is also introduced to illustrate the power of Hynger and Daikon in automatically identifying cyber-physical specification mismatches.<\/jats:p>","DOI":"10.1145\/3170500","type":"journal-article","created":{"date-parts":[[2018,7,5]],"date-time":"2018-07-05T19:19:10Z","timestamp":1530818350000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Cyber-Physical Specification Mismatches"],"prefix":"10.1145","volume":"2","author":[{"given":"Luan V.","family":"Nguyen","sequence":"first","affiliation":[{"name":"University of Texas at Arlington, Philadelphia, PA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1625-6479","authenticated-orcid":false,"given":"Khaza Anuarul","family":"Hoque","sequence":"additional","affiliation":[{"name":"University of Oxford, Naka Hall, Columbia, MO"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stanley","family":"Bak","sequence":"additional","affiliation":[{"name":"Air Force Research Laboratory, Rome, NY"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven","family":"Drager","sequence":"additional","affiliation":[{"name":"Air Force Research Laboratory, Rome, NY"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[{"name":"Vanderbilt University, Nashville, TN"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,7,5]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Report by the Inquiry Board","author":"Failure ARIANE","year":"1996","unstructured":"ARIANE 5 Flight 501 Failure , Report by the Inquiry Board . 1996 . Technical report. ESA Inquiry Board, Paris, France. Retrieved from https:\/\/www.ima.umn.edu\/ arnold\/disasters\/ariane5rep.html. ARIANE 5 Flight 501 Failure, Report by the Inquiry Board. 1996. Technical report. ESA Inquiry Board, Paris, France. Retrieved from https:\/\/www.ima.umn.edu\/ arnold\/disasters\/ariane5rep.html."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2013.49"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805817"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1450058.1450071"},{"key":"e_1_2_1_5_1","volume-title":"S-taliro: A tool for temporal logic falsification for hybrid systems. In Tools and Algorithms for the Construction and Analysis of Systems","author":"Annpureddy Yashwanth","year":"2011","unstructured":"Yashwanth Annpureddy , Che Liu , Georgios Fainekos , and Sriram Sankaranarayanan . 2011 . S-taliro: A tool for temporal logic falsification for hybrid systems. In Tools and Algorithms for the Construction and Analysis of Systems . Springer . Yashwanth Annpureddy, Che Liu, Georgios Fainekos, and Sriram Sankaranarayanan. 2011. S-taliro: A tool for temporal logic falsification for hybrid systems. In Tools and Algorithms for the Construction and Analysis of Systems. Springer."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2014.21"},{"key":"e_1_2_1_7_1","unstructured":"Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The SMT-LIB standard: Version 2.0. Retrieved from http:\/\/smt-lib.org\/.  Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The SMT-LIB standard: Version 2.0. Retrieved from http:\/\/smt-lib.org\/."},{"key":"e_1_2_1_8_1","volume-title":"Software Testing Techniques","author":"Beizer Boris","unstructured":"Boris Beizer . 1990. Software Testing Techniques ( 2 nd ed.) . Van Nostrand Reinhold Co. , New York, NY . Boris Beizer. 1990. Software Testing Techniques (2nd ed.) . Van Nostrand Reinhold Co., New York, NY.","edition":"2"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-014-0410-8"},{"key":"e_1_2_1_10_1","volume-title":"Francisco Jose Romero-Campero, and Neil Walkinshaw","author":"Bernardini Francesco","year":"2007","unstructured":"Francesco Bernardini , Marian Gheorghe , Francisco Jose Romero-Campero, and Neil Walkinshaw . 2007 . A hybrid approach to modeling biological systems. In Membrane Computing, George Eleftherakis, Petros Kefalas, Gheorghe Paun, Grzegorz Rozenberg, and Arto Salomaa (Eds.). LNCS, Vol. 4860 . Springer , Berlin, 138--159. Francesco Bernardini, Marian Gheorghe, Francisco Jose Romero-Campero, and Neil Walkinshaw. 2007. A hybrid approach to modeling biological systems. In Membrane Computing, George Eleftherakis, Petros Kefalas, Gheorghe Paun, Grzegorz Rozenberg, and Arto Salomaa (Eds.). LNCS, Vol. 4860. Springer, Berlin, 138--159."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146258"},{"key":"e_1_2_1_12_1","unstructured":"Consumer Product Safety Commission. 2010. Fire alarm control panels recalled by Fire-Lite Alarms due to alert failure (alert no. 11-702). Retrieved from http:\/\/www.cpsc.gov\/en\/Recalls\/2011\/Fire-Alarm-Control-Panels-Recalled-by-Fire-Lite-Alarms-Due-to-Alert-Failure\/.  Consumer Product Safety Commission. 2010. Fire alarm control panels recalled by Fire-Lite Alarms due to alert failure (alert no. 11-702). Retrieved from http:\/\/www.cpsc.gov\/en\/Recalls\/2011\/Fire-Alarm-Control-Panels-Recalled-by-Fire-Lite-Alarms-Due-to-Alert-Failure\/."},{"key":"e_1_2_1_13_1","unstructured":"Consumer Product Safety Commission. 2011. Simplex fire alarm control panels recalled by Tyco Safety Products Westminster due to failure to alert monitoring centers (alert no. 11-721). Retrieved from http:\/\/www.cpsc.gov\/en\/Recalls\/2011\/Simplex-Fire-Alarm-Control-Panels-Recalled-by-Tyco-Safety-Products-Westminster-Due-to-Failure-to-Alert-Monitoring-Centers\/.  Consumer Product Safety Commission. 2011. Simplex fire alarm control panels recalled by Tyco Safety Products Westminster due to failure to alert monitoring centers (alert no. 11-721). Retrieved from http:\/\/www.cpsc.gov\/en\/Recalls\/2011\/Simplex-Fire-Alarm-Control-Panels-Recalled-by-Tyco-Safety-Products-Westminster-Due-to-Failure-to-Alert-Monitoring-Centers\/."},{"key":"e_1_2_1_14_1","unstructured":"Consumer Product Safety Commission. 2012. Fire control panels recalled by Bosch Security Systems Corp. due to alarm failure posing a fire hazard (alert no. 12-721). Retrieved from http:\/\/www.cpsc.gov\/en\/Recalls\/2012\/Fire-Control-Panels-Recalled-by-Bosch-Security-Systems-Corp-Due-to-Alarm-Failure-Posing-a-Fire-Hazard\/.  Consumer Product Safety Commission. 2012. Fire control panels recalled by Bosch Security Systems Corp. due to alarm failure posing a fire hazard (alert no. 12-721). Retrieved from http:\/\/www.cpsc.gov\/en\/Recalls\/2012\/Fire-Control-Panels-Recalled-by-Bosch-Security-Systems-Corp-Due-to-Alarm-Failure-Posing-a-Fire-Hazard\/."},{"key":"e_1_2_1_15_1","unstructured":"Consumer Product Safety Commission. 2012. Residential elevators recalled for repair by ThyssenKrupp Access Manufacturing due to fall hazard (alert no. 12-750). Retrieved from http:\/\/www.cpsc.gov\/en\/Recalls\/2012\/Residential-Elevators-Recalled-for-Repair-by-ThyssenKrupp-Access-Manufacturing-Due-to-Fall-Hazard\/.  Consumer Product Safety Commission. 2012. Residential elevators recalled for repair by ThyssenKrupp Access Manufacturing due to fall hazard (alert no. 12-750). Retrieved from http:\/\/www.cpsc.gov\/en\/Recalls\/2012\/Residential-Elevators-Recalled-for-Repair-by-ThyssenKrupp-Access-Manufacturing-Due-to-Fall-Hazard\/."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368127"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"e_1_2_1_20_1","volume-title":"Meeting a powertrain verification challenge. In International Conference on Computer Aided Verification. Springer, 536--543","author":"Duggirala Parasara Sridhar","year":"2015","unstructured":"Parasara Sridhar Duggirala , Chuchu Fan , Sayan Mitra , and Mahesh Viswanathan . 2015 . Meeting a powertrain verification challenge. In International Conference on Computer Aided Verification. Springer, 536--543 . Parasara Sridhar Duggirala, Chuchu Fan, Sayan Mitra, and Mahesh Viswanathan. 2015. Meeting a powertrain verification challenge. In International Conference on Computer Aided Verification. Springer, 536--543."},{"key":"e_1_2_1_21_1","volume-title":"Erickson and Dragan Maksimovi\u0107","author":"Robert","year":"2004","unstructured":"Robert W. Erickson and Dragan Maksimovi\u0107 . 2004 . Fundamentals of Power Electronics (2nd ed.). Springer . Robert W. Erickson and Dragan Maksimovi\u0107. 2004. Fundamentals of Power Electronics (2nd ed.). Springer."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 2nd Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH\u201915)","author":"Fan Chuchu","year":"2015","unstructured":"Chuchu Fan , Parasara Sridhar Duggirala , Sayan Mitra , and Mahesh Viswanathan . 2015 . Progress on powertrain verification challenge with C2E2 . In Proceedings of the 2nd Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH\u201915) . Chuchu Fan, Parasara Sridhar Duggirala, Sayan Mitra, and Mahesh Viswanathan. 2015. Progress on powertrain verification challenge with C2E2. In Proceedings of the 2nd Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH\u201915)."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032335"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/225014.225031"},{"volume-title":"Proceedings of the Power and Energy Conference at Illinois (PECI\u201913)","author":"Hossain Shamina","key":"e_1_2_1_27_1","unstructured":"Shamina Hossain , Sairaj Dhople , and Taylor T. Johnson . 2013. Reachability analysis of closed-loop switching power converters . In Proceedings of the Power and Energy Conference at Illinois (PECI\u201913) . 130--134. Shamina Hossain, Sairaj Dhople, and Taylor T. Johnson. 2013. Reachability analysis of closed-loop switching power converters. In Proceedings of the Power and Energy Conference at Illinois (PECI\u201913). 130--134."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 1st International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH\u201914)","author":"Jin Xiaoqing","year":"2014","unstructured":"Xiaoqing Jin , Jyotirmoy V. Deshmukh , James Kapinski , Koichi Ueda , and Ken Butts . 2014 . Benchmarks for model transformations and conformance checking . In Proceedings of the 1st International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH\u201914) . Xiaoqing Jin, Jyotirmoy V. Deshmukh, James Kapinski, Koichi Ueda, and Ken Butts. 2014. Benchmarks for model transformations and conformance checking. In Proceedings of the 1st International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH\u201914)."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461337"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2735960.2735979"},{"volume-title":"Proceedings of the Power and Energy Conference at Illinois (PECI\u201912)","author":"Johnson Taylor T.","key":"e_1_2_1_31_1","unstructured":"Taylor T. Johnson , Zhihao Hong , and A. Kapoor . 2012. Design verification methods for switching power converters . In Proceedings of the Power and Energy Conference at Illinois (PECI\u201912) . IEEE. 1--6. Taylor T. Johnson, Zhihao Hong, and A. Kapoor. 2012. Design verification methods for switching power converters. In Proceedings of the Power and Energy Conference at Illinois (PECI\u201912). IEEE. 1--6."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_33"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 17th IEEE Instrumentation and Measurement Technology Conference (IMTC\u201900)","volume":"2","author":"Lee Kang","year":"2000","unstructured":"Kang Lee . 2000 . IEEE 1451: A standard in support of smart transducer networking . In Proceedings of the 17th IEEE Instrumentation and Measurement Technology Conference (IMTC\u201900) , Vol. 2 . IEEE, 525--528. Kang Lee. 2000. IEEE 1451: A standard in support of smart transducer networking. In Proceedings of the 17th IEEE Instrumentation and Measurement Technology Conference (IMTC\u201900), Vol. 2. IEEE, 525--528."},{"volume-title":"System safety engineering: Back to the future","author":"Leveson Nancy G.","key":"e_1_2_1_34_1","unstructured":"Nancy G. Leveson . 2002. System safety engineering: Back to the future . Massachusetts Institute of Technology . Nancy G. Leveson. 2002. System safety engineering: Back to the future. Massachusetts Institute of Technology."},{"volume-title":"Ariane 5 Flight 501 Failure","author":"Lions J. L.","key":"e_1_2_1_35_1","unstructured":"J. L. Lions . 1996. Ariane 5 Flight 501 Failure . Technical Report. Paris, France . Retrieved from http:\/\/www.di.unito.it\/ damiani\/ariane5rep.html. J. L. Lions. 1996. Ariane 5 Flight 501 Failure. Technical Report. Paris, France. Retrieved from http:\/\/www.di.unito.it\/ damiani\/ariane5rep.html."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00067-1"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967749"},{"key":"e_1_2_1_38_1","unstructured":"Kevin McCaney. 2014. Pentagon\u2019s rapid plan for maintaining air superiority. Retrieved from http:\/\/defensesystems.com\/Articles\/2014\/05\/01\/DARPA-system-of-systems-SoSITE.aspx.  Kevin McCaney. 2014. Pentagon\u2019s rapid plan for maintaining air superiority. Retrieved from http:\/\/defensesystems.com\/Articles\/2014\/05\/01\/DARPA-system-of-systems-SoSITE.aspx."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/2830865.2830885"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883826"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10452-7_3"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.4108\/eai.22-7-2015.2260045"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2014.6843717"},{"key":"e_1_2_1_44_1","unstructured":"National Highway Traffic Safety Administration (NHTSA). 2005. Action no. PE05029. Retrieved from http:\/\/www-odi.nhtsa.dot.gov\/cars\/problems\/defect\/results.cfm?action_number&equals;PE050298SearchType&equals;QuickSearch8summary&equals;true.  National Highway Traffic Safety Administration (NHTSA). 2005. Action no. PE05029. Retrieved from http:\/\/www-odi.nhtsa.dot.gov\/cars\/problems\/defect\/results.cfm?action_number&equals;PE050298SearchType&equals;QuickSearch8summary&equals;true."},{"key":"e_1_2_1_45_1","unstructured":"National Highway Traffic Safety Administration (NHTSA). 2011. Honda automatic transmission control module software. Recall no. 11V395000. Retrieved from https:\/\/repairpal.com\/recall\/11V395000.  National Highway Traffic Safety Administration (NHTSA). 2011. Honda automatic transmission control module software. Recall no. 11V395000. Retrieved from https:\/\/repairpal.com\/recall\/11V395000."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250746"},{"volume-title":"Proceedings of the Applied Verification for Continuous and Hybrid Systems Workshop (ARCH\u201914)","author":"Nguyen Luan Viet","key":"e_1_2_1_47_1","unstructured":"Luan Viet Nguyen and Taylor T. Johnson . 2014. Benchmark: DC-to-DC switched-mode power converters (buck converters, boost converters, and buck-boost converters) . In Proceedings of the Applied Verification for Continuous and Hybrid Systems Workshop (ARCH\u201914) . Berlin, Germany. Luan Viet Nguyen and Taylor T. Johnson. 2014. Benchmark: DC-to-DC switched-mode power converters (buck converters, boost converters, and buck-boost converters). In Proceedings of the Applied Verification for Continuous and Hybrid Systems Workshop (ARCH\u201914). Berlin, Germany."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127041.3127058"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/TEC.2014.2362716"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337304"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2556782"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568275"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566213"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629585"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2013.30"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.26"},{"key":"e_1_2_1_57_1","volume-title":"Understanding analog to digital converter specifications. Embed. Syst. Design","author":"Staller Len","year":"2005","unstructured":"Len Staller . 2005. Understanding analog to digital converter specifications. Embed. Syst. Design ( 2005 ). https:\/\/www.embedded.com\/design\/configurable-systems\/4025078\/Understanding-analog-to-digital-converter-specifications. Len Staller. 2005. Understanding analog to digital converter specifications. Embed. Syst. Design (2005). https:\/\/www.embedded.com\/design\/configurable-systems\/4025078\/Understanding-analog-to-digital-converter-specifications."},{"key":"e_1_2_1_58_1","unstructured":"Arthur G. Stephenson Daniel R. Mulville Frank H. Bauer Greg A. Dukeman Peter Norvig L. S. LaPiana P. J. Rutledge D. Folta and R. Sackheim. 1999. Mars climate orbiter mishap investigation board Phase I. Technical report. NASA Washington DC.  Arthur G. Stephenson Daniel R. Mulville Frank H. Bauer Greg A. Dukeman Peter Norvig L. S. LaPiana P. J. Rutledge D. Folta and R. Sackheim. 1999. Mars climate orbiter mishap investigation board Phase I. Technical report. NASA Washington DC."},{"key":"e_1_2_1_59_1","volume-title":"Lee","author":"Tripakis Stavros","year":"2013","unstructured":"Stavros Tripakis , Christos Stergiou , Chris Shaver , and Edward A . Lee . 2013 . A modular formal semantics for Ptolemy. Math. Struct. Comput. Sci. 23 (8 2013), 834--881. Issue Special Issue 04. Stavros Tripakis, Christos Stergiou, Chris Shaver, and Edward A. Lee. 2013. A modular formal semantics for Ptolemy. Math. Struct. Comput. Sci. 23 (8 2013), 834--881. Issue Special Issue 04."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2012.173"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-010-0096-1"}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3170500","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3170500","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3170500","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:26:58Z","timestamp":1750213618000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3170500"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,5]]},"references-count":61,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,10,31]]}},"alternative-id":["10.1145\/3170500"],"URL":"https:\/\/doi.org\/10.1145\/3170500","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"type":"print","value":"2378-962X"},{"type":"electronic","value":"2378-9638"}],"subject":[],"published":{"date-parts":[[2018,7,5]]},"assertion":[{"value":"2017-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-07-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}