Code Generation from Formal Models for Automatic RTOS Portability

Renata Martins Gomes, Marcel Carsten Baunach

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem KonferenzbandBegutachtung


Current approaches for portability of real-time operating systems (RTOSs) for embedded systems are largely based on manual coding, which is arduous and error prone. With increasing dependability requirements for cyber physical systems, specially within the Internet of Things (IoT), along with the expected great diversity of hardware platforms, software platforms will only remain competitive in the long run if they guarantee correct operation and easy deployment to every hardware platform. In this scenario, a new approach to the development and portability of RTOSs that guarantees correct implementations for all current and future devices and hardware architectures becomes indispensable.

We present a framework for automatic RTOS portability that integrates model-based design and formal methods into dependable embedded software development. We focus specially on modeling the interaction between software and hardware in order to generate low-level code. This enables automatic portability for hardware-related parts of the OS (i.e., context switching, memory management, security aspects, etc,) as well as for on-chip peripheral drivers (i.e., timers, I/O, etc.).

With our framework we will be able to prove the consistency of the refinements as well as that the RTOS model fulfills various functional and non-functional requirements. Automatic code generation guarantees that the model is correctly translated to machine language, avoiding implementation mistakes common to manual coding. Changes on the software, for bug fixes or testing of new concepts, for example, do not require knowledge of the target architectures, since they are done on the model and are immediately reflected in all implementations upon code generation, assuring consistency across platforms.
TitelCGO 2019: Proceedings of the 2019 IEEE/ACM International Symposium on Code Generation and Optimization
Herausgeber (Verlag)IEEE Press
ISBN (elektronisch)978-1-7281-1436-1
PublikationsstatusVeröffentlicht - 4 Jan. 2019
VeranstaltungInternational Symposium on Code Generation and Optimization - Washington DC, Washington DC, USA / Vereinigte Staaten
Dauer: 16 Feb. 201920 Feb. 2019


KonferenzInternational Symposium on Code Generation and Optimization
Land/GebietUSA / Vereinigte Staaten
OrtWashington DC


Untersuchen Sie die Forschungsthemen von „Code Generation from Formal Models for Automatic RTOS Portability“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren