Running-modes of real-time systems: a case-study with mode-automata

Real-time systems, in particular regulation systems, are often specified using the notion of running modes. On the other hand, the family of synchronous languages has been very successful in offering formally defined languages and programming environments for safety-critical systems. We are particularly interested in the data-flow language Lustre, which is well-suited for the description of regulation systems. We propose to extend Lustre with a new construct devoted to the description of running modes in regulation systems. This language extension is based upon the mathematical model of mode automata. We now have a running implementation of this extension. In this paper, we comment on a case study proposed by Saab, and argue for the introduction of language features that are devoted to the expression of modes, from different points of view: readability, efficiency of the compiled sequential code, ability to transmit hints to verification tools, accurate evaluation of the worst-case execution time (WCET), static analysis of the resources used, etc