A methodology for proving control systems with Lustre and PVS
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
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.Keywords
This publication has 6 references indexed in Scilit:
- Safety verification for automated platoon maneuvers: A case studyPublished by Springer Nature ,1997
- The temporal logic of actionsACM Transactions on Programming Languages and Systems, 1994
- Programming and verifying real-time systems by means of the synchronous data-flow language LUSTREIEEE Transactions on Software Engineering, 1992
- The synchronous data flow programming language LUSTREProceedings of the IEEE, 1991
- The calculus of constructionsInformation and Computation, 1988
- A functional model for describing and reasoning about time behaviour of computing systemsActa Informatica, 1986