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 proceedingConference contribution

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 languageEnglish
Title of host publicationSoftware Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings
Subtitle of host publication18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings
EditorsFrank de Boer, Antonio Cerone
PublisherSpringer International
Pages155-174
Number of pages20
ISBN (Electronic)978-3-030-58768-0
ISBN (Print)9783030587673
DOIs
Publication statusE-pub ahead of print - 8 Sep 2020
Event18th International Conference on Software Engineering and Formal Methods - Virtuell
Duration: 14 Sep 202018 Sep 2020

Publication series

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

Conference

Conference18th International Conference on Software Engineering and Formal Methods
Abbreviated titleSEFM 2020
CityVirtuell
Period14/09/2018/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

Fingerprint Dive into the research topics of 'A Formal Modeling Approach for Portable Low-Level OS Functionality'. Together they form a unique fingerprint.

Cite this