Code Generation from Formal Models for Automatic RTOS Portability

Renata Martins Gomes, Marcel Carsten Baunach

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review


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.
Original languageEnglish
Title of host publicationCGO 2019: Proceedings of the 2019 IEEE/ACM International Symposium on Code Generation and Optimization
PublisherIEEE Press
ISBN (Electronic)978-1-7281-1436-1
Publication statusPublished - 4 Jan 2019
EventInternational Symposium on Code Generation and Optimization - Washington DC, Washington DC, United States
Duration: 16 Feb 201920 Feb 2019


ConferenceInternational Symposium on Code Generation and Optimization
Abbreviated titleCGO2019
Country/TerritoryUnited States
CityWashington DC
Internet address


Dive into the research topics of 'Code Generation from Formal Models for Automatic RTOS Portability'. Together they form a unique fingerprint.

Cite this