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