{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T11:23:49Z","timestamp":1780053829873,"version":"3.54.0"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","funder":[{"name":"National Science Foundation","award":["2514683, 2514748, 2448886"],"award-info":[{"award-number":["2514683, 2514748, 2448886"]}]},{"DOI":"10.13039\/100000104","name":"National Aeronautics and Space Administration","doi-asserted-by":"crossref","award":["80NM0018D0004"],"award-info":[{"award-number":["80NM0018D0004"]}],"id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>\n            The design of complex cyber-physical system architectures is often hierarchical. System specifications are mapped to an implementation layer via a stepwise refinement process involving multiple intermediate layers. These layers may capture different functionalities, and the orchestration of a variety of heterogeneous techniques suited to each layer may be required to achieve the overall design objectives. Due to their heterogeneity, ensuring\n            <jats:italic toggle=\"yes\">traceability<\/jats:italic>\n            and\n            <jats:italic toggle=\"yes\">verifiability<\/jats:italic>\n            of such architectures is a challenging problem. In this article, we present a correct-by-construction methodology for designing heterogeneous layered architectures. We capture the specifications at each layer with\n            <jats:italic toggle=\"yes\">assume-guarantee contracts<\/jats:italic>\n            , a specification paradigm which can encompass a variety of modeling formalisms. We then use the notion of\n            <jats:italic toggle=\"yes\">contract embeddings<\/jats:italic>\n            to define\n            <jats:italic toggle=\"yes\">specification refinement<\/jats:italic>\n            , rigorously and traceably mapping specifications across layers modeled with heterogeneous formalisms. We instantiate our methodology on the design of\n            <jats:italic toggle=\"yes\">layered control architectures<\/jats:italic>\n            (LCAs), resulting in a novel approach that can verifiably orchestrate domain-specific techniques to satisfy both\n            <jats:italic toggle=\"yes\">global<\/jats:italic>\n            planning and\n            <jats:italic toggle=\"yes\">local<\/jats:italic>\n            safety requirements. In the context of LCAs, we derive necessary conditions for correct specification refinement and results for compositional realization of control safety specifications. We illustrate our design methodology on a motivating example and a case study derived from robotic mission planning and control.\n          <\/jats:p>","DOI":"10.1145\/3764587","type":"journal-article","created":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T11:32:18Z","timestamp":1756380738000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Contract Embeddings for Layered Control Architectures"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6871-2010","authenticated-orcid":false,"given":"Nikhil Vijay","family":"Naik","sequence":"first","affiliation":[{"name":"Ming Hsieh Department of Electrical and Computer Engineering, University of Southern California","place":["Los Angeles, United States"]},{"name":"AI Systems Engineering, RTX Technology Research Center","place":["Los Angeles, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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","place":["Pasadena, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2984-0364","authenticated-orcid":false,"given":"Pierluigi","family":"Nuzzo","sequence":"additional","affiliation":[{"name":"Department of Electrical Engineering and Computer Sciences, University of California Berkeley","place":["Berkeley, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,9,26]]},"reference":[{"key":"e_1_3_4_2_2","doi-asserted-by":"publisher","DOI":"10.23919\/ECC.2019.8796030"},{"key":"e_1_3_4_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2016.2638961"},{"key":"e_1_3_4_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_3_4_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1193228"},{"key":"e_1_3_4_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2017.8263977"},{"key":"e_1_3_4_7_2","doi-asserted-by":"publisher","DOI":"10.1561\/1000000053"},{"key":"e_1_3_4_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2010.5509503"},{"key":"e_1_3_4_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/JRA.1986.1087032"},{"key":"e_1_3_4_10_2","volume-title":"The Engineering Design of Systems: Models and Methods","author":"Buede Dennis M.","year":"2024","unstructured":"Dennis M. Buede and William D. Miller. 2024. The Engineering Design of Systems: Models and Methods. John Wiley and Sons."},{"key":"e_1_3_4_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2006.887322"},{"key":"e_1_3_4_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_3_4_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_4_14_2","first-page":"854","volume-title":"Int. Joint Conf. Artificial Intelligence","author":"Giacomo Giuseppe De","year":"2013","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. In Int. Joint Conf. Artificial Intelligence. ACM, 854\u2013860."},{"key":"e_1_3_4_15_2","first-page":"1","volume-title":"IEEE Aerospace Conf.","author":"Croix Jean-Pierre de la","year":"2024","unstructured":"Jean-Pierre de la Croix, Federico Rossi, Roland Brockers, Dustin Aguilar, Keenan Albee, Elizabeth Boroson, Abhishek Cauligi, Jeff Delaune, Robert Hewitt, Dima Kogan, et\u00a0al. 2024. Multi-agent autonomy for space exploration on the CADRE lunar technology demonstration. In IEEE Aerospace Conf. IEEE, 1\u201314."},{"key":"e_1_3_4_16_2","volume-title":"Galois Connections and Applications","author":"Denecke Klaus","year":"2013","unstructured":"Klaus Denecke, Marcel Ern\u00e9, and Shelly L. Wismath. 2013. Galois Connections and Applications. Springer Science and Business Media."},{"issue":"83","key":"e_1_3_4_17_2","first-page":"1","article-title":"CVXPY: A python-embedded modeling language for convex optimization","volume":"17","author":"Diamond Steven","year":"2016","unstructured":"Steven Diamond and Stephen Boyd. 2016. CVXPY: A python-embedded modeling language for convex optimization. J. Machine Learning Research 17, 83 (2016), 1\u20135. Retrieved from http:\/\/www.cvxpy.org\/","journal-title":"J. Machine Learning Research"},{"key":"e_1_3_4_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2656045.2656054"},{"key":"e_1_3_4_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2013.6631226"},{"key":"e_1_3_4_20_2","volume-title":"Space Navigation Guidance and Control, Vol. 1","author":"Draper C. S.","year":"1965","unstructured":"C. S. Draper, W. Wrigley, D. G. Hoag, R. H. Battin, J. E. Miller, D. A. Koso, A. L. Hopkins, and W. E. Vander Velde. 1965. Space Navigation Guidance and Control, Vol. 1. Technical Report NASA-CR-75543 (R-500, Vol. 1). Massachusetts Institute of Technology, Cambridge, Massachusetts. Retrieved from https:\/\/ntrs.nasa.gov\/api\/citations\/19660019462\/downloads\/19660019462.pdf"},{"key":"e_1_3_4_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2007.4282788"},{"key":"e_1_3_4_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_4_23_2","unstructured":"International Organization for Standardization. 2023. Safety of machinery\u2014Safety-related parts of control systems\u2014Part 1: General principles for design. Retrieved 10th September 2025 from https:\/\/www.iso.org\/standard\/73481.html"},{"key":"e_1_3_4_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/TVT.2016.2555853"},{"key":"e_1_3_4_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-32552-1_7"},{"key":"e_1_3_4_26_2","volume-title":"Nonlinear Control","author":"Khalil Hassan K.","year":"2015","unstructured":"Hassan K. Khalil. 2015. Nonlinear Control. Pearson, Upper Saddle River, NJ. Retrieved 10th September 2025 from https:\/\/www.pearson.com\/store\/p\/nonlinear-control\/P100000659701\/9780133499148"},{"key":"e_1_3_4_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2023.3306717"},{"key":"e_1_3_4_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.914952"},{"key":"e_1_3_4_29_2","doi-asserted-by":"publisher","DOI":"10.4271\/2016-01-0128"},{"key":"e_1_3_4_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"e_1_3_4_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_4_32_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511546877"},{"key":"e_1_3_4_33_2","volume-title":"The Tagged Signal Model: A Preliminary Version of a Denotational Framework for Comparing Models of Computation","author":"Lee Edward A.","year":"1996","unstructured":"Edward A. Lee and Alberto L. Sangiovanni-Vincentelli. 1996. The Tagged Signal Model: A Preliminary Version of a Denotational Framework for Comparing Models of Computation. Technical Report UCB\/ERL M96\/33. EECS Department, University of California, Berkeley. Retrieved from http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/1996\/3030.html"},{"key":"e_1_3_4_34_2","doi-asserted-by":"publisher","DOI":"10.23919\/DATE56975.2023.10137069"},{"key":"e_1_3_4_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/IROS55552.2023.10341755"},{"key":"e_1_3_4_36_2","first-page":"3723","volume-title":"IEEE\/RSJ Int. Conf. Intelligent Robots and Systems (IROS)","year":"2018","unstructured":"Anqi Li, Li Wang, Pietro Pierpaoli, and Magnus Egerstedt. 2018. Formally correct composition of coordinated behaviors using control barrier certificates. In IEEE\/RSJ Int. Conf. Intelligent Robots and Systems (IROS). IEEE, 3723\u20133729."},{"key":"e_1_3_4_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC51059.2022.9992715"},{"key":"e_1_3_4_38_2","volume-title":"Incremental Control Synthesis for Robotics in the Presence of Temporal Logic Specifications","author":"Livingston Scott Carlton","year":"2016","unstructured":"Scott Carlton Livingston. 2016. Incremental Control Synthesis for Robotics in the Presence of Temporal Logic Specifications. Ph. D. Dissertation. California Institute of Technology."},{"key":"e_1_3_4_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/MCS.2024.3382388"},{"key":"e_1_3_4_40_2","doi-asserted-by":"publisher","DOI":"10.1002\/rnc.1758"},{"key":"e_1_3_4_41_2","unstructured":"Manuel Mazo Jr Will Compton Max H. Cohen and Aaron D. Ames. 2024. A contract theory for layered control architectures. arXiv:2409.14902. Retrieved from https:\/\/arxiv.org\/abs\/2409.14902"},{"key":"e_1_3_4_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/MEMOCODE51338.2020.9315118"},{"key":"e_1_3_4_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2024.3447213"},{"key":"e_1_3_4_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2019.2963255"},{"key":"e_1_3_4_45_2","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2018.8342122"},{"key":"e_1_3_4_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95246-8_22"},{"key":"e_1_3_4_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2453253"},{"key":"e_1_3_4_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2013.2295764"},{"key":"e_1_3_4_49_2","volume-title":"Modern Control Engineering","author":"Ogata Katsuhiko","year":"2010","unstructured":"Katsuhiko Ogata. 2010. Modern Control Engineering. Pearson, Upper Saddle River."},{"key":"e_1_3_4_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-14835-4_5"},{"key":"e_1_3_4_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0024-z"},{"key":"e_1_3_4_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_4_53_2","volume-title":"System Design, Modeling, and Simulation Using Ptolemy II","author":"Ptolemaeus Claudius","year":"2014","unstructured":"Claudius Ptolemaeus (Ed.). 2014. System Design, Modeling, and Simulation Using Ptolemy II. Ptolemy.org. Retrieved from http:\/\/ptolemy.org\/books\/Systems"},{"key":"e_1_3_4_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2351672"},{"key":"e_1_3_4_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/2185632.2185641"},{"key":"e_1_3_4_56_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039363"},{"key":"e_1_3_4_57_2","volume-title":"DO-178C: Software Considerations in Airborne Systems and Equipment Certification","author":"Inc. RTCA,","year":"2011","unstructured":"RTCA, Inc.2011. DO-178C: Software Considerations in Airborne Systems and Equipment Certification. Technical Report. Radio Technical Commission for Aeronautics (RTCA), Washington, D.C. Retrieved from https:\/\/www.rtca.orgRTCA Document No. DO-178C."},{"key":"e_1_3_4_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996684"},{"key":"e_1_3_4_59_2","volume-title":"Compositional and Efficient Controller Synthesis for Cyber-physical Systems","author":"Saoud Adnane","year":"2019","unstructured":"Adnane Saoud. 2019. Compositional and Efficient Controller Synthesis for Cyber-physical Systems. Ph. D. Dissertation. Universit\u00e9 Paris Saclay (COmUE)."},{"key":"e_1_3_4_60_2","doi-asserted-by":"publisher","DOI":"10.1109\/9.388691"},{"key":"e_1_3_4_61_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2018.2849003"},{"key":"e_1_3_4_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5"},{"key":"e_1_3_4_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_9"},{"key":"e_1_3_4_64_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC51059.2022.9992999"},{"key":"e_1_3_4_65_2","unstructured":"Wikimedia Commons Contributors. 2024. Marius + Reiner - LROC - WAC. Retrieved from https:\/\/upload.wikimedia.org\/wikipedia\/commons\/5\/56\/Marius_%2B_Reiner_-_LROC_-_WAC.JPG"},{"key":"e_1_3_4_66_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC40024.2019.9029455"},{"key":"e_1_3_4_67_2","doi-asserted-by":"publisher","DOI":"10.23919\/DATE58400.2024.10546764"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764587","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T14:28:57Z","timestamp":1759933737000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3764587"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,26]]},"references-count":66,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3764587"],"URL":"https:\/\/doi.org\/10.1145\/3764587","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,26]]},"assertion":[{"value":"2025-08-13","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-17","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}