Lieu : CMI, salle 102, le 1/06/06 à 14h00.

Programme :

• Introduction to POEM 30min, Peter Niebert
• Tool Architecture :
  • Static analysis POEM, 30min, Peter Niebert
  • Implementation de Traces de Mazurkiewicz dans POEM, 30min, Hongyang Qu
• Algorithms :
  • Improved LFS algorithm, 30min, Hongyang Qu
  • Partial Order Semantics for Timed Automata with urgency, 30min, Peter Niebert
• Challenges for POEM, 15min, Peter Niebert.

Summary: POEM stands for "Partial Order Environment of Marseille". It is a model checker toolset with an emphasis on partial order semantics. POEM is designed to be extensible for different frontends and backends for the analysis. Currently, a frontend for VERIMAG's IF 2.0 language is operational (although not complete) and another frontend for Promela is nearly operational. On the backend side, currently only state explorers exist for discrete systems and for timed automata. Several algorithms exploiting partial order semantics are integrated into this backend, in particular, it contains an interesting implementation of Mazurkiewicz traces. Future backends might include SAT-based analysis. In order to facilitate the extension of POEM, a lot of code is backend independent, in particular the analysis of dependency among transitions.

A graphical user interface based on Eclipse is under development.

In the presentation, we explain the principles and practice of POEM and hope to shed light on how it can serve in the analysis of concurrent systems.

Transparents.