{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:19:48Z","timestamp":1750220388773,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":60,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,4,25]],"date-time":"2022-04-25T00:00:00Z","timestamp":1650844800000},"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":[],"published-print":{"date-parts":[[2022,4,25]]},"DOI":"10.1145\/3477314.3506996","type":"proceedings-article","created":{"date-parts":[[2022,5,7]],"date-time":"2022-05-07T00:37:36Z","timestamp":1651883856000},"page":"1156-1165","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A framework for OS portability"],"prefix":"10.1145","author":[{"given":"Renata Martins","family":"Gomes","sequence":"first","affiliation":[{"name":"Graz University of Technology, Graz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcel","family":"Baunach","sequence":"additional","affiliation":[{"name":"Graz University of Technology, Graz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,5,6]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Modeling in Event-B: system and software engineering","author":"Abrial Jean-Raymond","unstructured":"Jean-Raymond Abrial. 2010. Modeling in Event-B: system and software engineering (1st ed.). Cambridge University Press, New York, NY, USA.","edition":"1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.15"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2018.09.007"},{"key":"e_1_3_2_1_4_1","volume-title":"International conference on communication, management and information technology. CRC press, Chapter Modeling guidelines of FreeRTOS in Event-B, 453--462","author":"Alkhammash Eman H.","year":"2017","unstructured":"Eman H. Alkhammash, Michael J. Butler, and Corina Cristea. 2017. International conference on communication, management and information technology. CRC press, Chapter Modeling guidelines of FreeRTOS in Event-B, 453--462."},{"key":"e_1_3_2_1_5_1","volume-title":"Alessandro Fantechi, Stefania Gnesi, Franco Mazzanti, Andrea Piattino, Daniele Trentini, and Alessio Ferrari.","author":"Basile Davide","year":"2018","unstructured":"Davide Basile, Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi, Franco Mazzanti, Andrea Piattino, Daniele Trentini, and Alessio Ferrari. 2018. On the Industrial Uptake of Formal Methods in the Railway Domain. In Integrated Formal Methods, Carlo A. Furia and Kirsten Winter (Eds.). Springer International Publishing, Cham, 20--29."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3417990.3419227"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1984.tb00064.x"},{"volume-title":"The case of an opinionated, theory-oriented realtime operating system. NGOSCPS19","author":"Brandenburg Bj\u00f6rn B.","key":"e_1_3_2_1_8_1","unstructured":"Bj\u00f6rn B. Brandenburg. 2019. The case of an opinionated, theory-oriented realtime operating system. NGOSCPS19."},{"volume-title":"Formal Methods for Industrial Critical Systems, Maurice H. ter Beek and Dejan Ni\u010dkovi\u0107 (Eds.)","author":"Butler Michael","key":"e_1_3_2_1_9_1","unstructured":"Michael Butler, Philipp K\u00f6rner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, and Laurent Voisin. 2020. The First Twenty-Five Years of Industrial Use of the B-Method. In Formal Methods for Industrial Critical Systems, Maurice H. ter Beek and Dejan Ni\u010dkovi\u0107 (Eds.). Springer International Publishing, Cham, 189--209."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0308-9"},{"volume-title":"2011 Fifth International Conference on Secure Software Integration and Reliability Improvement - Companion. 19--25","author":"Cho D.","key":"e_1_3_2_1_11_1","unstructured":"D. Cho and D. Bae. 2011. Case study on installing a porting process for embedded operating system in a small team. In 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement - Companion. 19--25."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/502059.502042"},{"volume-title":"Formal refinement for operating system kernels","author":"Craig Iain D.","key":"e_1_3_2_1_13_1","unstructured":"Iain D. Craig. 2007. Formal refinement for operating system kernels. Springer-Verlag New York, Inc., Secaucus, NJ, USA."},{"key":"e_1_3_2_1_14_1","volume-title":"Formal models of operating system kernels","author":"Craig Iain D.","unstructured":"Iain D. Craig. 2010. Formal models of operating system kernels (1st ed.). Springer Publishing Company, Incorporated.","edition":"1"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54994-7_3"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.2174\/1874110X01509011125"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2017.12.001"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869475"},{"volume-title":"A formal modeling approach for portable low-level OS functionality","author":"Gomes Renata Martins","key":"e_1_3_2_1_19_1","unstructured":"Renata Martins Gomes, Bernhard Aichernig, and Marcel Baunach. 2020. A formal modeling approach for portable low-level OS functionality. In Software Engineering and Formal Methods, Frank de Boer and Antonio Cerone (Eds.). Springer International Publishing, Cham, 155--174."},{"key":"e_1_3_2_1_20_1","volume-title":"OSPERT'17","author":"Gomes Renata Martins","year":"2017","unstructured":"Renata Martins Gomes, Marcel Baunach, Maja Malenko, Leandro Batista Ribeiro, and Fabian Mauroner. 2017. A co-designed RTOS and MCU concept for dynamically composed embedded systems. In OSPERT'17."},{"key":"e_1_3_2_1_21_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). USENIX Association, Savannah, GA, 653--669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365137.3365401"},{"volume-title":"Retrieved","year":"2021","key":"e_1_3_2_1_24_1","unstructured":"Infineon. [n. d.]. AURIX TriCore Microcontroller. Retrieved December 21, 2021 from https:\/\/www.infineon.com\/cms\/en\/product\/microcontroller\/32-bit-tricore-microcontroller\/"},{"key":"e_1_3_2_1_25_1","volume-title":"Retrieved","author":"Instruments Texas","year":"2019","unstructured":"Texas Instruments. 2019. MSP430 ultra-low-power sensing and measurement MCUs. Retrieved October 12, 2021 from http:\/\/www.ti.com\/microcontrollers\/msp430-ultra-low-power-mcus\/overview\/overview.html"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287634"},{"volume-title":"2009 IEEE 31st International Conference on Software Engineering. 485--495","author":"Juergens E.","key":"e_1_3_2_1_27_1","unstructured":"E. Juergens, F. Deissenboeck, B. Hummel, and S. Wagner. 2009. Do code clones matter?. In 2009 IEEE 31st International Conference on Software Engineering. 485--495."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192377"},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the Linux Symposium.","author":"Kleen Andi","year":"2001","unstructured":"Andi Kleen. 2001. Porting linux to x86-64. In Proceedings of the Linux Symposium."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.22"},{"volume-title":"Formal Methods: Foundations and Applications, Simone Cavalheiro and Jos\u00e9 Fiadeiro (Eds.)","author":"Lecomte Thierry","key":"e_1_3_2_1_32_1","unstructured":"Thierry Lecomte, David Deharbe, Etienne Prun, and Erwan Mottin. 2017. Applying a Formal Method in Industry: A 25-Year Trajectory. In Formal Methods: Foundations and Applications, Simone Cavalheiro and Jos\u00e9 Fiadeiro (Eds.). Springer International Publishing, Cham, 70--87."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0063-9"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/584418.584423"},{"key":"e_1_3_2_1_35_1","first-page":"289","article-title":"CP-Miner: a tool for finding copy-paste and related bugs in operating system code","volume":"4","author":"Li Zhenmin","year":"2004","unstructured":"Zhenmin Li, Shan Lu, Suvda Myagmar, and Yuanyuan Zhou. 2004. CP-Miner: a tool for finding copy-paste and related bugs in operating system code.. In OSdi, Vol. 4. 289--302.","journal-title":"OSdi"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Anna Lyons Adrian Danis Yyshen Hesham Almatary Stephen Sherratt Amirreza Zarrabi Kent McLeod Gerwin Klein Latent Prion Joel Beeren Thomas Sewell Adam Rafal Kolanski Alexander Boettcher Partha Susarla Matthew Brecknell Jeff Waugh Seb Holzapfel Christopher Guikema Corey Richardson Cloudier Robbie VanVossen Mktnk3 Mokshasoft Tim Newsham Luke Mondy Jesse Millwood Jsuann Nathan Studer and Curtis Millar. 2018. seL4\/seL4: MCS pre-release. 10.5281\/ZENODO.591727","DOI":"10.5281\/ZENODO.591727"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.18420\/fgbs2021f-01"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2069216.2069252"},{"volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"Novikov Evgeny","key":"e_1_3_2_1_39_1","unstructured":"Evgeny Novikov and Ilja Zakharov. 2018. Verification of operating system monolithic kernels without extensions. In Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, Tiziana Margaria and Bernhard Steffen (Eds.). Springer International Publishing, Cham, 230--248."},{"volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"Nyberg Mattias","key":"e_1_3_2_1_40_1","unstructured":"Mattias Nyberg, Dilian Gurov, Christian Lidstr\u00f6m, Andreas Rasmusson, and Jonas Westman. 2018. Formal Verification in Automotive Industry: Enablers and Obstacles. In Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, Tiziana Margaria and Bernhard Steffen (Eds.). Springer International Publishing, Cham, 139--158."},{"volume-title":"2011 International Conference on Distributed Computing in Sensor Systems and Workshops (DCOSS). 1--6.","author":"Oikonomou G.","key":"e_1_3_2_1_41_1","unstructured":"G. Oikonomou and I. Phillips. 2011. Experiences from porting the Contiki operating system to a popular hardware platform. In 2011 International Conference on Distributed Computing in Sensor Systems and Workshops (DCOSS). 1--6."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2968478.2968493"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693095"},{"volume-title":"A Modeling Concept for Formal Verification of OS-Based Compositional Software. Under review at 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Ribeiro Leandro Batista","key":"e_1_3_2_1_44_1","unstructured":"Leandro Batista Ribeiro, Florian Lorber, Ulrik Nyman, Kim G. Larsen, and Marcel Baunach. 2022. A Modeling Concept for Formal Verification of OS-Based Compositional Software. Under review at 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_3_2_1_45_1","volume-title":"d.]. RISC-V. Retrieved","author":"Foundation RISC-V","year":"2021","unstructured":"RISC-V Foundation. [n. d.]. RISC-V. Retrieved October 12, 2021 from https:\/\/riscv.org\/"},{"volume-title":"Proceedings of the 28th Annual International Conference on Computer Science and Software Engineering (CASCON '18)","author":"Rivera Luis F.","key":"e_1_3_2_1_46_1","unstructured":"Luis F. Rivera, Norha M. Villegas, Gabriel Tamura, Miguel Jim\u00e9nez, and Hausi A. M\u00fcller. 2018. UML-Driven Automated Software Deployment. In Proceedings of the 28th Annual International Conference on Computer Science and Software Engineering (CASCON '18). IBM Corp., USA, 257--268."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0381-2"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/RAMECH.2004.1438043"},{"volume-title":"Towards Generating SPARK from Event-B Models","author":"Sritharan Sanjeevan","key":"e_1_3_2_1_49_1","unstructured":"Sanjeevan Sritharan and Thai Son Hoang. 2020. Towards Generating SPARK from Event-B Models. In Integrated Formal Methods, Brijesh Dongol and Elena Troubitsyna (Eds.). Springer International Publishing, Cham, 103--120."},{"key":"e_1_3_2_1_50_1","volume-title":"Porting the core of the Contiki operating system to the TelosB and MicaZ platforms","author":"Stan Alexandru","year":"2007","unstructured":"Alexandru Stan. 2007. Porting the core of the Contiki operating system to the TelosB and MicaZ platforms. International University, Bremen Bachelor thesis (2007)."},{"volume-title":"B 2007: Formal Specification and Development in B","author":"Stoddart Bill","key":"e_1_3_2_1_51_1","unstructured":"Bill Stoddart, Dominique Cansell, and Frank Zeyda. 2006. Modelling and proof analysis of interrupt driven scheduling. In B 2007: Formal Specification and Development in B, Jacques Julliand and Olga Kouchnarenko (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 155--170."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/iceccs.2015.24"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09539-7"},{"key":"e_1_3_2_1_54_1","volume-title":"Linux Symposium, John W. Lockhart (Ed.). The Linux Foundation, 398","author":"Takata Hirokazu","year":"2003","unstructured":"Hirokazu Takata, Naoto Sugai, and Hitoshi Yamamoto. 2003. Porting Linux to the M32R processor. In Linux Symposium, John W. Lockhart (Ed.). The Linux Foundation, 398."},{"volume-title":"Linux: a Portable Operating System. Master's thesis","author":"Torvalds Linus","key":"e_1_3_2_1_55_1","unstructured":"Linus Torvalds. 1997. Linux: a Portable Operating System. Master's thesis. University of Helsinki."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-9736-4"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"},{"key":"e_1_3_2_1_58_1","volume-title":"Workshop on integration of model-based formal methods and tools. 14","author":"Wright Steve","year":"2009","unstructured":"Steve Wright. 2009. Automatic generation of C from Event-B. In Workshop on integration of model-based formal methods and tools. 14."},{"key":"e_1_3_2_1_60_1","volume-title":"A Survey on Formal Specification and Verification of System-Level Achievements in Industrial Circles","author":"Zhang Feng","year":"2019","unstructured":"Feng Zhang and Wensheng Niu. 2019. A Survey on Formal Specification and Verification of System-Level Achievements in Industrial Circles. Academic journal of computing and information science (2019)."},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2597457.2597466"},{"volume-title":"Computer Network Security (2005-09-19)","author":"Zhou Zhouyi","key":"e_1_3_2_1_62_1","unstructured":"Zhouyi Zhou, Bin Liang, Li Jiang, Wenchang Shi, and Yeping He. 2005. A Formal Description of SECIMOS Operating System. In Computer Network Security (2005-09-19), Vladimir Gorodetsky, Igor Kotenko, and Victor Skormin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 286--297. https:\/\/www.ebook.de\/de\/product\/25413758\/computer_network_security.html"}],"event":{"name":"SAC '22: The 37th ACM\/SIGAPP Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Virtual Event","acronym":"SAC '22"},"container-title":["Proceedings of the 37th ACM\/SIGAPP Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477314.3506996","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3477314.3506996","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:33Z","timestamp":1750191513000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477314.3506996"}},"subtitle":["from formal models to low-level code"],"short-title":[],"issued":{"date-parts":[[2022,4,25]]},"references-count":60,"alternative-id":["10.1145\/3477314.3506996","10.1145\/3477314"],"URL":"https:\/\/doi.org\/10.1145\/3477314.3506996","relation":{},"subject":[],"published":{"date-parts":[[2022,4,25]]},"assertion":[{"value":"2022-05-06","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}