{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T13:23:47Z","timestamp":1773840227222,"version":"3.50.1"},"reference-count":115,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2015,11,1]],"date-time":"2015-11-01T00:00:00Z","timestamp":1446336000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"IBM"},{"name":"UTC"},{"name":"TerraSwarm Research Center"},{"name":"STARnet phase of the Focus Center Research Program (FCRP)"},{"DOI":"10.13039\/100007245","name":"MARCO","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100007245","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]},{"name":"EU Commission","award":["FP7-ICT-223844 CON4COORD"],"award-info":[{"award-number":["FP7-ICT-223844 CON4COORD"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. IEEE"],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1109\/jproc.2015.2453253","type":"journal-article","created":{"date-parts":[[2015,9,15]],"date-time":"2015-09-15T18:35:42Z","timestamp":1442342142000},"page":"2104-2132","source":"Crossref","is-referenced-by-count":128,"title":["A Platform-Based Design Methodology With Contracts and Related Tools for the Design of Cyber-Physical Systems"],"prefix":"10.1109","volume":"103","author":[{"given":"Pierluigi","family":"Nuzzo","sequence":"first","affiliation":[]},{"given":"Alberto L.","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[]},{"given":"Davide","family":"Bresolin","sequence":"additional","affiliation":[]},{"given":"Luca","family":"Geretti","sequence":"additional","affiliation":[]},{"given":"Tiziano","family":"Villa","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00067-1"},{"key":"ref33","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","article-title":"Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems","volume":"736","author":"alur","year":"1993","journal-title":"Hybrid Syst"},{"key":"ref32","first-page":"188","article-title":"Requirements validation for hybrid systems","volume":"5643","author":"cimatti","year":"2009","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref31","first-page":"152","article-title":"Monitoring temporal properties of continuous signals","author":"maler","year":"0","journal-title":"Proc Conf Formal Modeling Anal Timed Syst"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100062"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14509-4"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054107004577"},{"key":"ref28","article-title":"Satisfiability modulo theories","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_45"},{"key":"ref29","first-page":"71","article-title":"CalCS: SMT solving for non-linear convex constraints","author":"nuzzo","year":"0","journal-title":"Proc Formal Methods Comput -Aided Design"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-3879-3_8"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1193228"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/2656075.2656093"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1201\/9781420067859-c10"},{"key":"ref101","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.1997.649708"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2502524.2502540"},{"key":"ref100","doi-asserted-by":"publisher","DOI":"10.1080\/0020717031000123616"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/SIES.2011.5953662"},{"key":"ref50","first-page":"258","article-title":"Flow $^{\\ast}$: An analyzer for non-linear hybrid systems","volume":"8044","author":"chen","year":"2013","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33512-9_8"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0158-0"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0044-3"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1145\/1210268.1210276"},{"key":"ref56","first-page":"1","article-title":"Modeling and verification of hybrid dynamical system using CheckMate","author":"silva","year":"0","journal-title":"Proc Int Conf Autom Mixed Processes Hybrid Dynamic Syst"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410300190X"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.026"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2013.143"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-009-0082-7"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2006.890107"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54848-2_13"},{"key":"ref6","author":"clarke","year":"2008","journal-title":"Model checking"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/JSEN.2012.2211098"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92188-2_9"},{"key":"ref49","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","article-title":"SpaceEx: Scalable verification of hybrid systems","volume":"6806","author":"frehse","year":"2011","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.18.217-238"},{"key":"ref46","author":"b\u00e9rard","year":"2000","journal-title":"Comparing verification with HyTech KRONOS and Uppaal on the railroad crossing example"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1002\/spe.1006"},{"key":"ref48","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","article-title":"PHAVer: Algorithmic verification of hybrid systems past HyTech","volume":"10","author":"frehse","year":"2008","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"ref47","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/3-540-46430-1_6","article-title":"Approximate reachability analysis of piecewise-linear dynamical systems","volume":"1790","author":"asarin","year":"2000","journal-title":"Proc Hybrid Systems Computation and Control"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1002\/rnc.2914"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561342"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"key":"ref43","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","article-title":"KRONOS: A verification tool for real-time systems","volume":"1","author":"yovine","year":"1997","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.3384\/ecp12076173"},{"key":"ref72","year":"0","journal-title":"Omg systems modeling language"},{"key":"ref71","first-page":"527","article-title":"Enabling multi-view modeling with SysML profiles and model transformations","author":"shah","year":"0","journal-title":"Proc Int Conf Product Lifecycle Manage"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.07.001"},{"key":"ref76","doi-asserted-by":"crossref","first-page":"561","DOI":"10.7873\/DATE.2015.0913","article-title":"Optimized Selection of Reliable and Cost-Effective Cyber-Physical System Architectures","author":"nikunj bajaj","year":"2015","journal-title":"Design Automation Test in Europe Conference Exhibition (DATE)"},{"key":"ref77","first-page":"441","article-title":"Synthesizing cyber-physical architectural models with real-time constraints","author":"hang","year":"0","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref74","year":"2010","journal-title":"Functional mock-up interface for co-simulation Version 1 0"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT.2013.6658580"},{"key":"ref78","first-page":"364","article-title":"Synthesis of reactive(1) designs","author":"piterman","year":"0","journal-title":"Verification Model Checking and Abstract Interpretation"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.914952"},{"key":"ref60","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","article-title":"Breach, a toolbox for verification and parameter synthesis of hybrid systems","author":"donz\u00e9","year":"2010","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref62","first-page":"296","article-title":"System level formal verification via model checking driven simulation","volume":"8044","author":"mancini","year":"2013","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref61","first-page":"254","article-title":"S-TaLiRo: A tool for temporal logic falsification for hybrid systems","author":"annpureddy","year":"0","journal-title":"Proc Int Conf Tools Algor Construct Anal Syst"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1109\/MCS.2007.906923"},{"key":"ref64","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1007\/3-540-46430-1_5","article-title":"Modular specification of hybrid systems in Charon","volume":"1790","author":"alur","year":"2000","journal-title":"Proc Hybrid Systems Computation and Control"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805825"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1145\/1176887.1176907"},{"key":"ref67","year":"2002","journal-title":"HSIF Semantics"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_37"},{"key":"ref69","author":"di cairano","year":"2006","journal-title":"An architecture for data interchange of switched linear systems"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2008.25"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2007.25"},{"key":"ref109","doi-asserted-by":"publisher","DOI":"10.2514\/4.479526"},{"key":"ref95","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2012.96"},{"key":"ref108","first-page":"1","article-title":"Contract-based design of control protocols for safety-critical cyber-physical systems","author":"nuzzo","year":"0","journal-title":"Proc Design Autom Test Eur"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6942758"},{"key":"ref107","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_4"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.1145\/2559934"},{"key":"ref106","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_20"},{"key":"ref92","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_49"},{"key":"ref105","author":"wulf","year":"2006","journal-title":"From timed models to timed implementations"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2009.2034922"},{"key":"ref104","first-page":"1381","article-title":"Synthesis of implementable control strategies for lazy linear hybrid automata","author":"di guglielmo","year":"0","journal-title":"Proc FedCSIS"},{"key":"ref90","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039363"},{"key":"ref103","doi-asserted-by":"publisher","DOI":"10.1109\/IWCMC.2011.5982784"},{"key":"ref102","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.10.042"},{"key":"ref111","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_3"},{"key":"ref112","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.23"},{"key":"ref110","year":"2012","journal-title":"IBM ILOG CPLEX Optimizer"},{"key":"ref98","year":"0","journal-title":"UPPAAL-Tiga A Synthesis Tool for Timed Games"},{"key":"ref99","doi-asserted-by":"publisher","DOI":"10.1109\/5.871303"},{"key":"ref96","first-page":"229","article-title":"On the synthesis of discrete controllers for timed systems (an extended abstract)","author":"maler","year":"0","journal-title":"Proc Sixth Symp Theoretical Aspects of Computer Science"},{"key":"ref97","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"ref10","author":"benveniste","year":"2012","journal-title":"Contracts for system design"},{"key":"ref11","author":"masin","year":"2011","journal-title":"META II Lingua franca design and integration language"},{"key":"ref12","first-page":"1","article-title":"Boosting re-use of embedded automotive applications through rich components","author":"damm","year":"0","journal-title":"Proceedings of Foundations of Interface Technologies"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2011.5763167"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2013.2295764"},{"key":"ref15","first-page":"1","article-title":"Library-based scalable refinement checking for contract-based design","author":"iannopollo","year":"0","journal-title":"Proc Design Autom Test Eur"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45928-7_5"},{"key":"ref82","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-14295-6_18","article-title":"JTLV: A framework for developing verification algorithms","volume":"6174","author":"pnueli","year":"2010","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1002\/j.2334-5837.2015.00060.x"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967747"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2014.6961848"},{"key":"ref84","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-3-642-14295-6_37","article-title":"RATSY—A new requirements analysis tool with synthesis","volume":"6174","author":"bloem","year":"2010","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref19","first-page":"58","article-title":"Contract-based design for computation and verification of a closed-loop hybrid system","author":"benvenuti","year":"0","journal-title":"Proc Hybrid Syst Comput Control"},{"key":"ref83","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_29"},{"key":"ref114","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"ref113","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0162-4"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"ref115","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","article-title":"PRISM 4.0: Verification of probabilistic real-time systems","volume":"6806","author":"kwiatkowska","year":"2011","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2013.6760330"},{"key":"ref85","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-013-0191-5"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1109\/5.21072"},{"key":"ref87","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7"},{"key":"ref88","first-page":"575","article-title":"CIF 3: Model-based engineering of supervisory controllers","author":"van beek","year":"2014","journal-title":"Int Conf on Tools and Algor for Constr and Analysis of Systems"}],"container-title":["Proceedings of the IEEE"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/5\/7302610\/07268792.pdf?arnumber=7268792","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T15:58:43Z","timestamp":1642003123000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7268792\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11]]},"references-count":115,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/jproc.2015.2453253","relation":{},"ISSN":["0018-9219","1558-2256"],"issn-type":[{"value":"0018-9219","type":"print"},{"value":"1558-2256","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,11]]}}}