{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T13:22:40Z","timestamp":1773840160456,"version":"3.50.1"},"reference-count":39,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/OAPA.html"}],"funder":[{"name":"IBM and United Technologies Corporation (UTC) via the iCyPhy consortium"},{"name":"TerraSwarm Research Center"},{"name":"STARnet phase of the Focus Center Research Program"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2014]]},"DOI":"10.1109\/access.2013.2295764","type":"journal-article","created":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T22:08:11Z","timestamp":1389823691000},"page":"1-25","source":"Crossref","is-referenced-by-count":128,"title":["A Contract-Based Methodology for Aircraft Electric Power System Design"],"prefix":"10.1109","volume":"2","author":[{"given":"Pierluigi","family":"Nuzzo","sequence":"first","affiliation":[]},{"family":"Huan Xu","sequence":"additional","affiliation":[]},{"given":"Necmiye","family":"Ozay","sequence":"additional","affiliation":[]},{"given":"John B.","family":"Finn","sequence":"additional","affiliation":[]},{"given":"Alberto L.","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[]},{"given":"Richard M.","family":"Murray","sequence":"additional","affiliation":[]},{"given":"Alexandre","family":"Donze","sequence":"additional","affiliation":[]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","year":"2012","journal-title":"IBM ILOG CPLEX Optimizer"},{"key":"ref38","first-page":"167","article-title":"Breach, a toolbox for verification and parameter synthesis of hybrid systems","author":"donz\ufffd","year":"2010","journal-title":"Proc 22nd Int Conf CAV"},{"key":"ref33","year":"2013","journal-title":"UPPAAL-Tiga A Synthesis Tool for Timed Games"},{"key":"ref32","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","author":"donz\ufffd","year":"2010","journal-title":"Formal Modeling and Analysis of Timed Systems"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967747"},{"key":"ref30","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-14295-6_18","author":"pnueli","year":"2010","journal-title":"Computer Aided Verification"},{"key":"ref37","first-page":"37","article-title":"A new component concept for fault trees","author":"kaiser","year":"2003","journal-title":"Proc 8th Austral Workshop Safety Critical Syst Softw"},{"key":"ref36","volume":"3","author":"lyu","year":"1996","journal-title":"Handbook of Software Reliability Engineering"},{"key":"ref35","first-page":"441","article-title":"Synthesizing cyber-physical architectural models with real-time constraints","author":"hang","year":"2011","journal-title":"Proc 23rd Int Conf CAV"},{"key":"ref34","volume":"4","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref10","author":"uckun","year":"2011","journal-title":"Meta Ii Formal Co-verification of Correctness of Large-scale Cyber-physical Systems during Design"},{"key":"ref11","year":"2013","journal-title":"Omg systems modeling language"},{"key":"ref12","author":"masin","year":"2011","journal-title":"META II Lingua franca design and integration language"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.2514\/6.2010-9263"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.2514\/6.2011-1506"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2011.6161470"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2012.6426175"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"ref18","first-page":"995","volume":"2","author":"emerson","year":"1990","journal-title":"Handbook Theoretical Comput Sci"},{"key":"ref19","year":"2008","journal-title":"Electrical starting generation conversion and distribution system architecture for a more electric vehicle"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/FSCS.1990.89597"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2006.890107"},{"key":"ref27","first-page":"147","author":"asarin","year":"2011","journal-title":"Runtime Verification"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2012.2235131"},{"key":"ref6","first-page":"1","article-title":"Complete aircraft system simulation for aircraft design?Paradigms for modelling of complex systems","author":"krus","year":"2000","journal-title":"Proc ICAS"},{"key":"ref29","first-page":"364","author":"piterman","year":"2006","journal-title":"Verification Model Checking and Abstract Interpretation"},{"key":"ref5","first-page":"1","article-title":"Taming Dr. Frankenstein: Contract-based design for cyber-physical systems","author":"sangiovanni-vincentelli","year":"2011","journal-title":"Proc Conf Decision Control"},{"key":"ref8","year":"2013","journal-title":"Modelica Language"},{"key":"ref7","first-page":"1","article-title":"Virtual iron bird?A multidisciplinary modelling and simulation platform for new aircraft system architectures","author":"bals","year":"2005","journal-title":"Proc German Aerosp Conf"},{"key":"ref2","author":"jomier","year":"2009","journal-title":"Final MOET technical report"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.3384\/ecp11063704"},{"key":"ref1","doi-asserted-by":"crossref","DOI":"10.2514\/4.479526","author":"moir","year":"2008","journal-title":"Aircraft Systems Mechanical Electrical and Avionics Subsystems Integration"},{"key":"ref20","author":"benveniste","year":"2012","journal-title":"Contracts for system design"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/JSEN.2012.2211098"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1989.63473"},{"key":"ref23","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref26","first-page":"152","author":"maler","year":"2004","journal-title":"Formal Modeling and Analysis of Timed Systems"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/6705689\/06690099.pdf?arnumber=6690099","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:24:31Z","timestamp":1642004671000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6690099\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"references-count":39,"URL":"https:\/\/doi.org\/10.1109\/access.2013.2295764","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}