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

Renata Martins Gomes; Marcel Carsten Baunach

doi:10.1145/3477314.3506996

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

Renata Martins Gomes, Marcel Carsten Baunach

Institute of Technical Informatics (4480)

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

Abstract

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 language	English
Title of host publication	Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, SAC 2022
Publisher	Association of Computing Machinery
Pages	1156-1165
Number of pages	10
ISBN (Electronic)	978-1-4503-8713-2
DOIs	https://doi.org/10.1145/3477314.3506996
Publication status	Published - 25 Apr 2022
Event	37th ACM/SIGAPP Symposium On Applied Computing: SAC 2022 - Virtuell, United States Duration: 25 Apr 2022 → 29 Apr 2022

Publication series

Name	Proceedings of the ACM Symposium on Applied Computing

Conference

Conference	37th ACM/SIGAPP Symposium On Applied Computing
Abbreviated title	SAC 2022
Country/Territory	United States
City	Virtuell
Period	25/04/22 → 29/04/22

Keywords

code generation
dependability
embedded systems
formal methods
operating systems
portability
verification

ASJC Scopus subject areas

Software

Fields of Expertise

Information, Communication & Computing

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1145/3477314.3506996

Cite this

A framework for OS portability: from formal models to low-level code. / Martins Gomes, Renata; Baunach, Marcel Carsten.
Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, SAC 2022. Association of Computing Machinery, 2022. p. 1156-1165 (Proceedings of the ACM Symposium on Applied Computing).

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

Martins Gomes, R & Baunach, MC 2022, A framework for OS portability: from formal models to low-level code. in Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, SAC 2022. Proceedings of the ACM Symposium on Applied Computing, Association of Computing Machinery, pp. 1156-1165, 37th ACM/SIGAPP Symposium On Applied Computing, Virtuell, United States, 25/04/22. https://doi.org/10.1145/3477314.3506996

@inproceedings{78fecc51efac4c7b99b457ce6ce74759,

title = "A framework for OS portability: from formal models to low-level code",

abstract = "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.",

keywords = "code generation, dependability, embedded systems, formal methods, operating systems, portability, verification",

author = "{Martins Gomes}, Renata and Baunach, {Marcel Carsten}",

year = "2022",

month = apr,

day = "25",

doi = "10.1145/3477314.3506996",

language = "English",

series = "Proceedings of the ACM Symposium on Applied Computing",

publisher = "Association of Computing Machinery",

pages = "1156--1165",

booktitle = "Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, SAC 2022",

address = "United States",

note = "37th ACM/SIGAPP Symposium On Applied Computing : SAC 2022, SAC 2022 ; Conference date: 25-04-2022 Through 29-04-2022",

}

TY - GEN

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

AU - Martins Gomes, Renata

AU - Baunach, Marcel Carsten

PY - 2022/4/25

Y1 - 2022/4/25

N2 - 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.

AB - 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.

KW - code generation

KW - dependability

KW - embedded systems

KW - formal methods

KW - operating systems

KW - portability

KW - verification

UR - http://www.scopus.com/inward/record.url?scp=85130331201&partnerID=8YFLogxK

U2 - 10.1145/3477314.3506996

DO - 10.1145/3477314.3506996

M3 - Conference paper

T3 - Proceedings of the ACM Symposium on Applied Computing

SP - 1156

EP - 1165

BT - Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, SAC 2022

PB - Association of Computing Machinery

T2 - 37th ACM/SIGAPP Symposium On Applied Computing

Y2 - 25 April 2022 through 29 April 2022

ER -

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

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Fields of Expertise

UN SDGs

Access to Document

Other files and links

Fingerprint

Embedded Automotive Systems

Dependable Internet of Things

Embedded Operating Systems

Cite this

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

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Fields of Expertise

UN SDGs

Access to Document

Other files and links

Fingerprint

Projects

Embedded Automotive Systems

Dependable Internet of Things

Embedded Operating Systems

Cite this