View article

We investigate the bene ts of using a synchronous data-ow language for programming critical real-time systems. These bene ts concern ergonomy| since the data ow approach meets traditional description tools used in this domain|, and ability to support formal design and veri cation methods. We show, on a simple example, how the language Lustre and its associated veri cation tool Lesar, can be used to design a program, to specify its critical properties, and to verify these properties. As the language Lustre and its use have been already published in several papers (eg, 11, 18]), we put particular emphasis on program veri cation. A preliminary version of this paper has been published in 28].