Skip to Main content Skip to Navigation
Journal articles

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

Hervé Marchand 1 Eric 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.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/inria-00526287
Contributor : Hervé Marchand <>
Submitted on : Thursday, October 14, 2010 - 11:07:52 AM
Last modification on : Thursday, February 11, 2021 - 2:48:04 PM

Links full text

Identifiers

Citation

Hervé Marchand, Eric 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⟩

Share

Metrics

Record views

327