5th International Workshop on

Formal Methods for Industrial Critical Systems

Berlin, April 3-4, 2000

Applying Formal Methods to Industrial Cases: The Language Approach

In this paper we comment on the "language approach" to applying formal methods to real industrial problems. Our opinion is that it is always a good idea to let the user tell as much as he knows about the structure of a complex system. When he has a given structure in mind but needs to encode it into the available constructs of a language, the interesting information is likely to be lost somewhere on the way from the original design to the actual implementation. This may have consequences on the efficiency of the code produced, or even on the correctness of the design.

Following this idea, the family of synchronous languages [BB91] has been very successful in offering domain-specific, formally defined languages and programming environments for safety-critical systems. We are particularly interested in the data-flow language Lustre, well-suited for the description of regulation systems. These systems are often specified using the notion of running modes, which appears in informal designs. However, there seemed to exist no language in which the mode-structure of a complex system could be expressed directly. We proposed to extend Lustre with a new construct devoted to the description of these running modes of regulation systems.

The language extension is based upon the model of mode-automata [MR98]. We now have a running implementation of this extension [MRR00], which has been applied successfully to the industrial case-studies of the SYRF project [SYR99], proposed by SAAB M.A. (a temperature regulation system) and Schneider Electric (the control of the starting and shut-down phases in a nuclear plant).

We are now working on a case-study proposed by Aerospatiale (a piece of software of the Airbus A340-600, for the development of which Aerospatiale has chosen SCADE, the commercial version of Lustre), under a non-disclosure agreement. However, some of the ideas that this example already suggested to us can also be illustrated with a simpler example. In this paper we show how to program the production-cell case-study [LL95] using mode-automata (a pure Lustre version, written by Leszek Holenderski at GMD Birlinghoven, appeared in [LL95]). We used the environment simulator in TCL-TK provided by FZI Karlsruhe.

Note: The content of the following files is part of GMD Report No. 91 and subject to its copyright.

ERCIM FMICS Home Page, GMD FOKUS Home Page

Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST, Axel Rennoch