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 Konferenzband

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.

Originalspracheenglisch
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
Seiten155-174
Seitenumfang20
ISBN (elektronisch)978-3-030-58768-0
ISBN (Print)9783030587673
DOIs
PublikationsstatusElektronische Veröffentlichung vor Drucklegung. - 8 Sep 2020
Veranstaltung18th International Conference on Software Engineering and Formal Methods: SEFM 2020 - Virtuell, Amsterdam, Niederlande
Dauer: 14 Sep 202018 Sep 2020

Publikationsreihe

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

Konferenz

Konferenz18th International Conference on Software Engineering and Formal Methods
KurztitelSEFM 2020
LandNiederlande
OrtVirtuell, Amsterdam
Zeitraum14/09/2018/09/20

ASJC Scopus subject areas

  • !!Theoretical Computer Science
  • !!Computer Science(all)

Fields of Expertise

  • Information, Communication & Computing

Fingerprint

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

Dieses zitieren