{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:11:01Z","timestamp":1750306261981,"version":"3.41.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,5,11]],"date-time":"2017-05-11T00:00:00Z","timestamp":1494460800000},"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":[[2017,11,30]]},"abstract":"<jats:p>In an embedded system, the specialization of the code of the real-time operating system (RTOS) according to the requirements of the application allows one to remove unused services and other sources of dead code from the binary program. The typical specialization process is based on a mix of precompiler macros and build scripts, both of which are known for being sources of errors.<\/jats:p>\n          <jats:p>In this article, we present a new model-based approach to the design of application-specific RTOS. Starting with finite state models describing the RTOS and the application requirements, the set of blocks in the RTOS code actually used by the application is automatically computed. This set is used to build an application-specific RTOS model. This model is fed into a code generator to produce the source code of an application-specific RTOS. It is also used to carry on model-based validations and verifications, including the formal verification that the specialization process did not introduce unwanted behaviors or suppress expected ones.<\/jats:p>\n          <jats:p>To demonstrate the feasibility of this approach, it is applied to specialize Trampoline, an open-source implementation of the AUTOSAR OS standard, to an industrial case study from the automotive domain.<\/jats:p>","DOI":"10.1145\/3015777","type":"journal-article","created":{"date-parts":[[2017,5,11]],"date-time":"2017-05-11T12:51:05Z","timestamp":1494507065000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Formal Model-Based Synthesis of Application-Specific Static RTOS"],"prefix":"10.1145","volume":"16","author":[{"given":"Kabland Toussaint Gautier","family":"Tigori","sequence":"first","affiliation":[{"name":"\u00c9cole Centrale de Nantes, IRCCyN"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Luc","family":"B\u00e9chennec","sequence":"additional","affiliation":[{"name":"CNRS, IRCCyN"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9bastien","family":"Faucou","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Nantes, IRCCyN"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olivier Henri","family":"Roux","sequence":"additional","affiliation":[{"name":"\u00c9cole Centrale de Nantes, IRCCyN"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,5,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/WWOS.1992.275682"},{"key":"e_1_2_1_2_1","volume-title":"10th International Conference on Real-Time Systems (RTS\u201902)","author":"Barreto Luciano Porto","year":"2002","unstructured":"Luciano Porto Barreto and Gilles Muller . 2002 . Bossa: A language-based approach to the design of real-time schedulers . In 10th International Conference on Real-Time Systems (RTS\u201902) , 19--31. Luciano Porto Barreto and Gilles Muller. 2002. Bossa: A language-based approach to the design of real-time schedulers. In 10th International Conference on Real-Time Systems (RTS\u201902), 19--31."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2006.355432"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/WORDS.2003.1218077"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/CLUSTR.2003.1253322"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2011.26"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_2_1_8_1","volume-title":"11th Annual Workshop on Operating Systems Platforms for Embedded Real-Time applications (OSPERT\u201915)","author":"Dietrich Christian","year":"2015","unstructured":"Christian Dietrich , Martin Hoffman , and Daniel Lohmann . 2015 . Back to the roots: Implementing the RTOS as a specialized state machine . In 11th Annual Workshop on Operating Systems Platforms for Embedded Real-Time applications (OSPERT\u201915) . 7--12. Christian Dietrich, Martin Hoffman, and Daniel Lohmann. 2015. Back to the roots: Implementing the RTOS as a specialized state machine. In 11th Annual Workshop on Operating Systems Platforms for Embedded Real-Time applications (OSPERT\u201915). 7--12."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/IWOOOS.1993.324907"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/378993.379006"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1049\/ic:19981078"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/165854.165867"},{"key":"e_1_2_1_13_1","volume-title":"20th Network and Distributed System Security Symposium (NDSS\u201913)","author":"Kurmus Anil","year":"2013","unstructured":"Anil Kurmus , Reinhard Tartler , Daniela Dorneanu , Bernhard Heinloth , Valentin Rothberg , Andreas Ruprecht , Wolfgang Schr\u00f6der-Preikschat , Daniel Lohmann , and R\u00fcdiger Kapitza . 2013 . Attack surface metrics and automated compile-time OS kernel tailoring . In 20th Network and Distributed System Security Symposium (NDSS\u201913) . Anil Kurmus, Reinhard Tartler, Daniela Dorneanu, Bernhard Heinloth, Valentin Rothberg, Andreas Ruprecht, Wolfgang Schr\u00f6der-Preikschat, Daniel Lohmann, and R\u00fcdiger Kapitza. 2013. Attack surface metrics and automated compile-time OS kernel tailoring. In 20th Network and Distributed System Security Symposium (NDSS\u201913)."},{"key":"e_1_2_1_14_1","volume-title":"USENIX Annual Technical Conference.","author":"Lohmann Daniel","year":"2009","unstructured":"Daniel Lohmann , Wanja Hofer , Wolfgang Schr\u00f6der-Preikschat , Jochen Streicher , and Olaf Spinczyk . 2009 . CiAO: An aspect-oriented operating-system family for resource-constrained embedded systems . In USENIX Annual Technical Conference. Daniel Lohmann, Wanja Hofer, Wolfgang Schr\u00f6der-Preikschat, Jochen Streicher, and Olaf Spinczyk. 2009. CiAO: An aspect-oriented operating-system family for resource-constrained embedded systems. In USENIX Annual Technical Conference."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2695664.2695751"},{"key":"e_1_2_1_16_1","unstructured":"OSEK Group et al. 1999a. OSEK\/VDX OS Test Plan Version 2.0.  OSEK Group et al. 1999a. OSEK\/VDX OS Test Plan Version 2.0."},{"key":"e_1_2_1_17_1","unstructured":"OSEK Group et al. 1999b. OSEK\/VDX OS Test Procedure Version 2.0.  OSEK Group et al. 1999b. OSEK\/VDX OS Test Procedure Version 2.0."},{"key":"e_1_2_1_18_1","unstructured":"OSEK Group et al. 2005. OSEK\/VDX Operating System Specification.  OSEK Group et al. 2005. OSEK\/VDX Operating System Specification."},{"volume-title":"Proceedings of the 12th IEEE International Conference on Embedded Software and Systems. IEEE","author":"Gautier Tigori Kabland Toussaint","key":"e_1_2_1_19_1","unstructured":"Kabland Toussaint Gautier Tigori , Jean-Luc Bechennec , and Olivier H. Roux . 2015. Formal synthesis of optimal RTOS (Best paper award) . In Proceedings of the 12th IEEE International Conference on Embedded Software and Systems. IEEE , New York, 977--983. Kabland Toussaint Gautier Tigori, Jean-Luc Bechennec, and Olivier H. Roux. 2015. Formal synthesis of optimal RTOS (Best paper award). In Proceedings of the 12th IEEE International Conference on Embedded Software and Systems. IEEE, New York, 977--983."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevE.62.1805"},{"volume-title":"International Colloquium on Theoretical Aspects of Computing","author":"Yatake Kenro","key":"e_1_2_1_21_1","unstructured":"Kenro Yatake and Toshiaki Aoki . 2012. Model checking of OSEK\/VDX OS design model based on environment modeling . In International Colloquium on Theoretical Aspects of Computing . Springer , 183--197. Kenro Yatake and Toshiaki Aoki. 2012. Model checking of OSEK\/VDX OS design model based on environment modeling. In International Colloquium on Theoretical Aspects of Computing. Springer, 183--197."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3015777","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3015777","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:14Z","timestamp":1750220654000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3015777"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5,11]]},"references-count":21,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,11,30]]}},"alternative-id":["10.1145\/3015777"],"URL":"https:\/\/doi.org\/10.1145\/3015777","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2017,5,11]]},"assertion":[{"value":"2015-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-05-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}