Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |
Download paper Adobe portable document format (pdf)
Copyright noticeThis 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.
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.
Hervé Marchand
hmarchan@irisa.fr
@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}
}
Get EndNote Reference (.ref)