Abstract :
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
Keywords :
automata theory; computerised control; parallel languages; program diagnostics; programming environments; real-time systems; safety-critical software; Lustre language extension; Saab; case study; compiled sequential code efficiency; data-flow language; formally defined languages; hint transmission; language features; mode automata; mode expression; programming environments; readability; real-time systems; regulation systems; running implementation; running modes; safety-critical systems; static analysis; synchronous languages; verification tools; worst-case execution time evaluation; Aircraft; Cost accounting; Documentation; Embedded system; Equations; Formal specifications; Job shop scheduling; Mathematical model; Real time systems; Service robots;
