Code Generation from Formal Models for Automatic RTOS Portability

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.