H. Marchand, E. Rutten, M. Le Borgne, M. Samaan. Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller. Science of Computer Programming, 2000.
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
@article{marchand00g,
Author = {Marchand, H. and Rutten, E. and Le Borgne, M. and Samaan, M.},
Title = {Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller},
Journal = {Science of Computer Programming},
Year = {2000}
}
Get EndNote Reference (.ref)
This page is part the Espresso project web site.
It has been automatically generated using the bib2html program.