{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,27]],"date-time":"2026-01-27T11:05:07Z","timestamp":1769511907130,"version":"3.49.0"},"reference-count":110,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2017,12,1]],"date-time":"2017-12-01T00:00:00Z","timestamp":1512086400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS-1239498"],"award-info":[{"award-number":["CNS-1239498"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Systems Journal"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1109\/jsyst.2015.2496293","type":"journal-article","created":{"date-parts":[[2015,11,20]],"date-time":"2015-11-20T20:20:23Z","timestamp":1448050823000},"page":"2614-2627","source":"Crossref","is-referenced-by-count":67,"title":["Perceptions on the State of the Art in Verification and Validation in Cyber-Physical Systems"],"prefix":"10.1109","volume":"11","author":[{"given":"Xi","family":"Zheng","sequence":"first","affiliation":[]},{"given":"Christine","family":"Julien","sequence":"additional","affiliation":[]},{"given":"Miryung","family":"Kim","sequence":"additional","affiliation":[]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/780822.781133"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0244-z"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_9"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"ref30","article-title":"Static verification of dynamic properties","author":"deutsch","year":"2004","journal-title":"PolySpace White Paper"},{"key":"ref37","first-page":"195","article-title":"Using modelica for testing embedded systems","author":"freiseisen","year":"0","journal-title":"Proc 2nd Int Modelica Conf"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2014.28"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/CACSD.1999.808720"},{"key":"ref34","author":"el-khoury","year":"0"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020947"},{"key":"ref27","doi-asserted-by":"crossref","first-page":"321","DOI":"10.15700\/saje.v28n3a176","article-title":"The “movement” of mixed methods research and the role of educators","volume":"3","author":"creswell","year":"2008","journal-title":"South Afr J Edu"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2011.2160929"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_44"},{"key":"ref22","article-title":"Analysis and verification challenges for cyber-physical transportation systems","author":"clarke","year":"0","journal-title":"Proc Nat Workshop Res High Confidence Transp"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_23"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-5757-3_2"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24372-1_1"},{"key":"ref101","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2001.972741"},{"key":"ref26","author":"creswell","year":"2012","journal-title":"Qualitative Inquiry and Research Design Choosing Among Five Traditions"},{"key":"ref100","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_21"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"ref50","year":"2015","journal-title":"Klocwork"},{"key":"ref51","year":"2015","journal-title":"Simulink Design Verifier Temporal Properties—MathWorks"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1145\/1460412.1460423"},{"key":"ref57","first-page":"672","article-title":"Why don’t software developers use static analysis tools to find bugs?","author":"johnson","year":"0","journal-title":"Proc Int Conf Softw Eng (ICSE)"},{"key":"ref56","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1109\/JPROC.2011.2161241","article-title":"Cyber-physical modeling of implantable cardiac medical devices","volume":"100","author":"jiang","year":"0","journal-title":"Proc IEEE"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88387-6_17"},{"key":"ref54","year":"2015","journal-title":"Simulink Design Verifier"},{"key":"ref53","year":"2015","journal-title":"Polyspace Static Analyzers"},{"key":"ref52","year":"2015","journal-title":"Simulink Design Verifier Types of Model Coverage—MathWorks"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/1595696.1595724"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24372-1_3"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.comcom.2012.01.003"},{"key":"ref6","first-page":"161","article-title":"Cyber-physical systems","author":"baheti","year":"2011","journal-title":"The Impact of Control Technology"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_21"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1965724.1965743"},{"key":"ref49","year":"2015","journal-title":"Coverity"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48320-9_12"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2006.27"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_29"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_48"},{"key":"ref48","year":"2015","journal-title":"C Global Surveyor"},{"key":"ref47","article-title":"Basic spin manual","author":"holzmann","year":"1994"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"ref41","first-page":"1183","article-title":"Reachability analysis of hybrid control systems using reduced-order models","volume":"2","author":"han","year":"0","journal-title":"Proc Amer Control Conf"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/2024724.2024777"},{"key":"ref43","author":"harrison","year":"2012","journal-title":"Theorem Proving with the Real Numbers"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.21236\/ADA447048"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1007\/s10958-006-0007-z"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1109\/DASC.2009.140"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1993.274940"},{"key":"ref76","article-title":"Automated test suite generation for time-continuous simulink models","author":"matinnejad","year":"2015"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1109\/32.910858"},{"key":"ref74","first-page":"35","article-title":"Grounded theory: A critical research methodology","author":"magnetto neff","year":"1998","journal-title":"Under Construction Working at the Intersections of Composition Theory Research and Practice"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2013.77"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1109\/ICIS.2010.73"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40787-1_10"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1145\/2807426.2817926"},{"key":"ref65","article-title":"Cyber-physical systems-are computing foundations adequate","volume":"2","author":"lee","year":"0","journal-title":"Proc NSF Workshop Cyber-Phys Syst (CPS)"},{"key":"ref66","article-title":"Computing foundations and practice for cyber-physical systems: A preliminary report","author":"lee","year":"2007"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2008.25"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.10.015"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2009.101"},{"key":"ref69","first-page":"351","article-title":"A verifying compiler for a multi-threaded object-oriented","volume":"9","author":"leino","year":"2007","journal-title":"Softw Syst Rel Security"},{"key":"ref1","first-page":"48","article-title":"Verification of hybrid systems: Formalization and proof rules in PVS","author":"abrah\u00e1m-mumm","year":"0","journal-title":"Proc Int Conf Eng Complex Comput Syst (ICECCS)"},{"key":"ref109","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2009.21"},{"key":"ref95","doi-asserted-by":"publisher","DOI":"10.1145\/1791212.1791235"},{"key":"ref108","doi-asserted-by":"publisher","DOI":"10.1145\/1322263.1322282"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.18.217-238"},{"key":"ref107","first-page":"308","article-title":"Specification, analyzing challenges and approaches for cyber-physical systems (CPS)","volume":"18","author":"wan","year":"2010","journal-title":"Eng Lett"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.1109\/RTCSA.2005.84"},{"key":"ref106","doi-asserted-by":"publisher","DOI":"10.1109\/NESEA.2010.5678065"},{"key":"ref92","first-page":"337","article-title":"PDA: Passive distributed assertions for sensor networks","author":"romer","year":"0","journal-title":"Proc Int Conf Inf Process Sensor Netw (IPSN)"},{"key":"ref105","article-title":"Torx: Automated model-based testing","author":"tretmans","year":"2003"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.1145\/1098918.1098946"},{"key":"ref104","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45873-5_36"},{"key":"ref90","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837461"},{"key":"ref103","doi-asserted-by":"publisher","DOI":"10.1145\/1795194.1795197"},{"key":"ref102","doi-asserted-by":"publisher","DOI":"10.1145\/1644038.1644053"},{"key":"ref110","doi-asserted-by":"publisher","DOI":"10.1109\/PerComW.2014.6815195"},{"key":"ref98","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2005.3"},{"key":"ref99","article-title":"ns-2","author":"simulator","year":"1989"},{"key":"ref96","doi-asserted-by":"publisher","DOI":"10.1109\/WCSP.2011.6096958"},{"key":"ref97","doi-asserted-by":"publisher","DOI":"10.1007\/s00163-013-0156-2"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"ref11","author":"ben-ari","year":"2008","journal-title":"Principles of the Spin Model Checker"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36377-7_5"},{"key":"ref13","article-title":"The successful development process with matlab simulink in the framework Of ESA’s ATV project","author":"bodemann","year":"0","journal-title":"Proc Int Astronautical Conf"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1984.233702"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0097-0"},{"key":"ref16","first-page":"389","article-title":"Temporal issues in cyber-physical systems","volume":"93","author":"broman","year":"2013","journal-title":"J Indian Inst Sci"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00088-8"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2000367.2000368"},{"key":"ref81","article-title":"Using models to address challenges in specifying requirements for medical cyber-physical systems","author":"murugesan","year":"0","journal-title":"Proc Int Conf Cyber Phys Syst (ICCPS)"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_36"},{"key":"ref84","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85778-5_1"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2012.77"},{"key":"ref83","volume":"2283","author":"nipkow","year":"2002","journal-title":"Isabelle\/HOL A Proof Assistant for Higher-Order Logic"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606579"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.02.005"},{"key":"ref85","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1145\/2584651","article-title":"Safety-critical medical device development using the UPP2SF model","volume":"13","author":"pajic","year":"2014","journal-title":"ACM Trans Embedded Comput Syst"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2010.22"},{"key":"ref87","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_23"},{"key":"ref88","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"}],"container-title":["IEEE Systems Journal"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/4267003\/8118221\/07332847.pdf?arnumber=7332847","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,11]],"date-time":"2021-10-11T02:35:07Z","timestamp":1633919707000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7332847\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12]]},"references-count":110,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/jsyst.2015.2496293","relation":{},"ISSN":["1932-8184","1937-9234","2373-7816"],"issn-type":[{"value":"1932-8184","type":"print"},{"value":"1937-9234","type":"electronic"},{"value":"2373-7816","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12]]}}}