Formal verification of Signal programs: Application to a power transformer station controller

International audience; 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 (i.e. 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 true, false and absent. Using operations in algebraic geometry on the 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.