Database of Research Tools Developed Using CADP

Meta-Modeling Tool [εm] for Analysis of Process Models

Organisation: University of Münster, School of Business & Economics

Functionality: Process model analysis

Tools used: CADP (Construction and Analysis of Distributed Processes)

Period: 2016 - 2017

Description: [εm] is a meta modeling tool that allows a user to create a definition of a modeling language and then use this language definition to create models in the defined language. [εm] features a plugin, which, given (1) a model, (2) its meta model, (3) a meta model-based execution semantics, and (4) a formal temporal property, we want to use model checking to determine the fulfillment of the given temporal property by the given model, and to get a hint why the property is fulfilled or why it is not, respectively.

The plugin works by translating the various inputs describing a process model to the LNT and MCL languages supported by CADP. First, the [εm] data types used by the processes are translated to LNT data types. Second, the behaviour of the processes, specified in ESDL (Execution Semantics Description Language), are also translated to LNT; this translation requires two steps, the translation of the expressions and parameters that are used by the parametric process schemes translated into LNT processes. In all these translation steps, the meta model is required to generate parsers for the input languages.

The properties to be checked are translated to MCL. To facilitate the expression of properties, the plugin offers a temporal property specification wizard, which guides users by asking a sequence of questions, each taking into account the answers to the previous one, so as to select an appropriate pattern, from which the temporal property is automatically generated. This property is then translated to MCL.

In a last step, the EVALUATOR tool is used for model checking. Besides checking the property on-the-fly, the plugin also supports the reduction of the correpsonding LTS with respect to safety equivalence. The latter approach requires the generation of the complete LTS, but yields witnesses that are easier to understand. In order to provide meaningful feedback to the designer, the translation renames transition labels, adding information about the processes involved in the action, thus making it possible to distinguish between similar actions performed by different processes.

Conclusions: After a survey of model checkers, CADP was selected because the model checkeer EVALUATOR generates witnesses that can easily be converted into a format related to the original model.

Publications: [Pribnow-17] Hauke Pribnow. "Leveraging Propositional Logic-Based Model Checking to Enable Convenient Analysis of Process Models in Arbitrary Graph-Based Process Modeling Languages". Masters thesis at the Chair for Information Systems and Information Management (Westfälische Wilhelms-Universität, Münster), December 2017.
Available on-line at:
or from our FTP site in PDF or PostScript

Contact:
Hauke Pribnow (Uni Muenster),
University of Münster, School of Business & Economics
Universitätsstraße 14-16
48143 Münster
Germany



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Wed Apr 24 17:57:17 2019.


Back to the CADP research tools page