{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T13:22:31Z","timestamp":1773840151263,"version":"3.50.1"},"reference-count":31,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"vor","delay-in-days":1461,"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"funder":[{"name":"ARTEMIS Joint Undertaking","award":["269265"],"award-info":[{"award-number":["269265"]}]},{"name":"ARTEMIS Joint Undertaking","award":["295373"],"award-info":[{"award-number":["295373"]}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2015,1]]},"DOI":"10.1016\/j.scico.2014.06.011","type":"journal-article","created":{"date-parts":[[2014,7,7]],"date-time":"2014-07-07T21:45:40Z","timestamp":1404769540000},"page":"333-348","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":63,"special_numbering":"P3","title":["Contracts-refinement proof system for component-based embedded systems"],"prefix":"10.1016","volume":"97","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.scico.2014.06.011_br0010","series-title":"SEAA","article-title":"A property-based proof system for contract-based design","author":"Cimatti","year":"2012"},{"issue":"10","key":"10.1016\/j.scico.2014.06.011_br0020","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","article-title":"Applying \u201cDesign by contract\u201d","volume":"25","author":"Meyer","year":"1992","journal-title":"Computer"},{"key":"10.1016\/j.scico.2014.06.011_br0030","series-title":"FMCO","first-page":"200","article-title":"Multiple viewpoint contract-based specification and design","author":"Benveniste","year":"2007"},{"key":"10.1016\/j.scico.2014.06.011_br0040","series-title":"A generic model of contracts for embedded systems","author":"Benveniste","year":"2007"},{"key":"10.1016\/j.scico.2014.06.011_br0050","series-title":"SEFM","first-page":"377","article-title":"Contract-based verification of hierarchical systems of components","author":"Quinton","year":"2008"},{"key":"10.1016\/j.scico.2014.06.011_br0060","series-title":"TIMOBD'11","article-title":"Contract-based reasoning for component systems with complex interactions","author":"Graf","year":"2011"},{"key":"10.1016\/j.scico.2014.06.011_br0070","series-title":"DATE","first-page":"1023","article-title":"Using contract-based component specifications for virtual integration testing and architecture design","author":"Damm","year":"2011"},{"key":"10.1016\/j.scico.2014.06.011_br0080","series-title":"FASE","first-page":"43","article-title":"Moving from specifications to contracts in component-based design","author":"Bauer","year":"2012"},{"key":"10.1016\/j.scico.2014.06.011_br0090","series-title":"NFM","first-page":"126","article-title":"Compositional verification of architectural models","author":"Cofer","year":"2012"},{"key":"10.1016\/j.scico.2014.06.011_br0100","series-title":"Contracts for system design","author":"Benveniste","year":"2012"},{"key":"10.1016\/j.scico.2014.06.011_br0110","series-title":"ASE","first-page":"702","article-title":"OCRA: a tool for checking the refinement of temporal contracts","author":"Cimatti","year":"2013"},{"key":"10.1016\/j.scico.2014.06.011_br0120","series-title":"FOCS","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"key":"10.1016\/j.scico.2014.06.011_br0130","series-title":"CAV","first-page":"188","article-title":"Requirements validation for hybrid systems","author":"Cimatti","year":"2009"},{"issue":"3","key":"10.1016\/j.scico.2014.06.011_br0140","doi-asserted-by":"crossref","first-page":"217","DOI":"10.3166\/ejc.18.217-238","article-title":"Taming Dr. Frankenstein: contract-based design for cyber-physical systems","volume":"18","author":"Sangiovanni-Vincentelli","year":"2012","journal-title":"Eur. J. Control"},{"key":"10.1016\/j.scico.2014.06.011_br0150","series-title":"EMSOFT","first-page":"148","article-title":"Interface theories for component-based design","author":"de Alfaro","year":"2001"},{"issue":"4","key":"10.1016\/j.scico.2014.06.011_br0160","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1145\/2377656.2377659","article-title":"Validation of requirements for hybrid systems: a formal approach","volume":"21","author":"Cimatti","year":"2012","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"4","key":"10.1016\/j.scico.2014.06.011_br0170","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","article-title":"Specifying real-time properties with metric temporal logic","volume":"2","author":"Koymans","year":"1990","journal-title":"Real-Time Syst."},{"key":"10.1016\/j.scico.2014.06.011_br0180","series-title":"LICS","first-page":"390","article-title":"Real-time logics: complexity and expressiveness","author":"Alur","year":"1990"},{"issue":"3","key":"10.1016\/j.scico.2014.06.011_br0190","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/j.jss.2009.09.013","article-title":"Timed property sequence chart","volume":"83","author":"Zhang","year":"2010","journal-title":"J. Syst. Softw."},{"issue":"3","key":"10.1016\/j.scico.2014.06.011_br0200","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/2491509.2491514","article-title":"Bounded satisfiability checking of metric temporal logic specifications","volume":"22","author":"Pradella","year":"2013","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"10.1016\/j.scico.2014.06.011_br0210","unstructured":"SAE ARP4761 Guidelines and methods for conducting the safety assessment process on civil airborne systems and equipment, Dec. 1996."},{"key":"10.1016\/j.scico.2014.06.011_br0220","doi-asserted-by":"crossref","first-page":"109","DOI":"10.3233\/FI-1999-402302","article-title":"The AltaRica formalism for describing concurrent systems","volume":"40","author":"Arnold","year":"2000","journal-title":"Fundam. Inform."},{"issue":"5","key":"10.1016\/j.scico.2014.06.011_br0230","doi-asserted-by":"crossref","first-page":"754","DOI":"10.1093\/comjnl\/bxq024","article-title":"Safety, dependability, and performance analysis of extended AADL models","volume":"54","author":"Bozzano","year":"2011","journal-title":"Comput. J."},{"issue":"3","key":"10.1016\/j.scico.2014.06.011_br0240","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/MS.2011.27","article-title":"Rigorous component-based system design using the BIP framework","volume":"28","author":"Basu","year":"2011","journal-title":"IEEE Softw."},{"key":"10.1016\/j.scico.2014.06.011_br0250","series-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Methods","author":"de Roever","year":"2001"},{"key":"10.1016\/j.scico.2014.06.011_br0260","series-title":"IFM","first-page":"307","article-title":"Partial order reduction for state\/event LTL","author":"Benes","year":"2009"},{"key":"10.1016\/j.scico.2014.06.011_br0280","series-title":"CAV","first-page":"532","article-title":"Boolean abstraction for temporal logic satisfiability","author":"Cimatti","year":"2007"},{"key":"10.1016\/j.scico.2014.06.011_br0290","series-title":"TACAS","first-page":"93","article-title":"The MathSAT5 SMT solver","author":"Cimatti","year":"2013"},{"key":"10.1016\/j.scico.2014.06.011_br0300","series-title":"HART","first-page":"33","article-title":"State clock logic: a decidable real-time logic","author":"Raskin","year":"1997"},{"key":"10.1016\/j.scico.2014.06.011_br0310","series-title":"TACAS","first-page":"46","article-title":"IC3 modulo theories via implicit predicate abstraction","author":"Cimatti","year":"2014"},{"key":"10.1016\/j.scico.2014.06.011_br0320","series-title":"CAV","article-title":"Verifying LTL properties of hybrid systems with K-liveness","author":"Cimatti","year":"2014"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/api.elsevier.com\/content\/article\/PII:S0167642314002901?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/api.elsevier.com\/content\/article\/PII:S0167642314002901?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,8,22]],"date-time":"2020-08-22T01:55:56Z","timestamp":1598061356000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642314002901"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1]]},"references-count":31,"alternative-id":["S0167642314002901"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/j.scico.2014.06.011","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2015,1]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Contracts-refinement proof system for component-based embedded systems","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/j.scico.2014.06.011","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2014 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}