Accès aux Résumé | Contact | Référence BibTex | Référence EndNote |

marchand00g

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.

Résumé

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

Contact

Hervé Marchand
Eric Rutten

Référence BibTex

@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}
}

Référence EndNote [help]

Charger la référence EndNote (.ref)

This page is part the Espresso project web site.
It has been automatically generated using the bib2html program.