Database of Research Tools Developed Using CADP

Automated Analysis of Workflow Applications

Organisation: CONVECS team, INRIA, LIG
Naver Labs Europe (formerly Xerox Research Center Europe)

Functionality: Formal Analysis of Mangrove Models

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

Period: 2018

Description: Optimizing a business process aims at saving time and money. The authors propose techniques for the automated formal analysis of business processes modeled in Mangrove, a generic description meta-model unifying businesses processes and service-oriented architectures. Mangrove provides behavioural support, and facilitates the mapping from domain specific languages to standard workflow languages.

The authors developed behavioural and data-based analyses for Mangrove models. For the former, a Mangrove model is transformed into the intermediate format PIF (Process Intermediate Format). This transformation is defined by a set of transformation patterns. PIF is supported by the VBPMN platform, which in turn is connected to the CADP toolbox. This connection makes two different analysis techniques possible. First, it becomes possible to check the existence of deadlocks or livelocks, or even more general temporal logic properties, specified in MCL using well-known property patterns available in CADP. Second, it is also possible to check the equivalence of two process models, which is particularly helpful when assessing the correction of a process evolution.

For data-based analyses, the authors developed a static analysis to check the feasibility of execution paths by encoding Mangrove's condition expressions as satisfiability constraints and evaluating them using the SMT solver Z3.

Conclusions: Mangrove is simple and expressive enough to model realistic business workflows. Through a connection to CADP, formal analysis is automated, enabling the user to assess the correctness of envisioned process evolutions.

Publications: [CortesCornax-Krishna-Mos-Salaun-18] Mario Cortes-Cornax, Ajay Krishna, Adrian Mos, and Gwen Salaün. "Automated Analysis of Industrial Workflow-based Models". Proceedings of the 33rd Annual ACM Symposium on Applied Computing (SAC 2018), Pau, France, pages 120-127, ACM, April 2018.
Available on-line at:
or from the CADP Web site in PDF or PostScript

Gwen Salaün
Inria Grenoble - Rhône-Alpes / CONVECS
655 Avenue de l'Europe
38330 Montbonnot Saint-Martin
Email: Gwen.Salaun at

Further remarks: This tool, amongst others, is described on the CADP Web site:

Last modified: Sat Jun 12 22:02:11 2021.

Back to the CADP research tools page