POEM (Partial Order Environment of Marseille) is a modular model checking tool built to support several input languages, several analysis and solving algorithms. POEM provides reusable code for some powerful partial order based model checking algorithms. POEM consists of a set of modules interconnected : first, a model and a property are parsed by a frontend according to its language and represented with the global data structure GDS which plays the role of a bus for the three subsystems. core analyses and transforms the GDS structure in performing type checking, constant propagation, model transformation, transition generation including dependency analysis for partial order algorithms, etc. The result of this analysis is passed to the backend that implements solving algorithms to check the property. The core then transforms the findings (e.g. a trace) into an XML file that is readable by a GUI and allows the latter to visualise the found execution with a link to the source code.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element