{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T14:48:12Z","timestamp":1775746092378,"version":"3.50.1"},"reference-count":256,"publisher":"Emerald","issue":"2-3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,3,28]]},"abstract":"<jats:p>Recently, contract-based design has been proposed as an \u201corthogonal\u201d approach that complements system design methodologies proposed so far to cope with the complexity of system design. Contract-based design provides a rigorous scaffolding for verification, analysis, abstraction\/refinement, and even synthesis. A number of results have been obtained in this domain but a unified treatment of the topic that can help put contract-based design in perspective was missing. This monograph intends to provide such a treatment where contracts are precisely defined and characterized so that they can be used in design methodologies with no ambiguity. In particular, this monograph identifies the essence of complex system design using contracts through a mathematical \u201cmeta-theory\u201d, where all the properties of the methodology are derived from a very abstract and generic notion of contract. We show that the meta-theory provides deep and illuminating links with existing contract and interface theories, as well as guidelines for designing new theories. Our study encompasses contracts for both software and systems, with emphasis on the latter. We illustrate the use of contracts with two examples: requirement engineering for a parking garage management, and the development of contracts for timing and scheduling in the context of the Autosar methodology in use in the automotive sector.<\/jats:p>","DOI":"10.1561\/1000000053","type":"journal-article","created":{"date-parts":[[2018,3,28]],"date-time":"2018-03-28T10:52:23Z","timestamp":1522234343000},"page":"124-400","source":"Crossref","is-referenced-by-count":154,"title":["Contracts for System Design"],"prefix":"10.1561","volume":"12","author":[{"given":"Albert","family":"Benveniste","sequence":"first","affiliation":[{"name":"INRIA, Rennes,","place":["France"]}]},{"given":"Beno\u00eet","family":"Caillaud","sequence":"additional","affiliation":[{"name":"INRIA, Rennes,","place":["France"]}]},{"given":"Dejan","family":"Nickovic","sequence":"additional","affiliation":[{"name":"Austrian Institute of Technology"}]},{"given":"Roberto","family":"Passerone","sequence":"additional","affiliation":[{"name":"University of Trento ,","place":["Italy"]}]},{"given":"Jean-Baptiste","family":"Raclet","sequence":"additional","affiliation":[{"name":"IRIT , Toulouse,","place":["France"]}]},{"given":"Philipp","family":"Reinkemeier","sequence":"additional","affiliation":[{"name":"Offis , Oldenburg,","place":["Germany"]}]},{"given":"Alberto","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[{"name":"University of California at Berkeley"}]},{"given":"Werner","family":"Damm","sequence":"additional","affiliation":[{"name":"Offis and University of Oldenburg ,","place":["Germany"]}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[{"name":"IST Austria , Klosterneuburg"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[{"name":"Aalborg University ,","place":["Denmark"]}]}],"member":"140","published-online":{"date-parts":[[2018,3,28]]},"reference":[{"key":"2026032901170081100_ref001","volume-title":"D.5.1.2 Pilot Project Evaluation Report. Technical report, SPEEDS project consortium","year":"2010"},{"key":"2026032901170081100_ref002","volume-title":"10 years AUTOSAR: the worldwide automotive standard for E\/E systems. ATZ extra","year":"2013"},{"issue":"1","key":"2026032901170081100_ref003","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/151646.151649","article-title":"Composing specifications","volume":"15","author":"Abadi","year":"1993","journal-title":"ACM Trans. Program. Lang. Syst"},{"issue":"3","key":"2026032901170081100_ref004","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1145\/203095.201069","article-title":"Conjoining specifications","volume":"17","author":"Abadi","year":"1995","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"2026032901170081100_ref005","first-page":"1","volume-title":"CALP, volume 372 of Lecture Notes in Computer Science","author":"Abadi","year":"1989"},{"key":"2026032901170081100_ref006","first-page":"538","volume-title":"Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science","author":"Abarbanel","year":"2000"},{"key":"2026032901170081100_ref007","first-page":"59","article-title":"Ticc: A Tool for Interface Compatibility and Composition","author":"Thomas Adler","year":"2006"},{"key":"2026032901170081100_ref008","doi-asserted-by":"crossref","DOI":"10.21236\/ADA461347","article-title":"Interface-based design","author":"Alfaro","year":"2004"},{"issue":"2","key":"2026032901170081100_ref009","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"2026032901170081100_ref010","first-page":"1","volume-title":"Lecture Notes in Computer Science","author":"Alur","year":"1994"},{"issue":"1-2","key":"2026032901170081100_ref011","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/S0304-3975(97)00173-4","article-title":"Event-clock automata: A determinizable class of timed automata","volume":"211","author":"Alur","year":"1999","journal-title":"Theor. Comput. Sci"},{"issue":"1","key":"2026032901170081100_ref012","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008739929481","article-title":"Reactive modules","volume":"15","author":"Alur","year":"1999","journal-title":"Formal Methods in System Design"},{"issue":"5","key":"2026032901170081100_ref013","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","article-title":"Alternating-time temporal logic","volume":"49","author":"Alur","year":"2002","journal-title":"J. ACM"},{"key":"2026032901170081100_ref014","first-page":"163","article-title":"Alternating refinement relations","author":"Alur","year":"1998"},{"key":"2026032901170081100_ref015","first-page":"521","article-title":"MOCHA: modularity in model checking","author":"Alur","year":"1998"},{"issue":"1","key":"2026032901170081100_ref016","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/2501626.2501629","article-title":"A comparison of compositional schedulability analysis techniques for hierarchical real-time systems","volume":"13","author":"Anand","year":"2013","journal-title":"ACM Trans. Embedded Comput. Syst"},{"key":"2026032901170081100_ref017","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/978-3-642-25264-8_20","volume-title":"SDL 2011: Integrating System and Software Modeling \u2013 15th International SDL Forum Toulouse","author":"Anssi","year":"2011"},{"key":"2026032901170081100_ref018","first-page":"152","article-title":"Enabling scheduling analysis for AUTOSAR systems","author":"Anssi","year":"2011"},{"issue":"94","key":"2026032901170081100_ref019","article-title":"20 Years of Modal and Mixed Specifications","volume":"1","author":"Antonik","year":"2008","journal-title":"Bulletin of European Association of Theoretical Computer Science"},{"key":"2026032901170081100_ref020","first-page":"112","article-title":"Complexity of Decision Problems for Mixed and Modal Specifications","volume-title":"FoSSaCS","author":"Antonik","year":"2008"},{"key":"2026032901170081100_ref021","first-page":"47","article-title":"Contracts and Behavioral Patterns for SoS: The EU IP DANSE approach","volume-title":"AiSoS, volume 133 of EPTCS","author":"Arnold","year":"2013"},{"key":"2026032901170081100_ref022","first-page":"1","article-title":"Requirement boilerplates: Transition from manually-enforced to automatically-verifiable natural language patterns","author":"Arora"},{"key":"2026032901170081100_ref023","volume-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"2026032901170081100_ref024","first-page":"129","article-title":"Constraints specification at higher levels of abstraction","author":"Balarin"},{"key":"2026032901170081100_ref025","first-page":"1013","article-title":"Functional verification methodology based on formal interface specification and transactor generation","author":"Balarin"},{"issue":"10","key":"2026032901170081100_ref026","doi-asserted-by":"crossref","first-page":"1749","DOI":"10.1109\/TCAD.2007.895792","article-title":"Specification, synthesis and simulation of transactor processes","volume":"26","author":"Balarin","year":"2007","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"2026032901170081100_ref027","first-page":"155","article-title":"A formal approach to system level design: Metamodels and unified design environments","author":"Balarin"},{"issue":"2","key":"2026032901170081100_ref028","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1109\/MC.2006.54","article-title":"Developing applications using model-driven design environments","volume":"39","author":"Balasubramanian","year":"2006","journal-title":"IEEE Computer"},{"key":"2026032901170081100_ref029","first-page":"43","volume-title":"FASE, volume 7212 of Lecture Notes in Computer Science","author":"Bauer","year":"2012"},{"issue":"2","key":"2026032901170081100_ref030","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/s10703-012-0178-9","article-title":"Weighted modal transition systems","volume":"42","author":"Bauer","year":"2013","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"2026032901170081100_ref031","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1017\/S0960129511000697","article-title":"Extending modal transition systems with structured labels","volume":"22","author":"Bauer","year":"2012","journal-title":"Mathematical Structures in Computer Science"},{"key":"2026032901170081100_ref032","first-page":"175","article-title":"On Weak Modal Compatibility, Refinement, and the MIO Workbench","author":"Bauer","year":"2010"},{"key":"2026032901170081100_ref033","volume-title":"Architecture Modeling","author":"Baumgart","year":"2011"},{"key":"2026032901170081100_ref034","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems: International School on Formal Methods for the Design of Computer, Communication, and Software Systems","author":"Behrmann","year":"2004"},{"key":"2026032901170081100_ref035","first-page":"112","volume-title":"ICTAC, volume 5684 of Lecture Notes in Computer Science","author":"Benes","year":"2009"},{"issue":"41","key":"2026032901170081100_ref036","doi-asserted-by":"crossref","first-page":"4026","DOI":"10.1016\/j.tcs.2009.06.009","article-title":"On determinism in modal transition systems","volume":"410","author":"Benes","year":"2009","journal-title":"Theoretical Computer Science"},{"key":"2026032901170081100_ref037","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-32943-2_17","article-title":"Ensuring Reachability by Design","volume-title":"Int. Colloquium on Theoretical Aspects of Computing","author":"Caillaud","year":"2012"},{"key":"2026032901170081100_ref038","first-page":"1270","article-title":"The synchronous approach to reactive and real-time systems","author":"Benveniste","year":"1991"},{"key":"2026032901170081100_ref039","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1145\/1086228.1086276","volume-title":"EMSOFT","author":"Benveniste","year":"2005"},{"key":"2026032901170081100_ref040","first-page":"200","article-title":"Multiple viewpoint contract-based specification and design","author":"Benveniste"},{"issue":"1","key":"2026032901170081100_ref041","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1006\/inco.2000.9999","article-title":"Compositionality in dataflow synchronous languages: Specification and distributed code generation","volume":"163","author":"Benveniste","year":"2000","journal-title":"Inf Comput"},{"key":"2026032901170081100_ref042","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1201\/9781420067859-c15","volume-title":"Model-Based Design for Embedded Systems","author":"Benveniste","year":"2009"},{"key":"2026032901170081100_ref043","first-page":"7252","volume-title":"Application of interface theories to the separate compilation of synchronous programs","author":"Benveniste","year":"2012"},{"key":"2026032901170081100_ref044","first-page":"64","article-title":"The Synchronous Languages 12 years later","author":"Benveniste","year":"2003"},{"key":"2026032901170081100_ref045","volume-title":"Compositional Contract Abstraction for System Design","author":"Benveniste","year":"2014"},{"key":"2026032901170081100_ref046","first-page":"142","article-title":"A contract-based formalism for the specification of heterogeneous systems","author":"Benvenuti"},{"key":"2026032901170081100_ref047","article-title":"The effectiveness of synchronous languages for the development of safety-critical systems","volume-title":"Esterel Technologies","author":"Berry","year":"2003"},{"key":"2026032901170081100_ref048","first-page":"679","article-title":"A compositional approach on modal specifications for timed systems","author":"Bertrand","year":"2009"},{"issue":"12","key":"2026032901170081100_ref049","doi-asserted-by":"crossref","first-page":"1212","DOI":"10.1016\/j.scico.2011.01.007","article-title":"Modal event-clock specifications for timed component-based design","volume":"77","author":"Bertrand","year":"2012","journal-title":"Sci. Comput. Program"},{"key":"2026032901170081100_ref050","first-page":"152","article-title":"Refinement and consistency of timed modal specifications","author":"Bertrand","year":"2009"},{"issue":"7","key":"2026032901170081100_ref051","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1109\/2.774917","article-title":"Making components contract aware","volume":"32","author":"Beugnard","year":"1999","journal-title":"IEEE Computer"},{"key":"2026032901170081100_ref052","first-page":"148","volume-title":"Allan Ellis and Tatsuya Hagino","author":"Beyer","year":"2005"},{"issue":"2","key":"2026032901170081100_ref053","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/s00165-007-0045-4","article-title":"Interface synthesis and protocol conversion","volume":"20","author":"Bhaduri","year":"2008","journal-title":"Formal Aspects of Computing"},{"key":"2026032901170081100_ref054","first-page":"441","volume-title":"Design, Automation and Test in Europe (DATE\u201910)","author":"Bhaduri","year":"2010"},{"key":"2026032901170081100_ref055","first-page":"591","article-title":"Automatic test generation with agatha","author":"Bigot","year":"2003"},{"issue":"10","key":"2026032901170081100_ref056","doi-asserted-by":"crossref","first-page":"1315","DOI":"10.1109\/TC.2008.26","article-title":"The Algebra of Connectors \u2013 Structuring Interaction in BIP","volume":"57","author":"Bliudze","year":"2008","journal-title":"IEEE Trans. Computers"},{"key":"2026032901170081100_ref057","volume-title":"Manual for property-based synthesis tool","author":"Bloem","year":"2006"},{"key":"2026032901170081100_ref058","first-page":"425","volume-title":"CAV, volume 6174 of Lecture Notes in Computer Science","author":"Bloem","year":"2010"},{"key":"2026032901170081100_ref059","article-title":"Design Paradigms for Multi-Layer Time Coherency in ADAS and Automated Driving (MULTIC)","volume-title":"Forschungsvereinigung Automobiltechnik e.V., number 302 in FAT-Schriftenreihe. Verband der Automobilindustrie (VDA)","author":"B\u00f6de","year":"2017"},{"key":"2026032901170081100_ref060","first-page":"500","article-title":"Xeve, an ESTEREL verification environment","author":"Bouali","year":"1998"},{"issue":"1","key":"2026032901170081100_ref061","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(92)90276-L","article-title":"Graphical versus logical specifications","volume":"106","author":"Boudol","year":"1992","journal-title":"Theor. Comput. Sci"},{"key":"2026032901170081100_ref062","first-page":"152","article-title":"Non-deterministic modal interfaces","author":"Bujtor","year":"2015"},{"key":"2026032901170081100_ref063","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1016\/j.tcs.2016.06.011","article-title":"Nondeterministic modal interfaces","volume":"642","author":"Bujtor","year":"2016","journal-title":"Theor. Comput. Sci"},{"key":"2026032901170081100_ref064","first-page":"162","article-title":"Error-pruning in interface automata","author":"Bujtor"},{"key":"2026032901170081100_ref065","first-page":"42","article-title":"Failure semantics for modal transition systems","author":"Bujtor"},{"key":"2026032901170081100_ref066","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1016\/j.tcs.2015.06.047","article-title":"Error-pruning in interface automata","volume":"597","author":"Bujtor","year":"2015","journal-title":"Theor. Comput. Sci"},{"key":"2026032901170081100_ref067","doi-asserted-by":"crossref","DOI":"10.21236\/ADA256199","volume-title":"Trace Algebra for Automatic Verification of Real-Time Concurrent Systems","author":"Burch","year":"1992"},{"key":"2026032901170081100_ref068","first-page":"13","article-title":"Overcoming heterophobia: Modeling concurrency in heterogeneous systems","author":"Burch"},{"key":"2026032901170081100_ref069","doi-asserted-by":"crossref","DOI":"10.1007\/0-387-27578-9","volume-title":"Hard Real-Time Computing Systems: Predictable Scheduling Algorithms and Applications","author":"Buttazzo","year":"2005"},{"key":"2026032901170081100_ref070","author":"Caillaud","year":"2011"},{"key":"2026032901170081100_ref071","doi-asserted-by":"crossref","DOI":"10.1109\/QEST.2010.23","article-title":"Compositional design methodology with constraint Markov chains","author":"Caillaud","year":"2010"},{"key":"2026032901170081100_ref072","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/j.scico.2016.08.005","article-title":"On the verification of SCOOP programs","volume":"133","author":"Caltais","year":"2017","journal-title":"Sci. Comput. Program"},{"issue":"2","key":"2026032901170081100_ref073","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/TII.2010.2043741","article-title":"Toward correctness in the specification and handling of non-functional attributes of high-integrity real-time embedded systems","volume":"6","author":"Cancila","year":"2010","journal-title":"IEEE Transactions on Industrial Informatics"},{"issue":"1\/2","key":"2026032901170081100_ref074","article-title":"Languages and tools for hybrid systems design","volume":"1","author":"Carloni","year":"2006","journal-title":"Foundations and Trends in Electronic Design Automation"},{"key":"2026032901170081100_ref075","first-page":"137","article-title":"Contract-based analysis for verification of communication-based train control (cbtc) system","author":"Carloni","year":"2014"},{"key":"2026032901170081100_ref076","first-page":"178","article-title":"Contract modeling and verification with formalspecs verifier tool-suite \u2013 application to ansaldo sts rapid transit metro system use case","author":"Carloni","year":"2015"},{"key":"2026032901170081100_ref077","first-page":"66","article-title":"Efficient on-the-fly algorithms for the analysis of timed games","author":"Cassez","year":"2005"},{"key":"2026032901170081100_ref078","first-page":"253","volume-title":"CAV, volume 697 of Lecture Notes in Computer Science","author":"Cerans","year":"1993"},{"key":"2026032901170081100_ref079","first-page":"29","article-title":"Interface simulation distances","volume-title":"GandALF, volume 96 of EPTCS","author":"Cern\u00fd","year":"2012"},{"key":"2026032901170081100_ref080","volume-title":"A Framework for Compositional Design and Analysis of Systems","author":"Chakrabarti","year":"2007"},{"key":"2026032901170081100_ref081","first-page":"428","volume-title":"CAV, volume 2404 of Lecture Notes in Computer Science","author":"Chakrabarti","year":"2002"},{"key":"2026032901170081100_ref082","first-page":"414","article-title":"Synchronous and Bidirectional Component Interfaces","author":"Chakrabarti","year":"2002"},{"key":"2026032901170081100_ref083","first-page":"117","volume-title":"EM-SOFT, volume 2855 of Lecture Notes in Computer Science","author":"Chakrabarti","year":"2003"},{"key":"2026032901170081100_ref084","first-page":"474","volume-title":"ICALP, volume 623 of Lecture Notes in Computer Science","author":"Chang","year":"1992"},{"key":"2026032901170081100_ref085","first-page":"148","volume-title":"ESOP, volume 7211 of Lecture Notes in Computer Science","author":"Chen","year":"2012"},{"key":"2026032901170081100_ref086","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1016\/j.tcs.2014.07.018","article-title":"An algebraic theory of interface automata","volume":"549","author":"Chilton","year":"2014","journal-title":"Theoretical Computer Science"},{"key":"2026032901170081100_ref087","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/j.scico.2013.12.010","article-title":"Compositional assume-guarantee reasoning for input\/output component theories","volume":"91","author":"Chilton","year":"2014","journal-title":"Sci. Comput. Program"},{"key":"2026032901170081100_ref088","first-page":"75","volume-title":"FORMATS, volume 7595 of Lecture Notes in Computer Science","author":"Chilton","year":"2012"},{"key":"2026032901170081100_ref089","volume-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"2026032901170081100_ref090","first-page":"353","article-title":"Compositional model checking","volume-title":"LICS","author":"Clarke","year":"1989"},{"issue":"4","key":"2026032901170081100_ref091","doi-asserted-by":"crossref","first-page":"807","DOI":"10.1093\/logcom\/exm030","article-title":"A structural proof of the soundness of rely\/guarantee rules","volume":"17","author":"Coleman","year":"2007","journal-title":"J. Log. Comput"},{"key":"2026032901170081100_ref092","first-page":"238","volume-title":"POPL","author":"Cousot","year":"1977"},{"issue":"2&3","key":"2026032901170081100_ref093","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","article-title":"Abstract interpretation and application to logic programs","volume":"13","author":"Cousot","year":"1992","journal-title":"J. Log. Program"},{"issue":"4","key":"2026032901170081100_ref094","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","article-title":"Abstract Interpretation Frameworks","volume":"2","author":"Cousot","year":"1992","journal-title":"J. Log. Comput"},{"key":"2026032901170081100_ref095","doi-asserted-by":"crossref","DOI":"10.1109\/ICST.2014.50","article-title":"Compositional specifications for ioco testing","volume-title":"ICST","author":"Daca","year":"2014"},{"key":"2026032901170081100_ref096","article-title":"Dependability assessment of SOA-based CPS with contracts and model-based fault injection","volume-title":"IEEE Transactions on Industrial Informatics","author":"Lago","year":"2017"},{"key":"2026032901170081100_ref097","first-page":"118","article-title":"Controlling Speculative Design Processes Using Rich Component Models","author":"Damm"},{"issue":"1","key":"2026032901170081100_ref098","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1023\/A:1011227529550","article-title":"LSCs: Breathing life into message sequence charts","volume":"19","author":"Damm","year":"2001","journal-title":"Formal Methods in System Design"},{"key":"2026032901170081100_ref099","first-page":"1023","volume-title":"Design, Automation and Test in Europe, DATE 2011","author":"Damm","year":"2011"},{"issue":"1s","key":"2026032901170081100_ref100","doi-asserted-by":"crossref","DOI":"10.1145\/2435227.2435245","article-title":"metroII: A design environment for cyber-physical systems","volume":"12","author":"Davare","year":"2013","journal-title":"ACM Transactions on Embedded Computing Systems"},{"key":"2026032901170081100_ref101","first-page":"365","article-title":"ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems","author":"David","year":"2010"},{"key":"2026032901170081100_ref102","first-page":"91","article-title":"Timed I\/O automata: A complete specification theory for real-time systems","author":"David","year":"2010"},{"key":"2026032901170081100_ref103","first-page":"269","volume-title":"Verification: Theory and Practice, volume 2772 of Lecture Notes in Computer Science","author":"de Alfaro","year":"2003"},{"key":"2026032901170081100_ref104","first-page":"81","article-title":"Sociable Interfaces","author":"de Alfaro","year":"2005"},{"key":"2026032901170081100_ref105","first-page":"109","article-title":"Interface automata","author":"de Alfaro","year":"2001"},{"key":"2026032901170081100_ref106","first-page":"148","volume-title":"EMSOFT, volume 2211 of Lecture Notes in Computer Science","author":"de Alfaro","year":"2001"},{"key":"2026032901170081100_ref107","first-page":"108","article-title":"Timed Interfaces","author":"de Alfaro","year":"2002"},{"key":"2026032901170081100_ref108","first-page":"1","volume-title":"Modular Specification and Compositional Analysis of Stochastic Systems","author":"Delahaye","year":"2010"},{"key":"2026032901170081100_ref109","doi-asserted-by":"crossref","DOI":"10.1109\/ACSD.2010.13","article-title":"Probabilistic Contracts: A Compositional Reasoning Methodology for the Design of Stochastic Systems","author":"Delahaye","year":"2010"},{"issue":"1","key":"2026032901170081100_ref110","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10703-010-0107-8","article-title":"Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and\/or non-deterministic aspects","volume":"38","author":"Delahaye","year":"2011","journal-title":"Formal Methods in System Design"},{"key":"2026032901170081100_ref111","first-page":"203","volume-title":"FMOODS\/FORTE, volume 7273 of Lecture Notes in Computer Science","author":"Delahaye","year":"2012"},{"key":"2026032901170081100_ref112","first-page":"324","volume-title":"VMCAI, volume 6538 of Lecture Notes in Computer Science","author":"Delahaye","year":"2011"},{"issue":"3","key":"2026032901170081100_ref113","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/j.jlap.2011.10.003","article-title":"Consistency and refinement for interval markov chains","volume":"81","author":"Delahaye","year":"2012","journal-title":"J. Log. Algebr. Program"},{"issue":"5","key":"2026032901170081100_ref114","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1109\/MDT.2006.112","article-title":"A platform-based taxonomy for ESL design","volume":"23","author":"Densmore","year":"2006","journal-title":"IEEE Design and Test of Computers"},{"key":"2026032901170081100_ref115","unstructured":"AUTOSAR development cooperation\n          . Specification of Timing Extensions. http:\/\/www.autosar.org, Release 4.2.1, 2014."},{"key":"2026032901170081100_ref116","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/6874.001.0001","volume-title":"Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits","author":"Dill","year":"1989"},{"key":"2026032901170081100_ref117","first-page":"475","article-title":"MTSA: The Modal Transition System Analyser","author":"D\u2019Ippolito","year":"2008"},{"key":"2026032901170081100_ref118","first-page":"79","article-title":"Interface theories with component reuse","author":"Doyen","year":"2008"},{"key":"2026032901170081100_ref119","volume-title":"Compiling Esterel","author":"Potop-Butucaru","year":"2007"},{"key":"2026032901170081100_ref120","first-page":"371","article-title":"A compositional scheduling framework for digital avionics systems","author":"Easwaran"},{"key":"2026032901170081100_ref121","first-page":"1","volume-title":"RV, volume 4839 of Lecture Notes in Computer Science","author":"Eisner","year":"2007"},{"key":"2026032901170081100_ref122","volume-title":"Formal Syntax and Semantics of PSL \u2013 Appendix B of Accellera LRM January 2003","author":"Eisner","year":"2003"},{"key":"2026032901170081100_ref123","first-page":"27","volume-title":"CAV, volume 2725 of Lecture Notes in Computer Science","author":"Eisner","year":"2003"},{"key":"2026032901170081100_ref124","first-page":"127","article-title":"Taming heterogeneity \u2013 the ptolemy approach","author":"Eker","year":"2003"},{"key":"2026032901170081100_ref125","first-page":"58","volume":"18","author":"Engel","year":"2008","journal-title":"Assumptions\/promises \u2013 shifting the paradigm in systems-engineering"},{"key":"2026032901170081100_ref126","first-page":"251","article-title":"Formal model-based test for autosar multicore rtos","author":"Fang"},{"key":"2026032901170081100_ref127","article-title":"A compositional framework for end-to-end path delay calculation of automotive systems under different path semantics","author":"Feiertag"},{"key":"2026032901170081100_ref128","doi-asserted-by":"crossref","article-title":"BCL: a compositional contract language for embedded systems","author":"Ferrante","DOI":"10.1109\/ETFA.2014.7005353"},{"key":"2026032901170081100_ref129","doi-asserted-by":"crossref","article-title":"Monitor-based run-time contract verification of distributed systems","author":"Ferrante","DOI":"10.1109\/SIES.2014.7087332"},{"key":"2026032901170081100_ref130","volume-title":"Modal specifications are a syntactic fragment of the Mucalculus","author":"Feuillade","year":"2005"},{"key":"2026032901170081100_ref131","first-page":"297","article-title":"On correct and complete strong merging of partial behaviour models","author":"Fischbein","year":"2008"},{"key":"2026032901170081100_ref132","first-page":"1293","article-title":"The Esterel language","author":"Boussinot","year":"1991"},{"key":"2026032901170081100_ref133","volume-title":"Principles of Object-Oriented Modeling and Simulation with Modelica 2.1","author":"Fritzson","year":"2003"},{"key":"2026032901170081100_ref134","article-title":"A Refinement Checking Technique for Contract-Based Architecture Designs","author":"Gezgin"},{"key":"2026032901170081100_ref135","first-page":"323","article-title":"Automatic verification of real-time systems using Epsilon","author":"Chr","year":"1994"},{"key":"2026032901170081100_ref136","doi-asserted-by":"crossref","article-title":"Modal Contracts for Component-based Design","author":"G\u00f6ssler","DOI":"10.1109\/SEFM.2009.26"},{"key":"2026032901170081100_ref137","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/978-1-4614-3879-3_8","volume-title":"Embedded Systems Development: From Functional Models to Implementations, volume 20 of Embedded Systems","author":"Graf","year":"2014"},{"key":"2026032901170081100_ref138","first-page":"1","volume-title":"FORTE, volume 4574 of Lecture Notes in Computer Science","author":"Graf","year":"2007"},{"issue":"3","key":"2026032901170081100_ref139","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","article-title":"Model checking and modular verification","volume":"16","author":"Grumberg","year":"1994","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"2026032901170081100_ref140","doi-asserted-by":"crossref","article-title":"Metronomy: a function-architecture co-simulation framework for timing verification of cyber-physical systems","author":"Guo","DOI":"10.1145\/2656075.2656093"},{"key":"2026032901170081100_ref141","first-page":"436","article-title":"Reasoning about Safety and Progress Using Contracts","author":"Hafaiedh","year":"2010"},{"key":"2026032901170081100_ref142","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2231-4","volume-title":"Synchronous programming of reactive systems","author":"Halbwachs","year":"1993"},{"issue":"9","key":"2026032901170081100_ref143","doi-asserted-by":"crossref","first-page":"785","DOI":"10.1109\/32.159839","article-title":"Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language Lustre","volume":"18","author":"Halbwachs","year":"1992","journal-title":"IEEE Trans. Software Eng"},{"key":"2026032901170081100_ref144","first-page":"83","article-title":"Synchronous observers and the verification of reactive systems","author":"Halbwachs","year":"1993"},{"key":"2026032901170081100_ref145","first-page":"1","volume-title":"ASIAN, volume 1742 of Lecture Notes in Computer Science","author":"Halbwachs","year":"1999"},{"issue":"3","key":"2026032901170081100_ref146","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","article-title":"Statecharts: A visual formalism for complex systems","volume":"8","author":"Harel","year":"1987","journal-title":"Sci. Comput. Program"},{"key":"2026032901170081100_ref147","first-page":"477","volume-title":"SOFSEM, volume 5901 of Lecture Notes in Computer Science","author":"Harel","year":"2010"},{"key":"2026032901170081100_ref148","first-page":"279","volume-title":"EMSOFT","author":"Harel","year":"2011"},{"key":"2026032901170081100_ref149","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19029-2","volume-title":"Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine","author":"Harel","year":"2003"},{"issue":"7","key":"2026032901170081100_ref150","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/2209249.2209270","article-title":"Behavioral programming","volume":"55","author":"Harel","year":"2012","journal-title":"Commun. ACM"},{"key":"2026032901170081100_ref151","first-page":"171","article-title":"Behavioral programming, decentralized control, and multiple time scales","author":"Harel","year":"2011"},{"key":"2026032901170081100_ref152","first-page":"477","volume-title":"Logic and Models for Verification and Specification of Concurrent Systems, volume F13 of NATO ASI Series","author":"Harel","year":"1985"},{"key":"2026032901170081100_ref153","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1109\/DATE.2008.4484733","article-title":"Software Components for Reliable Automotive Systems","volume-title":"Design, Automation and Test in Europe, 2008. DATE \u201908","author":"Heinecke","year":"2008"},{"key":"2026032901170081100_ref154","first-page":"380","article-title":"Independent implementability of viewpoints","author":"Henzinger","year":"2012"},{"issue":"10","key":"2026032901170081100_ref155","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Commun. ACM"},{"key":"2026032901170081100_ref156","author":"Hu","year":"1998"},{"key":"2026032901170081100_ref157","first-page":"165","article-title":"Deadline analysis of AUTOSAR OS periodic tasks in the presence of interrupts","author":"Huang","year":"2013"},{"key":"2026032901170081100_ref158","unstructured":"INCOSE\n          . Incose systems engineering handbook, 2010. http:\/\/www.incose.org\/ProductsPubs\/products\/sehandbook.aspx."},{"key":"2026032901170081100_ref159","first-page":"321","article-title":"Specification and design of (parallel) programs","volume-title":"IFIP Congress","author":"Jones","year":"1983"},{"key":"2026032901170081100_ref160","first-page":"1","volume-title":"Programming Methodology","author":"Jones","year":"2000"},{"issue":"5","key":"2026032901170081100_ref161","doi-asserted-by":"crossref","first-page":"972","DOI":"10.1016\/j.jlamp.2016.01.002","article-title":"Possible values: Exploring a concept for concurrency","volume":"85","author":"Jones","year":"2016","journal-title":"J. Log. Algebr. Meth. Program"},{"issue":"3","key":"2026032901170081100_ref162","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/s00165-014-0310-2","article-title":"Balancing expressiveness in formal approaches to concurrency","volume":"27","author":"Jones","year":"2015","journal-title":"Formal Asp. Comput"},{"key":"2026032901170081100_ref163","volume-title":"Prentice Hall International Series in Computer Science","author":"Jones","year":"1991"},{"key":"2026032901170081100_ref164","first-page":"266","volume-title":"Logic in Computer Science (LICS)","author":"Jonsson","year":"1991"},{"key":"2026032901170081100_ref165","first-page":"558","volume":"18","author":"Josko","year":"2008","journal-title":"Designing embedded systems using heterogeneous rich components"},{"issue":"4","key":"2026032901170081100_ref166","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1016\/j.jlap.2012.03.008","article-title":"Modal transition systems with weight intervals","volume":"81","author":"Juhl","year":"2012","journal-title":"J. Log. Algebr. Program"},{"key":"2026032901170081100_ref167","first-page":"471","article-title":"The Semantics of Simple Language for Parallel Programming","volume-title":"IFIP Congress","author":"Kahn","year":"1974"},{"key":"2026032901170081100_ref168","volume-title":"Introduction to Simulink with Engineering Applications","author":"Karris","year":"2006"},{"issue":"1","key":"2026032901170081100_ref169","doi-asserted-by":"crossref","DOI":"10.1109\/JPROC.2002.805824","article-title":"Model-integrated development of embedded software","volume":"91","author":"Karsai","year":"2003","journal-title":"Proceedings of the IEEE"},{"key":"2026032901170081100_ref170","first-page":"381","volume-title":"COMPOS, volume 1536 of Lecture Notes in Computer Science","author":"Kupferman","year":"1997"},{"issue":"3","key":"2026032901170081100_ref171","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/s10617-010-9055-1","article-title":"Analytic real-time analysis and timed automata: a hybrid methodology for the performance analysis of embedded real-time systems","volume":"14","author":"Lampka","year":"2010","journal-title":"Design Automation for Embedded Systems"},{"issue":"3","key":"2026032901170081100_ref172","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/s10009-012-0257-7","article-title":"Component-based system design: analytic real-time interfaces for state-based component implementations","volume":"15","author":"Lampka","year":"2013","journal-title":"STTT"},{"issue":"2","key":"2026032901170081100_ref173","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","article-title":"Proving the correctness of multiprocess programs","volume":"3","author":"Lamport","year":"1977","journal-title":"IEEE Trans. Software Eng"},{"key":"2026032901170081100_ref174","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1016\/j.tcs.2013.08.015","article-title":"Robust synthesis for real-time systems","volume":"515","author":"Larsen","year":"2014","journal-title":"Theor. Comput. Sci"},{"key":"2026032901170081100_ref175","first-page":"232","volume-title":"Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science","author":"Larsen","year":"1989"},{"key":"2026032901170081100_ref176","first-page":"82","volume-title":"FM, volume 4085 of Lecture Notes in Computer Science","author":"Larsen","year":"2006"},{"key":"2026032901170081100_ref177","first-page":"64","article-title":"Modal I\/O Automata for Interface and Product Line Theories","author":"Larsen","year":"2007"},{"key":"2026032901170081100_ref178","first-page":"105","article-title":"On Modal Refinement and Consistency","author":"Larsen","year":"2007"},{"key":"2026032901170081100_ref179","first-page":"17","article-title":"A constraint oriented proof methodology based on modal transition systems","author":"Larsen","year":"1995"},{"key":"2026032901170081100_ref180","first-page":"203","article-title":"A Modal Process Logic","author":"Larsen","year":"1988"},{"key":"2026032901170081100_ref181","first-page":"108","article-title":"Equation solving using modal transition systems","author":"Larsen","year":"1990"},{"key":"2026032901170081100_ref182","article-title":"Refinement-based synthesis of correct contract model decompositions","author":"Thieu Le"},{"key":"2026032901170081100_ref183","article-title":"A tag contract framework for heterogeneous systems","author":"Thieu Le"},{"key":"2026032901170081100_ref184","first-page":"186","article-title":"Tag machines for modeling heterogeneous systems","author":"Thieu Le"},{"issue":"2","key":"2026032901170081100_ref185","article-title":"Contract-based requirement modularization via synthesis of correct decompositions","volume":"15","author":"Hoa Le","year":"2016","journal-title":"ACM Transactions on Embedded Computing Systems"},{"key":"2026032901170081100_ref186","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/j.scico.2015.06.004","article-title":"A tag contract framework for modeling heterogeneous systems","volume":"115-116","author":"Hoa Le","year":"2016","journal-title":"Science of Computer Programming"},{"issue":"11","key":"2026032901170081100_ref187","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1109\/2.963443","article-title":"Composing domain-specific design environments","volume":"34","author":"L\u00e9deczi","year":"2001","journal-title":"IEEE Computer"},{"key":"2026032901170081100_ref188","article-title":"The generic modeling environment","author":"Ledeczi"},{"key":"2026032901170081100_ref189","volume-title":"Real-Time Systems","author":"Liu","year":"2000"},{"key":"2026032901170081100_ref190","first-page":"665","article-title":"Modular scheduling of distributed heterogeneous time-triggered automotive systems","author":"Lukasiewycz"},{"issue":"3","key":"2026032901170081100_ref191","article-title":"Modal interface automata","volume":"9","author":"L\u00fcttgen","year":"2013","journal-title":"Logical Methods in Computer Science"},{"key":"2026032901170081100_ref192","article-title":"Richer interface automata with optimistic and pessimistic compatibility","volume":"66","author":"L\u00fcttgen","year":"2013","journal-title":"ECEASST"},{"key":"2026032901170081100_ref193","first-page":"187","volume-title":"CONCUR, volume 2761 of Lecture Notes in Computer Science","author":"Lynch","year":"2003"},{"issue":"1","key":"2026032901170081100_ref194","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/0890-5401(89)90066-7","article-title":"A proof of the kahn principle for input\/output automata","volume":"82","author":"Lynch","year":"1989","journal-title":"Inf. Comput"},{"key":"2026032901170081100_ref195","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems \u2013 specification","author":"Manna","year":"1992"},{"key":"2026032901170081100_ref196","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems: Safety","author":"Manna","year":"1995"},{"issue":"4","key":"2026032901170081100_ref197","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1023\/A:1008311720696","article-title":"Synthesis of Discrete-Event Controllers Based on the Signal Environment","volume":"10","author":"Marchand","year":"2000","journal-title":"Discrete Event Dynamic Systems"},{"issue":"8","key":"2026032901170081100_ref198","doi-asserted-by":"crossref","first-page":"729","DOI":"10.1109\/32.879811","article-title":"Incremental Design of a Power Transformer Station Controller Using a Controller Synthesis Methodology","volume":"26","author":"Marchand","year":"2000","journal-title":"IEEE Trans. Software Eng"},{"key":"2026032901170081100_ref199","first-page":"91","article-title":"A framework for compositional and hierarchical real-time scheduling","author":"Marimuthu"},{"issue":"10","key":"2026032901170081100_ref200","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":"IEEE Computer"},{"key":"2026032901170081100_ref201","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-92145-5","volume-title":"Touch of Class: Learning to Program Well Using Object Technology and Design by Contract","author":"Meyer","year":"2009"},{"key":"2026032901170081100_ref202","unstructured":"Antoine\n              Min\u00e9\n            \n          . Weakly Relational Numerical Abstract Domains. Phd, Ecole Normale Sup\u00e9rieure, d\u00e9partement d\u2019informatique, Dec2004. http:\/\/www.di.ens.fr\/~mine\/these\/these-color.pdf."},{"issue":"4","key":"2026032901170081100_ref203","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1002\/(SICI)1520-6858(1998)1:4<267::AID-SYS3>3.0.CO;2-D","article-title":"Architecting Principles for Systems of Systems","volume":"1","author":"Maier","year":"1998","journal-title":"Systems Engineering"},{"issue":"13-14","key":"2026032901170081100_ref204","doi-asserted-by":"crossref","first-page":"1907","DOI":"10.1016\/S0167-8191(99)00070-8","article-title":"Advances in the dataflow computational model","volume":"25","author":"Najjar","year":"1999","journal-title":"Parallel Computing"},{"key":"2026032901170081100_ref205","volume-title":"Process Spaces and the Formal Verification of Asynchronous Circuits","author":"Negulescu","year":"1998"},{"key":"2026032901170081100_ref206","first-page":"1305","article-title":"The synchronous data flow programming language Lustre","author":"Halbwachs","year":"1991"},{"issue":"12","key":"2026032901170081100_ref207","doi-asserted-by":"crossref","first-page":"3329","DOI":"10.1109\/JSEN.2012.2211098","article-title":"Methodology for the design of analog integrated interfaces using contracts","volume":"12","author":"Nuzzo","year":"2012","journal-title":"IEEE Sensors Journal"},{"key":"2026032901170081100_ref208","volume-title":"System modeling language specification v1.1","author":"Object Management Group (OMG)","year":"2008"},{"key":"2026032901170081100_ref209","volume-title":"Version 2.0. OMG Available Specification formal\/06-05-01, Object Management Group","author":"Object constraint language","year":"2006"},{"key":"2026032901170081100_ref210","volume-title":"1850-2010 \u2013 IEEE Standard for Property Specification Language (PSL)","author":"The Design Automation Standards Committee of the IEEE Computer Society","year":"2010"},{"key":"2026032901170081100_ref211","article-title":"The Architecture Analysis and Design Language (AADL): An Introduction","volume-title":"Software Engineering Institute (SEI) Technical Note, CMU\/SEI-2006-TN-011","author":"Hudak","year":"2006"},{"key":"2026032901170081100_ref212","volume-title":"Department of Electrical Engineering and Computer Sciences","author":"Passerone","year":"2004"},{"key":"2026032901170081100_ref213","first-page":"132","article-title":"Convertibility verification and converter synthesis: Two faces of the same coin","author":"Passerone"},{"issue":"1","key":"2026032901170081100_ref214","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10703-006-0024-z","article-title":"Refinement preserving approximations for the design and verification of heterogeneous systems","volume":"31","author":"Passerone","year":"2007","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"2026032901170081100_ref215","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1109\/MDT.2009.64","article-title":"Metamodels in Europe: Languages, tools, and applications","volume":"26","author":"Passerone","year":"2009","journal-title":"IEEE Design and Test of Computers"},{"key":"2026032901170081100_ref216","first-page":"1321","article-title":"Programming real-time applications with Signal","author":"Guernic","year":"1991"},{"key":"2026032901170081100_ref217","first-page":"111","article-title":"Modeling a BSG-E automotive system with the timing augmented description language","author":"Peraldi-Frati","year":"2012"},{"key":"2026032901170081100_ref218","first-page":"1","article-title":"Composing heterogeneous components for system-wide performance analysis","author":"Perathoner"},{"issue":"1","key":"2026032901170081100_ref219","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1145\/1967021.1967029","article-title":"CARTS: a tool for compositional analysis of real-time systems","volume":"8","author":"Linh","year":"2011","journal-title":"SIGBED Review"},{"key":"2026032901170081100_ref220","volume-title":"Property simulation","author":"Pill","year":"2005"},{"issue":"3","key":"2026032901170081100_ref221","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1145\/1142980.1142982","article-title":"System level design paradigms: Platform-based design and communication synthesis","volume":"11","author":"Pinto","year":"2006","journal-title":"ACM Transactions on Design Automation of Electronic Systems"},{"key":"2026032901170081100_ref222","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-48003-9","volume-title":"Advanced Model-Based Engineering of Embedded Systems: Extensions of the SPES 2020 Methodology","author":"Pohl","year":"2016"},{"key":"2026032901170081100_ref223","volume-title":"Visual modeling with Rational Rose 2000 and UML (2nd ed.)","author":"Terry Quatrani","year":"2000"},{"key":"2026032901170081100_ref224","article-title":"Quotient de sp\u00e9cifications pour la r\u00e9utilisation de composants","volume-title":"Ecole doctorale Matisse, universit\u00e9 de Rennes 1","author":"Raclet","year":"2007"},{"key":"2026032901170081100_ref225","article-title":"Residual for Component Specifications","author":"Raclet","year":"2007"},{"key":"2026032901170081100_ref226","first-page":"87","article-title":"Modal interfaces: Unifying interface automata and modal specifications","author":"Raclet"},{"issue":"1-2","key":"2026032901170081100_ref227","doi-asserted-by":"crossref","first-page":"119","DOI":"10.3233\/FI-2011-416","article-title":"A modal interface theory for component-based design","volume":"108","author":"Raclet","year":"2011","journal-title":"Fundamenta Informaticae"},{"key":"2026032901170081100_ref228","doi-asserted-by":"crossref","DOI":"10.1109\/ACSD.2009.22","article-title":"Why are modalities good for interface theories?","author":"Raclet","year":"2009"},{"key":"2026032901170081100_ref229","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-54862-8_15","article-title":"Basic problems in multi-view modeling","volume-title":"TACAS","author":"Reineke","year":"2014"},{"key":"2026032901170081100_ref230","first-page":"270","article-title":"Contracts for schedulability analysis","author":"Reinkemeier","year":"2015"},{"key":"2026032901170081100_ref231","first-page":"181","article-title":"Compositional timing analysis of real-time systems based on resource segregation abstraction","author":"Reinkemeier","year":"2013"},{"key":"2026032901170081100_ref232","unstructured":"Philipp\n              Reinkemeier\n             and IngoStierand. Real-Time Contracts \u2013 A Contract Theory Considering Resource Supplies and Demands. Reports of SFB\/TR 14 AVACS 100, SFB\/TR 14 AVACS, July2014. http:\/\/www.avacs.org."},{"key":"2026032901170081100_ref233","volume-title":"Evaluation of Architectural Frameworks Supporting Contract-Based Specification","author":"Payne","year":"2010"},{"key":"2026032901170081100_ref234","first-page":"19","article-title":"Assigning meaning to programs","author":"Floyd","year":"1967"},{"issue":"3","key":"2026032901170081100_ref235","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/MDT.2009.62","article-title":"Metamodeling: An emerging representation paradigm for systemlevel design","volume":"26","author":"Sangiovanni-Vincentelli","year":"2009","journal-title":"IEEE Design and Test of Computers"},{"issue":"3","key":"2026032901170081100_ref236","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":"European Journal of Control"},{"key":"2026032901170081100_ref237","first-page":"25","article-title":"Model-driven engineering","volume-title":"IEEE Computer","author":"Schmidt","year":"2006"},{"issue":"2-3","key":"2026032901170081100_ref238","first-page":"101","article-title":"Real Time Scheduling Theory: A Historical Perspective","volume":"28","author":"Sha","year":"2004","journal-title":"RealTime Systems"},{"key":"2026032901170081100_ref239","first-page":"127","article-title":"Checking safety properties using induction and a sat-solver","author":"Sheeran","year":"2000"},{"issue":"1","key":"2026032901170081100_ref240","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1008725524946","article-title":"A tutorial on st\u00e5lmarck\u2019s proof procedure for propositional logic","volume":"16","author":"Sheeran","year":"2000","journal-title":"Formal Methods in System Design"},{"key":"2026032901170081100_ref241","first-page":"57","article-title":"Compositional real-time scheduling framework","author":"Shin"},{"key":"2026032901170081100_ref242","doi-asserted-by":"crossref","article-title":"Existential Live Sequence Charts Revisited","author":"Sibay","DOI":"10.1145\/1368088.1368095"},{"key":"2026032901170081100_ref243","first-page":"1","volume-title":"Petri Nets, volume 5606 of Lecture Notes in Computer Science","author":"Sifakis","year":"2009"},{"key":"2026032901170081100_ref244","first-page":"369","volume-title":"FSTTCS, volume 206 of Lecture Notes in Computer Science","author":"Stark","year":"1985"},{"key":"2026032901170081100_ref245","first-page":"206","article-title":"Virtual integration of real-time systems based on resource segregation abstraction","author":"Stierand","year":"2014"},{"key":"2026032901170081100_ref246","first-page":"130","article-title":"Real-time scheduling interfaces and contracts for the design of distributed embedded systems","author":"Stierand"},{"key":"2026032901170081100_ref247","first-page":"83","volume-title":"Advances in Real-Time Systems (to Georg F\u00e4rber on the occasion of his appointment as Professor Emeritus at TU M\u00fcnchen after leading the Lehrstuhl f\u00fcr Realzeit-Computersysteme for 34 illustrious years)","author":"Stoimenov","year":"2012"},{"key":"2026032901170081100_ref248","volume-title":"AIAA Infotech Aerospace 2010","author":"Storm","year":"2010"},{"key":"2026032901170081100_ref249","first-page":"34","article-title":"Real-time interfaces for composing real-time systems","author":"Thiele","year":"2006"},{"key":"2026032901170081100_ref250","first-page":"67","article-title":"On relational interfaces","author":"Tripakis","year":"2009"},{"issue":"4","key":"2026032901170081100_ref251","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/1985342.1985345","article-title":"A theory of synchronous relational interfaces","volume":"33","author":"Tripakis","year":"2011","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"2026032901170081100_ref252","first-page":"43","article-title":"Merging partial behavioural models","author":"Uchitel","year":"2004"},{"key":"2026032901170081100_ref253","first-page":"86","article-title":"Compositional testing with ioco","author":"van der Bijl","year":"2003"},{"key":"2026032901170081100_ref254","first-page":"243","article-title":"Interface-based design of real-time systems with hierarchical scheduling","author":"Wandeler"},{"key":"2026032901170081100_ref255","volume-title":"The Object Constraint Language: Getting Your Models Ready for MDA","author":"Warmer","year":"2003","edition":"2nd"},{"key":"2026032901170081100_ref256","volume-title":"Department of Computer Science","author":"Wolf","year":"1995"}],"container-title":["Foundations and Trends\u00ae in Electronic Design Automation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/fteda\/article-pdf\/12\/2-3\/124\/11443627\/1000000053en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/fteda\/article-pdf\/12\/2-3\/124\/11443627\/1000000053en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T05:17:35Z","timestamp":1774761455000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/fteda\/article\/12\/2-3\/124\/1320867\/Contracts-for-System-Design"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3,28]]},"references-count":256,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2018,3,28]]}},"URL":"https:\/\/doi.org\/10.1561\/1000000053","relation":{},"ISSN":["1551-3939","1551-3947"],"issn-type":[{"value":"1551-3939","type":"print"},{"value":"1551-3947","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,3,28]]}}}