MIMOS: A Deterministic Model for the Design and Update of Real-Time Systems

Inspired by the pioneering work of Gilles Kahn on concurrent systems, we model real-time systems as a network of software components each of which is specified to compute a collection of functions according to given timing constraints. The components communicate with each other and their environment via two types of channels: (1) FIFO queues for buffering data, and (2) Registers for sampling time-dependent data streams from sensors or output streams of other components executed at different rates. We present a fixed-point semantics for this model which shows that each system function of a network computes for a given set of input (timed) streams, a unique (timed) output stream. Thanks to the deterministic semantics, a model-based approach is enabled for not only building systems but also updating them after deployment, allowing model-in-the-loop simulation to verify the complete behaviour of the resulting system.