A methodology for proving control systems with Lustre and PVS

Saddek Bensalem, Paul Caspi, Catherine Parent Vigouroux and Cécile Dumas Canovas

Seventh Working Conference on Dependable Computing for Critical Applications (DCCA7), San Jose, January 1999


In this paper, we intend to show how to use the synchronous data-flow language Lustre, combined with the PVS proof system in deriving provably-correct (distributed) control programs. We hopefully illustrate, based on a railway emergency braking system example, the features of our approach --- asynchronous periodic programs with nearly the same period, communicating by sampling --- equational reasoning which leaves to the Lustre compiler the task of scheduling computations --- no distinction between control programs and physical environments which are sampled in the same way. This allows us to provide ``elementary'' proofs based on difference equations instead of differential ones which require more involved PVS formalization.

Postscript