Flush : A System Development Tool Based on Scade/Lustre

Abstract : In safety-critical control systems, the Scade/Lustre development environment has proved its value, with notable achievements such as the Hong-Kong subway signalling system and Airbus A380 flight controls. The interest of the approach comes from the synchronous data-flow style of the Lustre language which makes is well-adapted to the culture of control engineers. At the same time Lustre is endowed with simple formal semantics which makes it amenable to formal development. The currently running Flush project consists of building a formal system development tool on top of it, by taking advantage of the formal properties of the Lustre language. To this end, a refinement calculus is defined, encompassing both functional and temporal aspects. Refinement proof obligations are generated, and several proof approaches can be used to discharge them: model-checking, abstract interpretation, and theorem proving through repeated induction and, finally translation to PVS proof obligations. The resulting methodology is illustrated on the island example used by J.R. Abrial for presenting the B system method.
Type de document :
Communication dans un congrès
T. Margaria and M. Massink. FMICS, Sep 2005, Lisbon, Portugal. ACM, pp.27-34, 2005, FMICS '05: Proceedings of the 10th international workshop on Formal methods for industrial critical systems. 〈10.1145/1081180.1081185〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00466170
Contributeur : Jan Mikac <>
Soumis le : lundi 22 mars 2010 - 21:07:21
Dernière modification le : vendredi 6 juillet 2018 - 10:08:02
Document(s) archivé(s) le : vendredi 25 juin 2010 - 11:56:15

Fichier

f23-mikac.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Jan Mikac, Paul Caspi. Flush : A System Development Tool Based on Scade/Lustre. T. Margaria and M. Massink. FMICS, Sep 2005, Lisbon, Portugal. ACM, pp.27-34, 2005, FMICS '05: Proceedings of the 10th international workshop on Formal methods for industrial critical systems. 〈10.1145/1081180.1081185〉. 〈inria-00466170〉

Partager

Métriques

Consultations de la notice

200

Téléchargements de fichiers

680