A framework for OS portability: from formal models to low-level code

Renata Martins Gomes, Marcel Carsten Baunach

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem KonferenzbandBegutachtung


Porting software to different target architectures has always been an issue for developers as well as a source of errors and inconsistencies with requirements. This is especially true for low-level software that interacts directly with hardware components, like drivers, system services, or operating system kernels. OS developers have assumed and accepted that, to have the OS run on another hardware platform, one will have to manually adapt and (re)implement major parts of the code.

We propose a different approach to OS portability, based on formal methods. The framework presented in this work has the potential to not only improve portability, but also overall maintainability and system dependability, as it combines verification and code generation.

We present the framework and its concepts, along with a proof of concept showing how a context switch is modeled in a generic way and how code is automatically generated for two different target architectures.
TitelProceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, SAC 2022
Herausgeber (Verlag)Association of Computing Machinery
ISBN (elektronisch)978-1-4503-8713-2
PublikationsstatusVeröffentlicht - 25 Apr. 2022
Veranstaltung37th ACM/SIGAPP Symposium On Applied Computing: SAC 2022 - Virtuell, USA / Vereinigte Staaten
Dauer: 25 Apr. 202229 Apr. 2022


NameProceedings of the ACM Symposium on Applied Computing


Konferenz37th ACM/SIGAPP Symposium On Applied Computing
KurztitelSAC 2022
Land/GebietUSA / Vereinigte Staaten

ASJC Scopus subject areas

  • Software

Fields of Expertise

  • Information, Communication & Computing


Untersuchen Sie die Forschungsthemen von „A framework for OS portability: from formal models to low-level code“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren