A Formal Modeling Approach for Portable Low-Level OS Functionality

Renata Martins Gomes; Bernhard Aichernig; Marcel Carsten Baunach

doi:10.1007/978-3-030-58768-0_9

A Formal Modeling Approach for Portable Low-Level OS Functionality

Renata Martins Gomes^*, Bernhard Aichernig, Marcel Carsten Baunach

^*Korrespondierende/r Autor/-in für diese Arbeit

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

Abstract

The increasing dependability requirements and hardware diversity of the Internet of Things (IoT) pose a challenge to developers. New approaches for software development that guarantee correct implementations will become indispensable. Specially for Real Time Operating Systems (RTOSs), automatic porting for all current and future devices will also be required. As part of our framework for embedded RTOS portability, based on formal methods and code generation, we present our approach to formally model low-level operating-system functionality using Event-B. We show the part of our RTOS model where the switch into the kernel and back to a task happens, and prove that the model is correct according to the specification. Hardware details are only introduced in late refinements, which allows us to reuse most of the RTOS model and proofs for several target platforms. As a proof of concept, we refine the generic model to two different architectures and prove safety and liveness properties of the models.

Originalsprache	englisch
Titel	Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings
Untertitel	18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings
Redakteure/-innen	Frank de Boer, Antonio Cerone
Herausgeber (Verlag)	Springer International
Seiten	155-174
Seitenumfang	20
ISBN (elektronisch)	978-3-030-58768-0
ISBN (Print)	9783030587673
DOIs	https://doi.org/10.1007/978-3-030-58768-0_9
Publikationsstatus	Veröffentlicht - 2020
Veranstaltung	18th International Conference on Software Engineering and Formal Methods: SEFM 2020 - Virtuell, Amsterdam, Niederlande Dauer: 14 Sept. 2020 → 18 Sept. 2020

Publikationsreihe

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Band	12310 LNCS
ISSN (Print)	0302-9743
ISSN (elektronisch)	1611-3349

Konferenz

Konferenz	18th International Conference on Software Engineering and Formal Methods
Kurztitel	SEFM 2020
Land/Gebiet	Niederlande
Ort	Virtuell, Amsterdam
Zeitraum	14/09/20 → 18/09/20

ASJC Scopus subject areas

Theoretische Informatik
Informatik (insg.)

Fields of Expertise

Information, Communication & Computing

Zugriff auf Dokument

10.1007/978-3-030-58768-0_9

Andere Dateien und Links

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

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

Best paper award SEFM 2020
Martins Gomes, Renata (Empfänger/-in), Aichernig, Bernhard (Empfänger/-in) & Baunach, Marcel Carsten (Empfänger/-in), 17 Sept. 2020
Auszeichnung: Preise / Medaillen / Ehrungen

Dieses zitieren

Martins Gomes, R., Aichernig, B., & Baunach, M. C. (2020). A Formal Modeling Approach for Portable Low-Level OS Functionality. in F. de Boer, & A. Cerone (Hrsg.), Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings (S. 155-174). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12310 LNCS). Springer International. https://doi.org/10.1007/978-3-030-58768-0_9

A Formal Modeling Approach for Portable Low-Level OS Functionality. / Martins Gomes, Renata; Aichernig, Bernhard ; Baunach, Marcel Carsten.
Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings. Hrsg. / Frank de Boer; Antonio Cerone. Springer International, 2020. S. 155-174 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12310 LNCS).

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

Martins Gomes, R, Aichernig, B & Baunach, MC 2020, A Formal Modeling Approach for Portable Low-Level OS Functionality. in F de Boer & A Cerone (Hrsg.), Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bd. 12310 LNCS, Springer International, S. 155-174, 18th International Conference on Software Engineering and Formal Methods, Virtuell, Amsterdam, Niederlande, 14/09/20. https://doi.org/10.1007/978-3-030-58768-0_9

Martins Gomes R, Aichernig B , Baunach MC. A Formal Modeling Approach for Portable Low-Level OS Functionality. in de Boer F, Cerone A, Hrsg., Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings. Springer International. 2020. S. 155-174. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2020 Sep 8. doi: 10.1007/978-3-030-58768-0_9

Martins Gomes, Renata ; Aichernig, Bernhard ; Baunach, Marcel Carsten. / A Formal Modeling Approach for Portable Low-Level OS Functionality. Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings. Hrsg. / Frank de Boer ; Antonio Cerone. Springer International, 2020. S. 155-174 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2905e1d59b604dd98bd9ad6187332ac7,

title = "A Formal Modeling Approach for Portable Low-Level OS Functionality",

abstract = "The increasing dependability requirements and hardware diversity of the Internet of Things (IoT) pose a challenge to developers. New approaches for software development that guarantee correct implementations will become indispensable. Specially for Real Time Operating Systems (RTOSs), automatic porting for all current and future devices will also be required. As part of our framework for embedded RTOS portability, based on formal methods and code generation, we present our approach to formally model low-level operating-system functionality using Event-B. We show the part of our RTOS model where the switch into the kernel and back to a task happens, and prove that the model is correct according to the specification. Hardware details are only introduced in late refinements, which allows us to reuse most of the RTOS model and proofs for several target platforms. As a proof of concept, we refine the generic model to two different architectures and prove safety and liveness properties of the models.",

keywords = "Verification, Refinement, Portability, RTOS, Event-B",

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

year = "2020",

doi = "10.1007/978-3-030-58768-0_9",

language = "English",

isbn = "9783030587673",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer International",

pages = "155--174",

editor = "{de Boer}, Frank and Antonio Cerone",

booktitle = "Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings",

note = "18th International Conference on Software Engineering and Formal Methods : SEFM 2020, SEFM 2020 ; Conference date: 14-09-2020 Through 18-09-2020",

}

TY - GEN

T1 - A Formal Modeling Approach for Portable Low-Level OS Functionality

AU - Martins Gomes, Renata

AU - Aichernig, Bernhard

AU - Baunach, Marcel Carsten

PY - 2020

Y1 - 2020

N2 - The increasing dependability requirements and hardware diversity of the Internet of Things (IoT) pose a challenge to developers. New approaches for software development that guarantee correct implementations will become indispensable. Specially for Real Time Operating Systems (RTOSs), automatic porting for all current and future devices will also be required. As part of our framework for embedded RTOS portability, based on formal methods and code generation, we present our approach to formally model low-level operating-system functionality using Event-B. We show the part of our RTOS model where the switch into the kernel and back to a task happens, and prove that the model is correct according to the specification. Hardware details are only introduced in late refinements, which allows us to reuse most of the RTOS model and proofs for several target platforms. As a proof of concept, we refine the generic model to two different architectures and prove safety and liveness properties of the models.

AB - The increasing dependability requirements and hardware diversity of the Internet of Things (IoT) pose a challenge to developers. New approaches for software development that guarantee correct implementations will become indispensable. Specially for Real Time Operating Systems (RTOSs), automatic porting for all current and future devices will also be required. As part of our framework for embedded RTOS portability, based on formal methods and code generation, we present our approach to formally model low-level operating-system functionality using Event-B. We show the part of our RTOS model where the switch into the kernel and back to a task happens, and prove that the model is correct according to the specification. Hardware details are only introduced in late refinements, which allows us to reuse most of the RTOS model and proofs for several target platforms. As a proof of concept, we refine the generic model to two different architectures and prove safety and liveness properties of the models.

KW - Verification

KW - Refinement

KW - Portability

KW - RTOS

KW - Event-B

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

U2 - 10.1007/978-3-030-58768-0_9

DO - 10.1007/978-3-030-58768-0_9

M3 - Conference paper

SN - 9783030587673

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 155

EP - 174

BT - Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings

A2 - de Boer, Frank

A2 - Cerone, Antonio

PB - Springer International

T2 - 18th International Conference on Software Engineering and Formal Methods

Y2 - 14 September 2020 through 18 September 2020

ER -

A Formal Modeling Approach for Portable Low-Level OS Functionality

Abstract

Publikationsreihe

Konferenz

ASJC Scopus subject areas

Fields of Expertise

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Projekte

Embedded Automotive Systems

Verlaesslichkeit im Internet der Dinge

Betriebssysteme für eingebettete Systeme

Auszeichnungen

Best paper award SEFM 2020

Dieses zitieren