%0 Journal Article 
%F marchand01a
%A Marchand, H.
%A Rutten, E.
%A Le Borgne, M.
%A Samaan, M.
%T Formal Verification of programs specified with SIGNAL : Application to a Power Transformer Station Controller
%J Science of Computer Programming
%V 41
%N 1
%P 85-104
%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
%U http://www.irisa.fr/vertecs/Publis/Ps/2001-JSCP.pdf
%U http://dx.doi.org/10.1016/S0167-6423(00)00020-4
%8 August
%D 2001