*********************************************************************
*                       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
*********************************************************************