论文标题
SMC4PEP：产品工程过程的随机模型检查
SMC4PEP: Stochastic Model Checking of Product Engineering Processes
论文作者
论文摘要
产品工程流程（PEP）用于描述大型企业（例如汽车和航空电子行业）的复杂产品开发。业务流程模型符号（BPMN）是一种广泛使用的语言，用于编码此类PEP中几个参与者之间的交互。在本文中，我们将SMC4PEP作为一种工具，是一种使用BPMN标准将业务流程的图形表示的工具，称为同等的离散时间随机控制过程，称为Markov决策过程（MDP）。为此，我们首先遵循早期调查中描述的方法，以产生语义上等效的业务流程，该过程更有能力处理PEP复杂性。特别是，不同级别的抽象级别之间的相互作用是通过事件而不是直接消息流实现的。之后，SMC4PEP将生成过程转换为概率模型检查工具棱镜的语法描述的MDP模型。因此，SMC4PEP为自动验证和验证业务流程提供了一个框架，尤其是关于法律标准（例如汽车香料）的要求。此外，由于基于替代事件的BPMN模型生成的较小的MDP模型，我们的实验结果证实了更快的验证程序。
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.
