Formal verification of programs specified with signal f 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 mathe- matical model that supports the various phases of the development of a control system' specifi- cation, verification, simulation, code generation, and implementation. The complex hierarchical, state-based and preemptive behavior of the power station controller is specified in SIGNAL GTi, 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.