SMC4PEP: Stochastic Model Checking of Product Engineering Processes

TL;DR

SMC4PEP is a tool that converts BPMN-based business process models into Markov Decision Processes for probabilistic model checking, enabling faster verification of complex product engineering processes in industries like automotive and avionics.

Contribution

This paper introduces SMC4PEP, a novel framework that transforms BPMN models into MDPs for efficient probabilistic verification, handling process complexity through event-based abstraction.

Findings

Faster verification routines with smaller MDP models.

Successful application to automotive SPICE compliance.

Enhanced handling of process complexity through event abstraction.

Abstract

Product Engineering Processes (PEPs) are used for describing complex product developments in big enterprises such as automotive and avionics industries. The Business Process Model Notation (BPMN) is a widely used language to encode interactions among several participants in such PEPs. In this paper, we present SMC4PEP as a tool to convert graphical representations of a business process using the BPMN standard to an equivalent discrete-time stochastic control process called Markov Decision Process (MDP). To this aim, we first follow the approach described in an earlier investigation to generate a semantically equivalent business process which is more capable of handling the PEP complexity. In particular, the interaction between different levels of abstraction is realized by events rather than direct message flows. Afterwards, SMC4PEP converts the generated process to an MDP model described by the syntax of the probabilistic model checking tool PRISM. As such, SMC4PEP provides a framework for automatic verification and validation of business processes in particular with respect to requirements from legal standards such as Automotive SPICE. Moreover, our experimental results confirm a faster verification routine due to smaller MDP models generated from the alternative event-based BPMN models.