{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T23:36:36Z","timestamp":1791416196044,"version":"4.3.3"},"reference-count":121,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"9","license":[{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1139138"],"award-info":[{"award-number":["CCF-1139138"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1116993"],"award-info":[{"award-number":["CCF-1116993"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1545126"],"award-info":[{"award-number":["CNS-1545126"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["FA8750-16-C-0043"],"award-info":[{"award-number":["FA8750-16-C-0043"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004405","name":"Toyota Motor Corporation through the CHESS Center","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004405","id-type":"DOI","asserted-by":"publisher"}]},{"name":"TerraSwarm Research Center, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA"},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1646497"],"award-info":[{"award-number":["CCF-1646497"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["FA8750-16-C-0043"],"award-info":[{"award-number":["FA8750-16-C-0043"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-14-1-0815"],"award-info":[{"award-number":["N00014-14-1-0815"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-14-1-0816"],"award-info":[{"award-number":["N00014-14-1-0816"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1553757"],"award-info":[{"award-number":["CCF-1553757"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1646381"],"award-info":[{"award-number":["CCF-1646381"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2017,9]]},"DOI":"10.1109\/tcad.2016.2633961","type":"journal-article","created":{"date-parts":[[2016,12,8]],"date-time":"2016-12-08T14:14:05Z","timestamp":1481206445000},"page":"1421-1434","source":"Crossref","is-referenced-by-count":147,"title":["Design Automation of Cyber-Physical Systems: Challenges, Advances, and Opportunities"],"prefix":"10.1109","volume":"36","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6190-8707","authenticated-orcid":false,"given":"Sanjit A.","family":"Seshia","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shiyan","family":"Hu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wenchao","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qi","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","article-title":"Satisfiability modulo theories","volume":"4","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref38","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","article-title":"Bounded model checking","volume":"58","author":"biere","year":"2003","journal-title":"Adv Comput"},{"key":"ref33","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1109\/JPROC.2006.890107","article-title":"Quo vadis, SLD? Reasoning about the trends and challenges of system level design","volume":"95","author":"sangiovanni-vincentelli","year":"2007","journal-title":"Proc IEEE"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996684"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/43.898830"},{"key":"ref30","article-title":"Data-driven probabilistic modeling and verification of human driver behavior","author":"sadigh","year":"2014","journal-title":"Proc Formal Verification Model Human Mach Syst AAAI Spring Symp"},{"key":"ref37","year":"2016","journal-title":"KMel Robotics"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6942758"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2453253"},{"key":"ref28","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-54862-8_40","article-title":"Synthesis of human-in-the-loop control systems","author":"li","year":"2014","journal-title":"Proc 20th Int Conf Tools Algorithms Construct Anal Syst (TACAS)"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2747927"},{"key":"ref29","first-page":"527","article-title":"Polynomial-time verification of PCTL properties of MDPs with convex uncertainties","author":"puggelli","year":"2013","journal-title":"Proc 25th Int Conf Comput -Aided Verification (CAV)"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562139"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2471838"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228425"},{"key":"ref24","article-title":"Towards verified artificial intelligence","author":"seshia","year":"2016","journal-title":"ArXiv e-prints"},{"key":"ref23","article-title":"Concrete problems in AI safety","author":"amodei","year":"2016","journal-title":"ArXiv e-prints"},{"key":"ref101","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2005.1570410"},{"key":"ref26","article-title":"To err is human: Building a safer health system","author":"kohn","year":"2000"},{"key":"ref100","year":"2013","journal-title":"Preliminary Statement of Policy Concerning Automated Vehicles"},{"key":"ref25","year":"1995","journal-title":"The Interfaces Between Flightcrews and Modern Flight Deck Systems"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/2502524.2502533"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2014.7001351"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1016\/j.enbuild.2011.09.039"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1016\/j.enbuild.2011.05.020"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1016\/j.buildenv.2010.08.002"},{"key":"ref56","first-page":"226","article-title":"Literature review on calibration of building energy simulation programs: Uses, problems, procedures, uncertainty, and tools","volume":"112","author":"reddy","year":"2006","journal-title":"ASHRAE Trans"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45928-7_5"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1145\/2821650.2821658"},{"key":"ref53","year":"0","journal-title":"EnergyPlus A Whole Building Energy Simulation Program"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2596670"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.20"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2011.2161529"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837462"},{"key":"ref6","author":"skogestad","year":"2007","journal-title":"Multivariable Feedback Control Analysis and Design"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2747922"},{"key":"ref8","author":"sastry","year":"2011","journal-title":"Adaptive Control Stability Convergence and Robustness"},{"key":"ref49","year":"0","journal-title":"Modelica"},{"key":"ref7","doi-asserted-by":"crossref","DOI":"10.1201\/9781420067859","author":"nicolescu","year":"2009","journal-title":"Model-Based Design for Embedded Systems"},{"key":"ref9","author":"\u00e5str\u00f6m","year":"2008","journal-title":"Adaptive Control"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2012.2201130"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/2803174"},{"key":"ref48","year":"0","journal-title":"Simulink"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2010.26"},{"key":"ref42","article-title":"Secure state estimation under sensor attacks: A satisfiability modulo theory approach","author":"shoukry","year":"2015","journal-title":"Proc Amer Control Conf (ACC)"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40349-1_4"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2013.2283096"},{"key":"ref43","first-page":"1","article-title":"SMT-based observer design for cyber-physical systems under sensor attacks","author":"shoukry","year":"2016","journal-title":"Proc Int Conf Cyber Phys Syst (ICCPS)"},{"key":"ref73","doi-asserted-by":"crossref","first-page":"2089","DOI":"10.1109\/TSG.2013.2257893","article-title":"Scalable and robust demand response with mixed-integer constraints","volume":"4","author":"kim","year":"2013","journal-title":"IEEE Trans Smart Grid"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1109\/TSG.2012.2226065"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1109\/TETC.2015.2484839"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1145\/2821650.2821664"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2015.2427841"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1109\/TSG.2015.2453342"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1109\/TSG.2010.2089069"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1109\/JSYST.2015.2418032"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1109\/TCSS.2016.2519506"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1109\/TSG.2013.2256939"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1115\/1.1564076"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1007\/s12273-013-0125-8"},{"key":"ref61","year":"0","journal-title":"TRNSYS An Energy Simulation Software Package"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1016\/j.enbuild.2011.12.001"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1080\/19401493.2010.549964"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1109\/DSAA.2015.7344784"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1145\/2674061.2674080"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1109\/PESGM.2015.7285865"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2014.6859389"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.18.217-238"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1109\/SAI.2015.7237185"},{"key":"ref1","author":"lee","year":"2015","journal-title":"Introduction to Embedded Systems A Cyber-physical Systems Approach"},{"key":"ref109","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228402"},{"key":"ref95","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2013.272"},{"key":"ref108","article-title":"Comprehensive experimental analyses of automotive attack surfaces","author":"checkoway","year":"2011","journal-title":"Proc Usenix Security Symp"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2016.2523937"},{"key":"ref107","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.34"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2008.45"},{"key":"ref106","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2013.31"},{"key":"ref92","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1996.563693"},{"key":"ref105","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2012.6315654"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"ref104","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2016.7759036"},{"key":"ref90","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2011.15"},{"key":"ref103","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2016.XII.029"},{"key":"ref102","doi-asserted-by":"publisher","DOI":"10.1145\/2735960.2735973"},{"key":"ref111","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2013.6691106"},{"key":"ref112","doi-asserted-by":"publisher","DOI":"10.1109\/VETECF.2008.259"},{"key":"ref110","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87698-4_21"},{"key":"ref98","year":"2015","journal-title":"Google Self-Driving Car Testing Report on Disengagements of Autonomous Mode"},{"key":"ref99","doi-asserted-by":"publisher","DOI":"10.1109\/IVS.2015.7225841"},{"key":"ref96","doi-asserted-by":"publisher","DOI":"10.1145\/2735960.2735972"},{"key":"ref97","article-title":"The internals of gametime: Implementation and evaluation of a timing analyzer for embedded software","author":"kotker","year":"2013"},{"key":"ref10","author":"chambers","year":"2011","journal-title":"Hands-Off Training Google’s Self-Driving Car Holds Tantalizing Promise but Major Roadblocks Remain"},{"key":"ref11","author":"mitchell","year":"1997","journal-title":"Machine Learning"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/356914.356918"},{"key":"ref13","article-title":"A theory of formal synthesis via inductive learning","author":"jha","year":"2015","journal-title":"ArXiv e-prints"},{"key":"ref14","first-page":"43","article-title":"Mining requirements from closed-loop control models","author":"jin","year":"2013","journal-title":"Proc Int Conf Hybrid Syst Comput Control (HSCC)"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970509"},{"key":"ref118","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2011.14"},{"key":"ref16","first-page":"239","article-title":"Reactive synthesis from signal temporal logic specifications","author":"raman","year":"2015","journal-title":"Proc 8th Int Conf Hybrid Syst Comput Control (HSCC)"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2015.7372606"},{"key":"ref117","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2009.5270342"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038660"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2015.2495244"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2008.4681634"},{"key":"ref84","first-page":"3","article-title":"This car runs on code","volume":"46","author":"charette","year":"2009","journal-title":"IEEE Spectr"},{"key":"ref119","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.2000.848446"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/2331147.2331165"},{"key":"ref83","doi-asserted-by":"publisher","DOI":"10.1145\/2560519.2565873"},{"key":"ref114","article-title":"Low cost multicast network authentication for embedded control systems","author":"szilagyi","year":"2012"},{"key":"ref113","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/978-3-642-35404-5_15","article-title":"LiBrA-CAN: A lightweight broadcast authentication protocol for controller area networks","author":"groza","year":"2012","journal-title":"Proc 11th Int Conf Cryptol Netw Security (CANS)"},{"key":"ref116","doi-asserted-by":"publisher","DOI":"10.1145\/1873548.1873558"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1109\/TETC.2015.2484841"},{"key":"ref115","article-title":"CANAuth—A simple, backward compatible broadcast authentication protocol for CAN bus","author":"herrewege","year":"2011","journal-title":"Proceedings of the Workshop on Embeded Security on Cars"},{"key":"ref120","first-page":"35","article-title":"Efficient and secure source authentication for multicast","author":"ran","year":"2001","journal-title":"Proc Network and Distributed System Security Symp (NDSS)"},{"key":"ref89","year":"2016","journal-title":"Automakers Opting for Model-Based Design"},{"key":"ref121","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2014.7001325"},{"key":"ref85","first-page":"23","article-title":"Why dinosaurs will keep ruling the auto industry","volume":"88","author":"macduffie","year":"2010","journal-title":"Harvard Bus Rev"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2009.2039550"},{"key":"ref87","year":"2013","journal-title":"The Road to 2020 and Beyond-What’s Driving the Global Automotive Industry"},{"key":"ref88","year":"2016","journal-title":"General Motors Developed Two-Mode Hybrid Powertrain With Mathworks Model-Based Design Cut 24 Months Off Expected Dev Time"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/ieeexplore.ieee.org\/ielaam\/43\/8013181\/7778207-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/8013181\/07778207.pdf?arnumber=7778207","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,8]],"date-time":"2022-04-08T14:47:48Z","timestamp":1649429268000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7778207\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":121,"journal-issue":{"issue":"9"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2016.2633961","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"value":"0278-0070","type":"print"},{"value":"1937-4151","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9]]}}}