{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,14]],"date-time":"2025-10-14T07:17:40Z","timestamp":1760426260633,"version":"3.37.3"},"reference-count":44,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"NSF","award":["1846524","2139982"],"award-info":[{"award-number":["1846524","2139982"]}]},{"name":"Jet Propulsion Laboratory (JPL) Graduate Fellowship"},{"name":"JPL, California Institute of Technology through National Aeronautics and Space Administration","award":["80NM0018D0004"],"award-info":[{"award-number":["80NM0018D0004"]}]},{"name":"International Conference on Embedded Software (EMSOFT) 2024 and the ESWEEK-TCAD special issue"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2024,11]]},"DOI":"10.1109\/tcad.2024.3447213","type":"journal-article","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T19:12:02Z","timestamp":1725995522000},"page":"4298-4309","source":"Crossref","is-referenced-by-count":3,"title":["Contract-Based Hierarchical Modeling and Traceability of Heterogeneous Requirements"],"prefix":"10.1109","volume":"43","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6871-2010","authenticated-orcid":false,"given":"Nikhil Vijay","family":"Naik","sequence":"first","affiliation":[{"name":"Department of Electrical and Computer Engineering, University of Southern California, Los Angeles, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8308-311X","authenticated-orcid":false,"given":"Alessandro","family":"Pinto","sequence":"additional","affiliation":[{"name":"NASA Jet Propulsion Laboratory, California Institute of Technology, Pasadena, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2984-0364","authenticated-orcid":false,"given":"Pierluigi","family":"Nuzzo","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, University of Southern California, Los Angeles, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"article-title":"NASA systems engineering handbook","year":"2017","author":"Hirshorn","key":"ref1"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/AERO50100.2021.9438470"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/AERO.2019.8742020"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3730-6_9"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1996.0002"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1002\/sys.20017"},{"volume-title":"Failure Mode and Effect Analysis","year":"2003","author":"Stamatis","key":"ref7"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s43154-021-00057-2"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1561\/1000000053"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2453253"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2018.8342122"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-14835-4_5"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693137"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95246-8_22"},{"article-title":"Principles for architecting autonomous systems","year":"2022","author":"Day","key":"ref15"},{"volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","year":"2002","author":"Lamport","key":"ref16"},{"volume-title":"System Modelling & Design Using Event-B","year":"2012","author":"Robinson","key":"ref17"},{"key":"ref18","first-page":"1","volume-title":"Refinement Calculus: A Systematic Introduction","author":"Back","year":"2012"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_6"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_9"},{"volume-title":"System Design, Modeling, and Simulation Using Ptolemy II","year":"2014","author":"Ptolemaeus","key":"ref22"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1193228"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/43.736561"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2351672"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/1017753.1017781"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68679-8_44"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0024-z"},{"article-title":"Compositional contract abstraction for system design","year":"2014","author":"Benveniste","key":"ref30"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-1898-5"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2013.2295764"},{"key":"ref33","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4614-6956-8","volume-title":"Measure Theory","volume":"5","author":"Cohn","year":"2013"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.21236\/ADA256199"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"volume-title":"Inverse of subset of relation is subset of inverse","year":"2024","key":"ref36"},{"volume-title":"A Course on Group Theory","year":"1994","author":"Rose","key":"ref37"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/SIES.2013.6601484"},{"volume-title":"Cooperative Autonomous Distributed Robotic Exploration (CADRE)","year":"2023","key":"ref40"},{"volume-title":"Control System Design: An Introduction to State-Space Methods","year":"2012","author":"Friedland","key":"ref41"},{"key":"ref42","first-page":"3","article-title":"Simple on-the-fly automatic verification of linear temporal logic","volume-title":"Proc. Int. Conf. Protocol Specification, Testing Verification","author":"Gerth"},{"key":"ref43","first-page":"854","article-title":"Linear temporal logic and linear dynamic logic on finite traces","volume-title":"Proc. Int. Joint Conf. Artif. Intell.","author":"De Giacomo"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15297-9_9"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"https:\/\/ieeexplore.ieee.org\/ielam\/43\/10745760\/10673795-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/43\/10745760\/10673795.pdf?arnumber=10673795","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T00:37:42Z","timestamp":1732667862000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10673795\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11]]},"references-count":44,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2024.3447213","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"type":"print","value":"0278-0070"},{"type":"electronic","value":"1937-4151"}],"subject":[],"published":{"date-parts":[[2024,11]]}}}