A methodology for proving control systems with Lustre and PVS

We intend to show how to use the synchronous dataflow 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.