%0 Conference Proceedings
%F leborgne96
%A Le Borgne, M.
%A Marchand, H.
%A Rutten, E.
%A Samaan, M.
%T Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller
%B Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology AMAST'96
%P 271-285
%I Springer-Verlag, LNCS 1101
%C Munich, Germany
%X We present a methodology for the verification of reactive systems, and its application to a case study. Systems are specified using the synchronous data flow language Signal. As this language is based on an equational approach (ie Signal programs are constraint equations between signals), it is natural to translate its boolean part into a system of polynomial equations over three values denoting <i>true</i>, <i> false</i> and <i> absent</i> (ie over Z/3Z). Using operations in algebraic geometry of polynomials, it is possible to check properties concerning the system, such as liveness, invariance, reachability and attractivity. We apply this method to the verification of the automatic circuit-breaking control system of an electric power transformer station. This system handles the reaction to electrical defects on high voltage lines
%U http://www.irisa.fr/vertecs/Publis/Ps/996-AMAST.pdf
%8 July
%D 1996