VBPMN Tool for Checking Business Process Evolution

Organisation:	LIP6, Paris (FRANCE) Inria Grenoble (FRANCE)
Functionality:	Business Processes.
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2016
Description:	Business processes support the modeling and the implementation of software as workflows of local and inter-process activities. Such software can be made executable using process engines or model-to-code translators. Evolution of software should thus also be dealt at the business process level. In this context, formal analysis tools can be useful to compare processes corresponding to different versions of the software, identify precisely the differences between them, and ensure the desired consistency. This work proposes such a tool named VBPMN, which can be used through a Web application. The VBPMN tool works as follows: A model transformation from business processes in the standard BPMN notation to processes in the LNT language allows BPMN processes to be given a formal semantics, which is ultimately defined in terms of LTS (Labelled Transition Systems). This LTS can be computed automatically using the CADP toolbox that supports LNT. Various relations are defined on this LTS for comparing BPMN processes. These relations are implemented using various features available in CADP, such as label renaming, synchronous product, branching equivalence and preorder comparison, and temporal logic verification.
Conclusions:	The use of LNT was preferred over a direct generation from BPMN to an LTS as it yields a simpler, higher-level, and more declarative transformation. Tool support provided by the state-of-the-art and comprehensive verification toolbox CADP was also an important criteria for choosing LNT, as it helped a lot to implement VBPMN. This implementation was made even simpler using the scripting facility provided by the language SVL. Various experiments show that the resulting tool is rather efficient as it can handle huge examples (up to 4.5 million states and 16.5 million transitions) within a reasonable amount of time (less than 10 minutes for the largest example).
Publications:	[Poizat-Salaun-Krishna-16] Pascal Poizat, Gwen Salaün, and Ajay Krishna. "Checking Business Process Evolution". Proceedings of the 13th International Conference on Formal Aspects of Component Software (FACS'16), Besançon, France. Lecture Notes in Computer Science vol. 10231, pages 36-53. Springer, 2017. Available on line at: https://hal.inria.fr/hal-01366641/en and from the CADP Web site in PDF or PostScript [Krishna-Poizat-Salaun-17] Ajay Krishna, Pascal Poizat, and Gwen Salaün. "VBPMN: Automated Verification of BPMN Processes". Proceedings of the 13th International Conference on Integrated Formal Methods (IFM'2017), Torino, Italy. Lecture Notes in Computer Science vol. 10510, pages 323-331. Springer Verlag, September 2017. Available on line at: https://hal.inria.fr/hal-01591665/en and from the CADP Web site in PDF or PostScript [Krishna-Poizat-Salaun-19] Ajay Krishna, Pascal Poizat, and Gwen Salaün. "Checking Business Process Evolution". Science of Computer Programming 170:1-26, 2019. Available on line at: http://hal.inria.fr/hal-01920273/en and from the CADP Web site in PDF or PostScript
Contact:	Pascal Poizat LIP6 Université Pierre et Marie Curie 4 place Jussieu 75252 Paris Cedex 05 FRANCE Email: Pascal.Poizat@lip6.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