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

Renata Martins Gomes, Marcel Carsten Baunach

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review


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.
Original languageEnglish
Title of host publicationProceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, SAC 2022
PublisherAssociation of Computing Machinery
Number of pages10
ISBN (Electronic)978-1-4503-8713-2
Publication statusPublished - 25 Apr 2022
Event37th ACM/SIGAPP Symposium On Applied Computing: SAC 2022 - Virtuell, United States
Duration: 25 Apr 202229 Apr 2022

Publication series

NameProceedings of the ACM Symposium on Applied Computing


Conference37th ACM/SIGAPP Symposium On Applied Computing
Abbreviated titleSAC 2022
Country/TerritoryUnited States


  • code generation
  • dependability
  • embedded systems
  • formal methods
  • operating systems
  • portability
  • verification

ASJC Scopus subject areas

  • Software

Fields of Expertise

  • Information, Communication & Computing


Dive into the research topics of 'A framework for OS portability: from formal models to low-level code'. Together they form a unique fingerprint.

Cite this