{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:52:47Z","timestamp":1780116767072,"version":"3.54.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T00:00:00Z","timestamp":1570492800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>Contract models have been proposed to promote and facilitate reuse and distributed development. In this paper, we cast contract models into a coherent formalism used to derive general results about the properties of their operators. We study several extensions of the basic model, including the distinction between weak and strong assumptions and maximality of the specification. We then analyze the disjunction and conjunction operators, and show how they can be broken up into a sequence of simpler operations. This leads to the definition of a new contract viewpoint merging operator, which better captures the design intent in contrast to the more traditional conjunction. The adjoint operation, which we call separation, can be used to re-partition the specification into different viewpoints. We show the symmetries of these operations with respect to composition and quotient.<\/jats:p>","DOI":"10.1145\/3358216","type":"journal-article","created":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T13:13:05Z","timestamp":1570713185000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Coherent Extension, Composition, and Merging Operators in Contract Models for System Design"],"prefix":"10.1145","volume":"18","author":[{"given":"Roberto","family":"Passerone","sequence":"first","affiliation":[{"name":"University of Trento, Trento, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"\u00cd\u00f1igo","family":"\u00cdncer Romeo","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, CA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alberto L.","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, CA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2820"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28872-2_3"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1376804.1376811"},{"key":"e_1_2_1_5_1","volume-title":"Formal Methods for Components and Objects, 6th International Symposium (FMCO\u201907)","author":"Benveniste Albert","year":"2007","unstructured":"Albert Benveniste , Beno\u00eet Caillaud , Alberto Ferrari , Leonardo Mangeruca , Roberto Passerone , and Christos Sofronis . 2008. Multiple viewpoint contract-based specification and design . In Formal Methods for Components and Objects, 6th International Symposium (FMCO\u201907) , Amsterdam, The Netherlands, October 24--26, 2007 , Revised Papers, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Lecture Notes in Computer Science, Vol. 5382 . Springer Verlag , Berlin Heidelberg, 200--225. Albert Benveniste, Beno\u00eet Caillaud, Alberto Ferrari, Leonardo Mangeruca, Roberto Passerone, and Christos Sofronis. 2008. Multiple viewpoint contract-based specification and design. In Formal Methods for Components and Objects, 6th International Symposium (FMCO\u201907), Amsterdam, The Netherlands, October 24--26, 2007, Revised Papers, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Lecture Notes in Computer Science, Vol. 5382. Springer Verlag, Berlin Heidelberg, 200--225."},{"key":"e_1_2_1_6_1","volume-title":"Larsen","author":"Benveniste Albert","year":"2018","unstructured":"Albert Benveniste , Beno\u00eet Caillaud , Dejan Nickovic , Roberto Passerone , Jean-Baptiste Raclet , Philipp Reinkemeier , Alberto L. Sangiovanni-Vincentelli , Werner Damm , Thomas A. Henzinger , and Kim G . Larsen . 2018 . Contracts for System Design. Foundations and Trends in Electronic Design Automation , Vol. 12 . now publishers. Albert Benveniste, Beno\u00eet Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, Philipp Reinkemeier, Alberto L. Sangiovanni-Vincentelli, Werner Damm, Thomas A. Henzinger, and Kim G. Larsen. 2018. Contracts for System Design. Foundations and Trends in Electronic Design Automation, Vol. 12. now publishers."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/FDL.2008.4641436"},{"key":"e_1_2_1_8_1","volume-title":"Sangiovanni Vincentelli","author":"Benvenuti Luca","year":"2008","unstructured":"Luca Benvenuti , Alberto Ferrari , Emanuele Mazzi , and Alberto L . Sangiovanni Vincentelli . 2008 . Contract-based design for computation and verification of a closed-loop hybrid system. In Hybrid Systems: Computation and Control, Magnus Egerstedt and Bud Mishra (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg, 58--71. Luca Benvenuti, Alberto Ferrari, Emanuele Mazzi, and Alberto L. Sangiovanni Vincentelli. 2008. Contract-based design for computation and verification of a closed-loop hybrid system. In Hybrid Systems: Computation and Control, Magnus Egerstedt and Bud Mishra (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 58--71."},{"key":"e_1_2_1_9_1","volume-title":"Compatibility in a multi-component environment. Theoretical Computer Science 484 (May","author":"Carmona Josep","year":"2013","unstructured":"Josep Carmona and Jetty Kleijn . 2013. Compatibility in a multi-component environment. Theoretical Computer Science 484 (May 2013 ), 1--15. Josep Carmona and Jetty Kleijn. 2013. Compatibility in a multi-component environment. Theoretical Computer Science 484 (May 2013), 1--15."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45212-6_9"},{"key":"e_1_2_1_11_1","volume-title":"An algebraic theory of interface automata. Theoretical Computer Science 549 (September","author":"Chilton Chris","year":"2014","unstructured":"Chris Chilton , Bengt Jonsson , and Marta Kwiatkowska . 2014. An algebraic theory of interface automata. Theoretical Computer Science 549 (September 2014 ), 146--174. Chris Chilton, Bengt Jonsson, and Marta Kwiatkowska. 2014. An algebraic theory of interface automata. Theoretical Computer Science 549 (September 2014), 146--174."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.06.011"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2011.5763167"},{"key":"e_1_2_1_14_1","unstructured":"Werner Damm Angelika Votintseva Alexander Metzner Bernhard Josko Thomas Peikenkamp and Eckard B\u00f6de. 2005. Boosting re-use of embedded automotive applications through rich components. In Foundations of Interface Technologies (FIT\u201905).  Werner Damm Angelika Votintseva Alexander Metzner Bernhard Josko Thomas Peikenkamp and Eckard B\u00f6de. 2005. Boosting re-use of embedded automotive applications through rich components. In Foundations of Interface Technologies (FIT\u201905)."},{"key":"e_1_2_1_15_1","volume-title":"Henzinger","author":"de Alfaro Luca","year":"2001","unstructured":"Luca de Alfaro and Thomas A . Henzinger . 2001 . Interface automata. In Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering. ACM Press , 109--120. Luca de Alfaro and Thomas A. Henzinger. 2001. Interface automata. In Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering. ACM Press, 109--120."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_17_1","volume-title":"Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits","author":"Dill David L.","unstructured":"David L. Dill . 1989. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits . MIT Press . David L. Dill. 1989. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press."},{"key":"e_1_2_1_18_1","volume-title":"Contract-based modeling and verification of timed safety requirements within SysML. Software 8 Systems Modeling","author":"Dragomir Iulia","year":"2015","unstructured":"Iulia Dragomir , Iulian Ober , and Christian Percebois . 2015. Contract-based modeling and verification of timed safety requirements within SysML. Software 8 Systems Modeling ( 2015 ), 1--38. Iulia Dragomir, Iulian Ober, and Christian Percebois. 2015. Contract-based modeling and verification of timed safety requirements within SysML. Software 8 Systems Modeling (2015), 1--38."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_20_1","volume-title":"Embedded Systems Development: From Functional Models to Implementations, Alberto L. Sangiovanni-Vincentelli, Haibo Zeng, Marco Di Natale, and Peter Marwedel (Eds.). Embedded Systems","author":"Graf Susanne","unstructured":"Susanne Graf , Roberto Passerone , and Sophie Quinton . 2014. Contract-based reasoning for component systems with rich interactions . In Embedded Systems Development: From Functional Models to Implementations, Alberto L. Sangiovanni-Vincentelli, Haibo Zeng, Marco Di Natale, and Peter Marwedel (Eds.). Embedded Systems , Vol. 20 . Springer New York , Chapter 8, 139--154. Susanne Graf, Roberto Passerone, and Sophie Quinton. 2014. Contract-based reasoning for component systems with rich interactions. In Embedded Systems Development: From Functional Models to Implementations, Alberto L. Sangiovanni-Vincentelli, Haibo Zeng, Marco Di Natale, and Peter Marwedel (Eds.). Embedded Systems, Vol. 20. Springer New York, Chapter 8, 139--154."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081713"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2018.8556872"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78970"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_7"},{"key":"e_1_2_1_26_1","volume-title":"16th European Symposium on Programming, (ESOP\u201907)","volume":"4421","author":"Larsen Kim G.","year":"2007","unstructured":"Kim G. Larsen , Ulrik Nyman , and Andrzej Wasowski . 2007 . Modal I\/O automata for interface and product line theories. In Programming Languages and Systems , 16th European Symposium on Programming, (ESOP\u201907) (Lecture Notes in Computer Science) , Vol. 4421 . Springer, 64--79. Kim G. Larsen, Ulrik Nyman, and Andrzej Wasowski. 2007. Modal I\/O automata for interface and product line theories. In Programming Languages and Systems, 16th European Symposium on Programming, (ESOP\u201907) (Lecture Notes in Computer Science), Vol. 4421. Springer, 64--79."},{"key":"e_1_2_1_27_1","volume-title":"A tag contract framework for modeling heterogeneous systems. Science of Computer Programming 115--116","author":"Thieu Le Hoa Thi","year":"2016","unstructured":"Hoa Thi Thieu Le , Roberto Passerone , Uli Fahrenberg , and Axel Legay . 2016. A tag contract framework for modeling heterogeneous systems. Science of Computer Programming 115--116 ( 2016 ), 225--246. Hoa Thi Thieu Le, Roberto Passerone, Uli Fahrenberg, and Axel Legay. 2016. A tag contract framework for modeling heterogeneous systems. Science of Computer Programming 115--116 (2016), 225--246."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.736561"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-004-0043-8"},{"key":"e_1_2_1_30_1","volume-title":"Categories for the Working Mathematician","author":"Lane Saunders Mac","unstructured":"Saunders Mac Lane . 1998. Categories for the Working Mathematician ( 2 nd ed.). Vol. 5 . New York, NY : Springer . xii + 314 pages. Saunders Mac Lane. 1998. Categories for the Working Mathematician (2nd ed.). Vol. 5. New York, NY: Springer. xii + 314 pages.","edition":"2"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/SIES.2013.6601484"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_16"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/2362088.2362095"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2009.22"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985342.1985345"},{"key":"e_1_2_1_39_1","volume-title":"Lee","author":"Tripakis Stavros","year":"2013","unstructured":"Stavros Tripakis , Christos Stergiou , Manfred Broy , and Edward A . Lee . 2013 . Error-completion in interface theories. In Model Checking Software, Ezio Bartocci and C. R. Ramakrishnan (Eds.). Lecture Notes in Computer Science, Vol. 7976 . Springer Berlin Heidelberg , 358--375. Stavros Tripakis, Christos Stergiou, Manfred Broy, and Edward A. Lee. 2013. Error-completion in interface theories. In Model Checking Software, Ezio Bartocci and C. R. Ramakrishnan (Eds.). Lecture Notes in Computer Science, Vol. 7976. Springer Berlin Heidelberg, 358--375."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358216","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358216","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:07Z","timestamp":1750202587000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358216"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,8]]},"references-count":37,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3358216"],"URL":"https:\/\/doi.org\/10.1145\/3358216","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,8]]},"assertion":[{"value":"2019-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-10-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}