A methodology for proving control systems with Lustre and
PVS
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