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

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.