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/KonferenzbandBeitrag in einem KonferenzbandBegutachtung


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.

TitelSoftware Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings
Untertitel18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings
Redakteure/-innenFrank de Boer, Antonio Cerone
Herausgeber (Verlag)Springer International
ISBN (elektronisch)978-3-030-58768-0
ISBN (Print)9783030587673
PublikationsstatusVeröffentlicht - 2020
Veranstaltung18th International Conference on Software Engineering and Formal Methods: SEFM 2020 - Virtuell, Amsterdam, Niederlande
Dauer: 14 Sep. 202018 Sep. 2020


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


Konferenz18th International Conference on Software Engineering and Formal Methods
KurztitelSEFM 2020
OrtVirtuell, Amsterdam

ASJC Scopus subject areas

  • Theoretische Informatik
  • Informatik (insg.)

Fields of Expertise

  • Information, Communication & Computing


Untersuchen Sie die Forschungsthemen von „A Formal Modeling Approach for Portable Low-Level OS Functionality“. Zusammen bilden sie einen einzigartigen Fingerprint.
  • Best paper award SEFM 2020

    Martins Gomes, Renata (Empfänger/-in), Aichernig, Bernhard (Empfänger/-in) & Baunach, Marcel Carsten (Empfänger/-in), 17 Sep. 2020

    Auszeichnung: Preise / Medaillen / Ehrungen

Dieses zitieren