Static verifications

  • Nicolas Halbwachs
Part of the The Springer International Series in Engineering and Computer Science book series (SECS, volume 215)


As seen in §2.5, an Esterel program can raise some temporal paradoxes, which involve either the absence of any behavior or a non-deterministic behavior. This phenomenon, which appears in all really synchronous languages, comes from the fact that a program reaction, while considered instantaneous, is made up of a sequence of elementary actions (sometimes called “microsteps” [HPSS86]) that are performed in fixed order 1: the first statement of a sequence is performed “before” the second one, a “present S do <stat>” statement checks the presence of S “before” any signal emission involved by “<stat>,” and so forth.


Boolean Expression Static Verification Causality Loop Input Part Program Fragment 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media Dordrecht 1993

Authors and Affiliations

  • Nicolas Halbwachs
    • 1
  1. 1.IMAG InstituteGrenobleFrance

Personalised recommendations