Verimag

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 | Plan du site | Site réalisé avec SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 915493