{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:27:31Z","timestamp":1750307251671,"version":"3.41.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2010,12,1]],"date-time":"2010-12-01T00:00:00Z","timestamp":1291161600000},"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":[[2010,12]]},"abstract":"<jats:p>Adaptation is increasingly used in the development of safety-critical embedded systems, in particular to reduce hardware needs and to increase availability. However, composing a system from many reconfigurable components can lead to a huge number of possible system configurations, inducing a complexity that cannot be handled during system design. To overcome this problem, we propose a new component-based modeling and verification method for adaptive embedded systems. The component-based modeling approach facilitates abstracting a composition of components to a hierarchical component. In the hierarchical component, the number of possible configurations of the composition is reduced to a small number of hierarchical configurations. Only these hierarchical configurations have to be considered when the hierarchical component is used in further compositions such that design complexity is reduced at each hierarchical level. In order to ensure well-definedness of components, we provide a model of computation enabling the formal verification of critical requirements of the adaptation behavior.<\/jats:p>","DOI":"10.1145\/1880050.1880056","type":"journal-article","created":{"date-parts":[[2011,1,5]],"date-time":"2011-01-05T16:59:17Z","timestamp":1294246757000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Component-based modeling and verification of dynamic adaptation in safety-critical embedded systems"],"prefix":"10.1145","volume":"10","author":[{"given":"Rasmus","family":"Adler","sequence":"first","affiliation":[{"name":"Fraunhofer Institute for Experimental Software Engineering"}]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[{"name":"Software Technology Group, University of Kaiserslautern, Kaiserslautern, Germany"}]},{"given":"Mario","family":"Trapp","sequence":"additional","affiliation":[{"name":"Fraunhofer Institute for Experimental Software Engineering"}]},{"given":"Arnd","family":"Poetzsch-Heffter","sequence":"additional","affiliation":[{"name":"Software Technology Group, University of Kaiserslautern, Kaiserslautern, Germany"}]}],"member":"320","published-online":{"date-parts":[[2011,1,7]]},"reference":[{"volume-title":"Proceedings of the International Conference on Formal Engineering Methods. IEEE","author":"Adler R.","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/7929"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Atkinson C. Bayer J. Bunse C. Kamsties E. Laitenberger O. Laqua R. Muthig D. Paech B. Wust J. and Zettel J. 2002. Component-Based Product Line Engineering with UML. Addison-Wesley Upper Saddle River NJ.   Atkinson C. Bayer J. Bunse C. Kamsties E. Laitenberger O. Laqua R. Muthig D. Paech B. Wust J. and Zettel J. 2002. Component-Based Product Line Engineering with UML. Addison-Wesley Upper Saddle River NJ.","DOI":"10.1007\/3-540-46020-9_34"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2006.27"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/SERA.2006.62"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062601"},{"key":"e_1_2_1_8_1","unstructured":"Clarke E. Grumberg O. and Peled D. 1999. Model checking. MIT Press.   Clarke E. Grumberg O. and Peled D. 1999. Model checking. MIT Press."},{"volume-title":"Proceedings of the Foundations of Interface Technologies. Elsevier Science","author":"Damm W.","key":"e_1_2_1_9_1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805829"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017753.1017778"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87891-9_15"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"volume-title":"Proceedings of the International Conference on Information System Implementation and Modeling.","author":"Hnetynka P.","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","unstructured":"Jantsch A. 2004. Modeling Embedded Systems and SoCs. Morgan Kaufmann San Francisco CA.   Jantsch A. 2004. Modeling Embedded Systems and SoCs. Morgan Kaufmann San Francisco CA."},{"key":"e_1_2_1_17_1","unstructured":"Kemman S. 2007. Tool supported specification of embedded component systems. Internal rep. Department of Component Engineering Fraunhofer IESE.  Kemman S. 2007. Tool supported specification of embedded component systems. Internal rep. Department of Component Engineering Fraunhofer IESE."},{"volume-title":"Proceedings of the Workshop on Intelligent Signal Processing. IEEE","author":"Ledeczi A.","key":"e_1_2_1_18_1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-004-0043-8"},{"key":"e_1_2_1_20_1","unstructured":"Lyu M. R. 1995. Software Fault Tolerance. John Wiley and Sons New York.   Lyu M. R. 1995. Software Fault Tolerance. John Wiley and Sons New York."},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A. 1995. Temporal Verification of Reactive Systems: Safety. Springer Berlin.   Manna Z. and Pnueli A. 1995. Temporal Verification of Reactive Systems: Safety. Springer Berlin.","DOI":"10.1007\/978-1-4612-4222-2"},{"volume-title":"Proceedings of the International Conference on Application of Concurrency to System Design. IEEE","author":"Mousavi M. R.","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Nipkow T. Paulson L. and Wenzel M. 2002. Isabelle\/HOL\u2014A proof Assistant for Higher-Order Logic. Springer Berlin.   Nipkow T. Paulson L. and Wenzel M. 2002. Isabelle\/HOL\u2014A proof Assistant for Higher-Order Logic. Springer Berlin.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1049404"},{"volume-title":"Proceedings of the Aerospace Conference. IEEE","author":"Rawashdeh O.","key":"e_1_2_1_25_1"},{"key":"e_1_2_1_26_1","unstructured":"Schaefer I. 2008. Integrating formal verification into the model-based development for adaptive embedded systems. Ph.D. thesis University of Kaiserslautern.  Schaefer I. 2008. Integrating formal verification into the model-based development for adaptive embedded systems. Ph.D. thesis University of Kaiserslautern."},{"volume-title":"Proceedings of the International Conference on Application of Concurrency to System Design. IEEE","author":"Schneider K.","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1137677.1137681"},{"key":"e_1_2_1_29_1","unstructured":"Selic B. Gullekson G. and Ward P. T. 1994. Real-Time Object-Oriented Modeling. John Wiley and Sons New York.   Selic B. Gullekson G. and Ward P. T. 1994. Real-Time Object-Oriented Modeling. John Wiley and Sons New York."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/WORDS.2003.1218078"},{"volume-title":"Proceedings of the International Conference on Dependable Systems and Networks. IEEE","author":"Shelton C. P.","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2006.33"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Szyperski C. 1999. Component Software. Beyond Object-Oriented Programming. ACM New York.   Szyperski C. 1999. Component Software. Beyond Object-Oriented Programming. ACM New York.","DOI":"10.1007\/3-540-46589-8_10"},{"key":"e_1_2_1_34_1","unstructured":"Trapp M. 2005. Modeling the adaptation behavior of adaptive embedded systems. Ph.D. thesis University of Kaiserslautern.  Trapp M. 2005. Modeling the adaptation behavior of adaptive embedded systems. Ph.D. thesis University of Kaiserslautern."},{"volume-title":"Proceedings of the International Multi-Conference on Software Engineering.","author":"Trapp M.","key":"e_1_2_1_35_1"},{"volume-title":"Proceedings of the 1st European Young Researcher Workshop on Service-Oriented Computing.","author":"Vall\u00e9e M.","key":"e_1_2_1_36_1"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/648200.748952"},{"volume-title":"Proceedings of the International Conference on Applied Informatics and Communications.","author":"Yan Z.","key":"e_1_2_1_38_1"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134337"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1880050.1880056","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1880050.1880056","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:16Z","timestamp":1750243936000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1880050.1880056"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["10.1145\/1880050.1880056"],"URL":"https:\/\/doi.org\/10.1145\/1880050.1880056","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2010,12]]},"assertion":[{"value":"2008-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}