%0 Journal Article 
%F marchand00g
%A Marchand, H.
%A Rutten, E.
%A Le Borgne, M.
%A Samaan, M.
%T Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller
%J Science of Computer Programming
%X 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
%D 2000