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
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo: Exploiting step semantics for efficient bounded model checking of asynchronous systems (2012)
- Herbreteau, Frédéric; Kini, Dileep; Srivathsan, B.; Walukiewicz, Igor: Using non-convex approximations for efficient analysis of timed automata (2011)
- Malinowski, Janusz; Niebert, Peter: SAT based bounded model checking with partial order semantics for timed automata (2010)
- Santocanale, Luigi: A Nice labelling for tree-like event structures of degree 3 (2010)
- Esparza, Javier; Heljanko, Keijo: Unfoldings: A partial-order approach to model checking. (2008)
- Kurbán, Marcos E.; Niebert, Peter; Qu, Hongyang; Vogler, Walter: Stronger reduction criteria for local first search (2006)
- Niebert, Peter; Qu, Hongyang: The implementation of Mazurkiewicz traces in POEM (2006)