Correct Transformation of High-Level Models into Time-Triggered Implementations

A number of component-based frameworks have been proposed to tackle the complexity of the design of concurrent software and systems and, in particular, to allow modelling and simulation of critical embedded applications. Such design frameworks usually provide a capability for automatic generation of C++ or Java code, which has to be compiled for the selected target platform. Thus, guaranteeing hard real-time constraints is, at best, difficult. On the other hand, a variety of Real-Time Operating System (RTOS), in particular, those based on the Time-Triggered (TT) paradigm, guarantee the temporal and behavioural determinism of the executed software. However, such TT-based RTOS do not provide high-level design frameworks enabling the scalable design of complex safety-critical real-time systems. In this report, we combine advantages of the two approaches, by deriving correct-by-construction TT implementations from high-level componentised models. We present an automatic semantics-preserving transformation from RT-BIP (Real-Time Behaviour-Interaction-Priority) to PharOS—a safety-oriented RTOS, implementing the TT paradigm. The transformation has been implemented; we prove its correctness and illustrate it with a realistic case-study.