Communication Protocols Verification with Esterel
J. Graña Gil
M. Vilares Ferro
R. Bernhard
Abstract
This work summarizes design, implementation and verification processes of a
digital telephone switchboard in the
Esterel
real-time programming environment. Our aim is to show the modularity
in the description and of flexibility in the verification process.
We also show the control synchronization mechanisms to coordinate
concurrent processes. The goal is to prevent in compile-time deadlock
and lockout phenomena, a feature that is not available in most programming
languages.
Key words: Synchronous Programming, Reactive Systems,
Automata Verification.
The present work was partially supported by projects XUGA10501A93, XUGA10501B93
and XUGA10502B94 from the Xunta de Galicia, the Autonomous Government of
Galicia.
Jorge Graña Gil
/
grana@dc.fi.udc.es