{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T02:46:46Z","timestamp":1777690006818,"version":"3.51.4"},"reference-count":75,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"5","license":[{"start":{"date-parts":[[2016,5,1]],"date-time":"2016-05-01T00:00:00Z","timestamp":1462060800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2016,5,1]],"date-time":"2016-05-01T00:00:00Z","timestamp":1462060800000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2016,5,1]],"date-time":"2016-05-01T00:00:00Z","timestamp":1462060800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2016,5,1]],"date-time":"2016-05-01T00:00:00Z","timestamp":1462060800000},"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":["#1329759"],"award-info":[{"award-number":["#1329759"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["#1139138"],"award-info":[{"award-number":["#1139138"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Industrial Cyber-Physical Systems Research Center"},{"name":"IBM and United Technologies"},{"DOI":"10.13039\/501100002341","name":"Academy of Finland","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002341","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. IEEE"],"published-print":{"date-parts":[[2016,5]]},"DOI":"10.1109\/jproc.2015.2510366","type":"journal-article","created":{"date-parts":[[2016,3,14]],"date-time":"2016-03-14T18:07:49Z","timestamp":1457978869000},"page":"960-972","source":"Crossref","is-referenced-by-count":39,"title":["Compositionality in the Science of System Design"],"prefix":"10.1109","volume":"104","author":[{"given":"Stavros","family":"Tripakis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594321"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1145\/1168917.1168907"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2006.890107"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-13338-6_7"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23217-6_27"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_23"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/1331331.1331339"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"ref32","first-page":"414","article-title":"Replacing testing with formal verification in Intel Core TM i7 processor execution engine validation","author":"kaivola","year":"0","journal-title":"Proc 21st Int Conf Comput Aided Verif"},{"key":"ref31","author":"holzmann","year":"2003","journal-title":"The SPIN Model Checker"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2008.81"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2013.77"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1965724.1965743"},{"key":"ref60","author":"fritzson","year":"2014","journal-title":"Principles of Object-Oriented Modeling and Simulation with Modelica 3 3 A Cyber-Physical Approach"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1145\/1086519.1086526"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2000.858698"},{"key":"ref28","article-title":"Piecewise affine approximations for a powertrain control benchmark","author":"deshmukh","year":"0","journal-title":"Proc Workshop Appl Verif Contin Hybrid Syst"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.2004.15"},{"key":"ref27","article-title":"Benchmarks for model transformations and conformance checking","author":"jin","year":"0","journal-title":"Proc Workshop Appl Verif Contin Hybrid Syst"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2006.27"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967707"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1038\/nbt1356"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2011.2161529"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2008.0141"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1145\/1506409.1506426"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2007.364"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_1"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1201\/b19290-7"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2006.888386"},{"key":"ref21","article-title":"This car runs on code","author":"charette","year":"2009","journal-title":"IEEE Spectrum"},{"key":"ref24","author":"nicolescu","year":"2010","journal-title":"Model-Based Design for Embedded Systems"},{"key":"ref23","article-title":"What to do (and how to find out) if your car is being recalled-updated","author":"gorzelany","year":"2014","journal-title":"Forbes"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562140"},{"key":"ref25","doi-asserted-by":"crossref","DOI":"10.1201\/9781420011746","author":"lee","year":"2007","journal-title":"Handbook of Real-Time and Embedded Systems"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/268999.269004"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.3384\/ecp15118159"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT.2013.6658580"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1109\/SAMOS.2015.7363660"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-32582-8_3"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1145\/2656045.2656068"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1145\/1985342.1985345"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45449-7_11"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"ref11","author":"alur","year":"2015","journal-title":"Principles of Cyber-Physical Systems"},{"key":"ref40","article-title":"The semantics of a simple language for parallel programming","author":"kahn","year":"0","journal-title":"Proc IFIP Congr Inf Process"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5"},{"key":"ref13","author":"kohavi","year":"1978","journal-title":"Switching and Finite Automata Theory"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10699-5_102"},{"key":"ref16","author":"clarke","year":"2000","journal-title":"Model checking"},{"key":"ref17","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2508443.2508452"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_15"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/SUTC.2008.85"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2008.25"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2012.2189792"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837461"},{"key":"ref8","author":"luenberger","year":"1979","journal-title":"Introduction to Dynamic Systems Theory Models and Applications"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2011.2167449"},{"key":"ref49","first-page":"219","article-title":"An introduction to input\/output automata","volume":"2","author":"lynch","year":"1989","journal-title":"CWI Quart"},{"key":"ref9","author":"oppenheim","year":"1983","journal-title":"Signals and Systems"},{"key":"ref46","first-page":"78","article-title":"Modular code generation from synchronous block diagrams—Modularity vs. code size","author":"lublinerman","year":"0","journal-title":"Proc 36th ACM SIGPLAN-SIGACT Symp Principles Programm Lang"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2008.12"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1987.13876"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2442116.2442133"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805829"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49213-5"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/1403375.1403736"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129512000278"}],"container-title":["Proceedings of the IEEE"],"original-title":[],"link":[{"URL":"http:\/\/ieeexplore.ieee.org\/ielaam\/5\/7456363\/7433380-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/5\/7456363\/07433380.pdf?arnumber=7433380","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,8]],"date-time":"2022-04-08T18:55:57Z","timestamp":1649444157000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7433380\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5]]},"references-count":75,"journal-issue":{"issue":"5"},"URL":"https:\/\/doi.org\/10.1109\/jproc.2015.2510366","relation":{},"ISSN":["0018-9219","1558-2256"],"issn-type":[{"value":"0018-9219","type":"print"},{"value":"1558-2256","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,5]]}}}