leborgne96

M. Le Borgne, H. Marchand, E. Rutten, M. Samaan. Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller. In Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology AMAST'96, Pages 271-285, Munich, Germany, July 1996.

Download [help]

Download paper: Adobe portable document (pdf)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

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 true, false and absent (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

Contact

Hervé Marchand http://www.irisa.fr/prive/hmarchan

BibTex Reference

@InProceedings{leborgne96,
   Author = {Le Borgne, M. and Marchand, H. and Rutten, E. and Samaan, M.},
   Title = {Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller},
   BookTitle = {Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology AMAST'96},
   Pages = {271--285},
   Publisher = {Springer-Verlag, LNCS 1101},
   Address = {Munich, Germany},
   Month = {July},
   Year = {1996}
}

EndNote Reference [help]

Get EndNote Reference (.ref)