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) Mangrove VBPMN Z3
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: https://hal.inria.fr/hal-01781315 or from the CADP Web site in PDF or PostScript
Contact:	Gwen Salaün Inria Grenoble - Rhône-Alpes / CONVECS 655 Avenue de l'Europe 38330 Montbonnot Saint-Martin France Email: Gwen.Salaun at inria.fr
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