Formal verification of programs specified with signal: application to a power transformer station controller

Hervé Marchand 1 Éric Rutten 2 Michel Le Borgne 3 Mazen Samaan 4
1 EP-ATR - Environnement de programmation d'applications temps réel
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
2 BIP - Biped Robot
Inria Grenoble - Rhône-Alpes
3 AIDA - Modeling and Machine Learning for Data Interpretation and Decision Assistance
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : We present a formal specification and verification of the automatic circuit-breaking behavior of an electric power transformer station, using the synchronous approach to reactive real-time systems implemented by the data-flow language Signal. Synchronous languages have a mathematical model that supports the various phases of the development of a control system: specification, verification, simulation, code generation, and implementation. The complex hierarchical, state-based and preemptive behavior of the power station controller is specified in Signalgti, an extension of Signal with notions of time intervals and preemptive tasks. To validate the specification, a graphical simulator is generated using Signal's execution environment, and the required behaviour is proven to be satisfied, using its proof method.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2001, 41 (1), pp.85-104. 〈10.1016/S0167-6423(00)00020-4〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00526287
Contributeur : Hervé Marchand <>
Soumis le : jeudi 14 octobre 2010 - 11:07:52
Dernière modification le : mercredi 16 mai 2018 - 11:23:02

Lien texte intégral

Identifiants

Collections

Citation

Hervé Marchand, Éric Rutten, Michel Le Borgne, Mazen Samaan. Formal verification of programs specified with signal: application to a power transformer station controller. Science of Computer Programming, Elsevier, 2001, 41 (1), pp.85-104. 〈10.1016/S0167-6423(00)00020-4〉. 〈inria-00526287〉

Partager

Métriques

Consultations de la notice

159