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

^*Corresponding author for this work

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

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.

Original language	English
Title of host publication	Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings
Subtitle of host publication	18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings
Editors	Frank de Boer, Antonio Cerone
Publisher	Springer International
Pages	155-174
Number of pages	20
ISBN (Electronic)	978-3-030-58768-0
ISBN (Print)	9783030587673
DOIs	https://doi.org/10.1007/978-3-030-58768-0_9
Publication status	Published - 2020
Event	18th International Conference on Software Engineering and Formal Methods: SEFM 2020 - Virtuell, Amsterdam, Netherlands Duration: 14 Sept 2020 → 18 Sept 2020

Publication series

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

Conference

Conference	18th International Conference on Software Engineering and Formal Methods
Abbreviated title	SEFM 2020
Country/Territory	Netherlands
City	Virtuell, Amsterdam
Period	14/09/20 → 18/09/20

Keywords

Verification
Refinement
Portability
RTOS
Event-B

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Fields of Expertise

Information, Communication & Computing

Access to Document

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

Cite this

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 (Eds.), Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings (pp. 155-174). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 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. ed. / Frank de Boer; Antonio Cerone. Springer International, 2020. p. 155-174 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12310 LNCS).

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

Martins Gomes, R, Aichernig, B & Baunach, MC 2020, A Formal Modeling Approach for Portable Low-Level OS Functionality. in F de Boer & A Cerone (eds), 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), vol. 12310 LNCS, Springer International, pp. 155-174, 18th International Conference on Software Engineering and Formal Methods, Virtuell, Amsterdam, Netherlands, 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, editors, 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. p. 155-174. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2020 Sept 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. editor / Frank de Boer ; Antonio Cerone. Springer International, 2020. pp. 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

Publication series

Conference

Keywords

ASJC Scopus subject areas

Fields of Expertise

Access to Document

Other files and links

Fingerprint

Embedded Operating Systems

Reconfigurable Processor Architectures

Embedded Automotive Systems

Best paper award SEFM 2020

Cite this

A Formal Modeling Approach for Portable Low-Level OS Functionality

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Fields of Expertise

Access to Document

Other files and links

Fingerprint

Projects

Embedded Operating Systems

Reconfigurable Processor Architectures

Embedded Automotive Systems

Prizes

Best paper award SEFM 2020

Cite this