{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,29]],"date-time":"2025-12-29T22:05:04Z","timestamp":1767045904089,"version":"3.41.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2015,9,28]],"date-time":"2015-09-28T00:00:00Z","timestamp":1443398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Science Foundation under NSF","award":["1136146"],"award-info":[{"award-number":["1136146"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2015,9,28]]},"abstract":"<jats:p>Constraint programming solvers, such as Satisfiability Modulo Theory (SMT) solvers, are capable tools in finding preferable configurations for embedded systems from large design spaces. However, constructing SMT constraint programs is not trivial, in particular for complex systems that exhibit multiple viewpoints and models. In thisarticle we propose CoDeL: a component-based description language that allows system designers to express components as reusable building blocks of the system with their parameterizable properties, models, and interconnectivity. Systems are synthesized by allocating, connecting, and parameterizing the components to satisfy the requirements of an application. We present an algorithm that transforms component-based design spaces, expressible in CoDeL, to an SMT program, which, solved by state-of-the-art SMT solvers, determines the satisfiability of the synthesis problem, and delivers a correct-by-construction system configuration. Evaluation results for use cases in the domain of scheduling and mapping of distributed real-time processes confirm, first, the performance gain of SMT compared to traditional design space exploration approaches, second, the usability gains by expressing design problems in CoDeL, and third, the capability of the CoDeL\/SMT approach to support the design of embedded systems.<\/jats:p>","DOI":"10.1145\/2746235","type":"journal-article","created":{"date-parts":[[2015,9,29]],"date-time":"2015-09-29T19:22:29Z","timestamp":1443554549000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Component-Based Synthesis of Embedded Systems Using Satisfiability Modulo Theories"],"prefix":"10.1145","volume":"20","author":[{"given":"Steffen","family":"Peter","sequence":"first","affiliation":[{"name":"University of California, Irvine"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tony","family":"Givargis","sequence":"additional","affiliation":[{"name":"University of California, Irvine"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,9,28]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE.2013.6612272"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/2485288.2485554"},{"key":"e_1_2_1_3_1","unstructured":"Clark Barrett Silvio Ranise Aaron Stump and Cesare Tinelli. 2013. The satisfiability modulo theories library (SMT-LIB). www.SMT-LIB.org.  Clark Barrett Silvio Ranise Aaron Stump and Cesare Tinelli. 2013. The satisfiability modulo theories library (SMT-LIB). www.SMT-LIB.org."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2006.104"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25318-8_3"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970506"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_12"},{"volume-title":"Bussieck and Alex Meeraus","year":"2004","author":"Michael","key":"e_1_2_1_8_1"},{"volume-title":"Proceedings of Foundations of Interface Technologies (FIT).","year":"2005","author":"Damm Werner","key":"e_1_2_1_9_1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503226"},{"volume-title":"Henzinger","year":"2001","author":"Alfaro Luca De","key":"e_1_2_1_11_1"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Moura Leonardo De","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2502524.2502540"},{"volume-title":"Kernighan","year":"1989","author":"Fourer Robert","key":"e_1_2_1_16_1"},{"volume-title":"Embedded System Design: Modeling, Synthesis and Verification","author":"Gajski Daniel D.","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.vlsi.2004.06.001"},{"volume-title":"Proceedings of the IEEE International Conference on Embedded Software and Systems (ICESS).","year":"2014","author":"Gunes Volkan","key":"e_1_2_1_19_1"},{"volume-title":"Computer Aided Verification","author":"Hang Christine","key":"e_1_2_1_20_1"},{"volume-title":"Proceedings of the Design, Automation and Test in Europe Conference and Exhibition. IEEE, 1168--1169","author":"Haubelt Christian","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2597809.2597817"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455229.1455230"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2485288.2485470"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2465449.2465455"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Philip Levis Sam Madden Joseph Polastre etal 2005. TinyOS: An operating system for sensor networks. In Ambient Intelligence Springer Berlin 115--148.  Philip Levis Sam Madden Joseph Polastre et al. 2005. TinyOS: An operating system for sensor networks. In Ambient Intelligence Springer Berlin 115--148.","DOI":"10.1007\/3-540-27139-2_7"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535857"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2010.204"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1356802.1356969"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958042"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Jose A. Martin Fabio Martinelli Ilaria Matteucci Ernesto Pimentel and Mathieu Turuani. 2014. On the synthesis of secure services composition. In Engineering Secure Future Internet Services and Systems 140--159.  Jose A. Martin Fabio Martinelli Ilaria Matteucci Ernesto Pimentel and Mathieu Turuani. 2014. On the synthesis of secure services composition. In Engineering Secure Future Internet Services and Systems 140--159.","DOI":"10.1007\/978-3-319-07452-8_6"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2744857"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000367.2000372"},{"volume-title":"Proceedings of the Workshop on Design Space Exploration of Cyber-Physical Systems (IDEAL).","year":"2014","author":"Neema Himanshu","key":"e_1_2_1_34_1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_18"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2013.2295764"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCN.2008.4664280"},{"volume-title":"Proceedings of the Design Automation Conference (DAC).","year":"2010","author":"Reimann Felix","key":"e_1_2_1_38_1"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024724.2024817"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/54.970421"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2013.6509684"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_38"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87891-9_21"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364542"},{"key":"e_1_2_1_45_1","unstructured":"Simulink. 2013. Simulation and Model-Based Design. http:\/\/www.mathworks.com\/products\/simulink\/.  Simulink. 2013. Simulation and Model-Based Design. http:\/\/www.mathworks.com\/products\/simulink\/."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0165-1684(92)90057-4"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/SAMOS.2011.6045482"},{"volume-title":"Proceedings of the Design, Automation and Test in Europe Conference and Exhibition. IEEE, 388--393","author":"Vachoux A.","key":"e_1_2_1_48_1"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2009.58"},{"volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design. 279--285","year":"2001","author":"Zhang Lintao","key":"e_1_2_1_50_1"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362336.2362352"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2746235","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2746235","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:44Z","timestamp":1750227404000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2746235"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,28]]},"references-count":50,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,9,28]]}},"alternative-id":["10.1145\/2746235"],"URL":"https:\/\/doi.org\/10.1145\/2746235","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2015,9,28]]},"assertion":[{"value":"2014-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-09-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}