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

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 SIGNALGTι̇, 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 behavior is proven to be satisfied, using its proof method.