Jan Mikac, Paul Caspi
Formal System Development with Lustre: Framework and Example (2005)
Formal System Development with Lustre: Framework and Example (2005)
TR-2005-11.pdf
Keywords: Lustre, refinement, temporal refinement
Abstract: This paper proposes a refinement framework for Lustre. First a very general calculus is provided, which ensures correctness and reactivity for a large class of systems. Then, this calculus is adapted to provide oversampling and temporal refinement. We obtain thus an effective calculus for Lustre, which allows us to refine both computations and time. The calculus and its use in the development of reactive systems are illustrated on the island example used by J.R. Abrial for presenting the B system method.
