{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:51:49Z","timestamp":1750308709647,"version":"3.41.0"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,1,29]],"date-time":"2013-01-29T00:00:00Z","timestamp":1359417600000},"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":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[2013,1,29]]},"abstract":"<jats:p>The increasing complexity of embedded systems is pushing their design to System-Level, thus leading to a convergence between software and hardware. Consequently, operating systems in this realm are also being required to deliver their services both as software and as hardware. In such a scenario, it is desirable to verify system properties regardless of whether its components are instantiated at software or hardware. In this paper, we describe an approach to formally verify functional correctness and safety properties of such system-level component. The approach is illustrated by a case study of EPOS' scheduler, whose implementation can be driven to yield both a software instance compiled by the GCC C++ compiler or a hardware instance synthesized by the CatapultC ESL tool. We demonstrate that the scheduler follows its specification regardless of the domain for which it is instantiated. We also demonstrate that the proposed approach causes no run-time overhead, since the adopted Software Model Checking techniques are deployed at compile-time.<\/jats:p>","DOI":"10.1145\/2433140.2433148","type":"journal-article","created":{"date-parts":[[2013,2,5]],"date-time":"2013-02-05T13:19:41Z","timestamp":1360070381000},"page":"28-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["On the formal verification of component-based embedded operating systems"],"prefix":"10.1145","volume":"47","author":[{"given":"Mateus Krepsky","family":"Ludwich","sequence":"first","affiliation":[{"name":"Federal University of Santa Catarina (UFSC), Software\/Hardware Integration Lab (LISHA), Florian\u00f3polis - SC - Brazil"}]},{"given":"Ant\u00f4nio Augusto","family":"Fr\u00f6hlich","sequence":"additional","affiliation":[{"name":"Federal University of Santa Catarina (UFSC), Software\/Hardware Integration Lab (LISHA), Florian\u00f3polis - SC - Brazil"}]}],"member":"320","published-online":{"date-parts":[[2013,1,29]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.5555\/1792734.1792781"},{"key":"e_1_2_1_2_1","volume-title":"CatapultC Synthesis","author":"Systems Calypto Design","year":"2011","unstructured":"Calypto Design Systems . CatapultC Synthesis , 2011 . http:\/\/www.calypto.com\/. Calypto Design Systems. CatapultC Synthesis, 2011. http:\/\/www.calypto.com\/."},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.5555\/2032305.2032329"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1007\/s10703-006-0020-3"},{"key":"e_1_2_1_5_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Clarke E.","year":"2004","unstructured":"E. Clarke , D. Kroening , and F. Lerda . A tool for checking ANSI-C programs . In K. Jensen and A. Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems , volume 2988 of Lecture Notes in Computer Science , pages 168 -- 176 , 2004 . E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In K. Jensen and A. Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 2988 of Lecture Notes in Computer Science, pages 168--176, 2004."},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1007\/978-3-642-03359-9_2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1007\/978-3-642-14295-6_42"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1109\/ICECS.2011.6122379"},{"key":"e_1_2_1_9_1","volume-title":"Sankt Augustin","author":"Fr\u00f6hlich A. A.","year":"2001","unstructured":"A. A. Fr\u00f6hlich . Application-Oriented Operating Systems. GMD -- Forschungszentrum Informationstechnik , Sankt Augustin , 2001 . A. A. Fr\u00f6hlich. Application-Oriented Operating Systems. GMD -- Forschungszentrum Informationstechnik, Sankt Augustin, 2001."},{"key":"e_1_2_1_10_1","volume-title":"Cybernetics and Informatics","author":"Fr\u00f6hlich A. A.","year":"2000","unstructured":"A. A. Fr\u00f6hlich and W. Schr\u00f6der-Preikschat . Scenario Adapters: Efficiently Adapting Components. In 4th World Multiconference on Systemics , Cybernetics and Informatics , Orlando, USA , July 2000 . A. A. Fr\u00f6hlich and W. Schr\u00f6der-Preikschat. Scenario Adapters: Efficiently Adapting Components. In 4th World Multiconference on Systemics, Cybernetics and Informatics, Orlando, USA, July 2000."},{"key":"e_1_2_1_11_1","volume-title":"Morgan Kaufmann","author":"Fujita M.","year":"2008","unstructured":"M. Fujita , I. Ghosh , and M. Prasad . Verification Techniques for System-Level Design . Morgan Kaufmann , San Francisco, CA, USA , 2008 . M. Fujita, I. Ghosh, and M. Prasad. Verification Techniques for System-Level Design. Morgan Kaufmann, San Francisco, CA, USA, 2008."},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1109\/TCAD.2009.2026356"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1145\/2034574.2034827"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_15_1","volume-title":"The cbmc homepage","author":"Kr\u00f6ning D.","year":"2012","unstructured":"D. Kr\u00f6ning . The cbmc homepage , 2012 . D. Kr\u00f6ning. The cbmc homepage, 2012."},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1109\/CSE.2009.407"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1109\/2.161279"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1145\/2146382.2146395"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: a proof assistant for higher-order logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , M. Wenzel , and L. C. Paulson . Isabelle\/HOL: a proof assistant for higher-order logic . Springer-Verlag , 2002 . T. Nipkow, M. Wenzel, and L. C. Paulson. Isabelle\/HOL: a proof assistant for higher-order logic. Springer-Verlag, 2002."}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2433140.2433148","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2433140.2433148","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:14:09Z","timestamp":1750277649000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2433140.2433148"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,29]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1,29]]}},"alternative-id":["10.1145\/2433140.2433148"],"URL":"https:\/\/doi.org\/10.1145\/2433140.2433148","relation":{},"ISSN":["0163-5980"],"issn-type":[{"type":"print","value":"0163-5980"}],"subject":[],"published":{"date-parts":[[2013,1,29]]},"assertion":[{"value":"2013-01-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}