Technical Reports

Jan Mikac, Paul Caspi
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.

Contact | Site Map | Site powered by SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4199681