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

Institut für Technische Informatik (4480)

Publikation: Beitrag in Buch/Bericht/Konferenzband › Beitrag in einem Konferenzband › Begutachtung

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.

Originalsprache	englisch
Titel	Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, SAC 2022
Herausgeber (Verlag)	Association of Computing Machinery
Seiten	1156-1165
Seitenumfang	10
ISBN (elektronisch)	978-1-4503-8713-2
DOIs	https://doi.org/10.1145/3477314.3506996
Publikationsstatus	Veröffentlicht - 25 Apr. 2022
Veranstaltung	37th ACM/SIGAPP Symposium On Applied Computing: SAC 2022 - Virtuell, USA / Vereinigte Staaten Dauer: 25 Apr. 2022 → 29 Apr. 2022

Publikationsreihe

Name	Proceedings of the ACM Symposium on Applied Computing

Konferenz

Konferenz	37th ACM/SIGAPP Symposium On Applied Computing
Kurztitel	SAC 2022
Land/Gebiet	USA / Vereinigte Staaten
Ort	Virtuell
Zeitraum	25/04/22 → 29/04/22

ASJC Scopus subject areas

Software

Fields of Expertise

Information, Communication & Computing

UN SDGs

Dieser Output leistet einen Beitrag zu folgendem(n) Ziel(en) für nachhaltige Entwicklung

Zugriff auf Dokument

10.1145/3477314.3506996

Andere Dateien und Links

Verknüpfung zur Publikation in Scopus

1 Laufend
3 Abgeschlossen

Embedded Automotive Systems
Baunach, M. C., Batista Ribeiro, L., Martins Gomes, R., Malenko, M., Scheipel, T. P., Saikia, A., Nagarajan, D., Manjunath, V., Kissich, M. & Kanics, K.
1/09/14 → …
Projekt: Arbeitsgebiet
Verlaesslichkeit im Internet der Dinge
Boano, C. A., Kubin, G., Bloem, R., Horn, M., Pernkopf, F., Zakany, N., Mangard, S., Witrisal, K., Römer, K. U., Aichernig, B., Bösch, W., Baunach, M. C., Tappler, M., Malenko, M., Weiser, S., Eichlseder, M., Leitinger, E., Grosinger, J., Großwindhager, B., Ebrahimi, M., Alothman Alterkawi, A. B., Knoll, C., Teschl, R., Saukh, O., Rath, M., Steinberger, M., Steinbauer-Wagner, G. & Tranninger, M.
1/01/16 → 31/03/22
Projekt: Forschungsprojekt
Betriebssysteme für eingebettete Systeme
Baunach, M. C., Martins Gomes, R., Batista Ribeiro, L., Malenko, M., Mauroner, F. & Scheipel, T. P.
1/09/15 → 31/12/23
Projekt: Forschungsprojekt

Dieses zitieren

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. S. 1156-1165 (Proceedings of the ACM Symposium on Applied Computing).

Publikation: Beitrag in Buch/Bericht/Konferenzband › Beitrag in einem Konferenzband › Begutachtung

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, S. 1156-1165, 37th ACM/SIGAPP Symposium On Applied Computing, Virtuell, USA / Vereinigte Staaten, 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

Publikationsreihe

Konferenz

ASJC Scopus subject areas

Fields of Expertise

UN SDGs

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Projekte

Embedded Automotive Systems

Verlaesslichkeit im Internet der Dinge

Betriebssysteme für eingebettete Systeme

Dieses zitieren