Quality Assurance for BPMN Models
Business Process modelling has acquired increasing relevance in software development. Available notations, such as BPMN, permit to describe the flow of activities of complex organisations, when they are pursuing specific objectives. On the one hand, this shortens the communication gap between domain experts and IT specialists. On the other hand, this permits to clarify the characteristics of software systems introduced to provide automatic support for such activities. Nonetheless the lack of a formal semantics hinders the adoption of the standard by software engineers, as it leaves room for ambiguity and it limits the possibility to precisely check the satisfaction of relevant behavioural properties. In both cases with a negative impact on the quality of the resulting software. The lecture will introduce a verification framework for BPMN, called BProVe, that is based on a structured operational semantics definition, implemented using the executable formal framework MAUDE. The specification has been devised to clarify the semantics of the language, and to make the model verification possible and effective. With the intention to effectively support BPMN model verification, also on those scenario suffering from the state-space explosion problem, BProVe integrates both standard model checking techniques, through the MAUDE’s LTL model checker, and statistical model checking techniques, through the statistical analyzer MultiVeSta. To support the adoption of the framework a complete toolchain that allows for rigorous modelling and verification of business processes has been developed. In the lecture practical examples will be used, and successively a set of exercises will be proposed to students that will have the opportunity to use the proposed tool chain.
Lecture at NEMO2019
Date/Time: Wednesday, July 24, 2019 at 16:30