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 the CADP Web 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

Back to the CADP research tools page