*********************************************************************
* Ecole Normale Supe'rieure *
* *
* Se'minaire *
* SEMANTIQUE ET INTERPRETATION ABSTRAITE *
* P. Cousot *
* *
* Vendredi, 14h00--15h30 *
* Salle W, 4e`me e'tage, toits du DMI *
* DMI ENS 45 rue d'Ulm 75005 Paris *
*********************************************************************
*** Vendredi 2 mai 1997 **** 14h00 **********************************
Relache (pont du 1er mai)
*** Vendredi 9 mai 1997 **** 14h00 **********************************
Relache (pont du 8 mai)
*** Vendredi 16 mai 1997 **** 14h00 *********************************
Compositional Verification of Statecharts
Francesca LEVI (LIX et Universite de Pise)
Re'sume' : Abstract: We present a compositional approach for the verification
of temporal and real-time properties of statecharts. Statecharts
is a synchronous language that is obtained by extending classical
state-transition diagrams with notions of parallelism, broadcast communication
and hierarchy. These features have been shown to
permit very elegant and modular specifications. However,
the synchrony hypothesis leads to some drawbacks in the definition
of a formal semantics, because of well-known causal paradoxes.
The first result is the definition of a compositional labelled
transition system semantics for
statecharts that provides the basis for compositional verification.
Such a semantics is obtained by translating statecharts into a new
process language called SP, that is characterized by an operator of
process refinement for representing the statecharts hierarchy. We show
how to instantiate the basic actions and the operations over actions of SP
in order to have
processes agreeing with the Pnueli and Shalev semantics of statecharts.
We define a compositional proof system for checking whether an SP
process satisfies a mu-calculus formula. This proof system exploits
the technique of tagging fixpoints of Winskel for supporting local
model checking. It is proved to be sound in general and complete for
finite-state processes, i.e. for statecharts.
Finally, we show how this compositional approach to verification can
be adapted to a discrete timed version of statechart by considering
an extension of mu-calculus with freeze quantification and clock
constraints. The main idea is that of considering judgments relativized
MOREto clock constraints and of adapting the tagged fixpoints method to
this framework.
*** Vendredi 23 mai 1997 **** 14h00 *********************************
Relache.
*** Vendredi 30 mai 1997 **** 14h00 *********************************
Relache (jury du corps des ponts et chaussees)
*********************************************************************
Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr
WWW: http://www.ens.fr/~cousot/annonceseminaire.html
*********************************************************************