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 SMC4PEPl 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, SMC4PEPl converts the generated process to an MDP model described by the syntax of the probabilistic model checking tool PRISM. As such, SMC4PEPl 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.
Chapter PDF
Similar content being viewed by others
Keywords
References
Daclin, N., Vallespir, B., Vincent, C.: Enabling model checking for collaborative process analysis: from bpmn to ‘network of timed automata’. In: Enterprise Inforation Systems. vol. 9, pp. 279–299. Taylor and Francis (2015)
Dehnert, C., Junges, S., Katoen, J., Volk, M.: The probabilistic model checker storm (extended abstract). CoRR abs/1610.08713 (2016), http://arxiv.org/abs/1610.08713
Duran, F., Rocha, C., Salaün, G.: Stochastic analysis of bpmn with time in rewriting logic. In: Science of Computer Programming. pp. 168, pp. 1–17. Elsevier (2018)
Europe, S.S.C.: Enterprise Architect 15.2 [Software] (2021), https://www.sparxsystems.de
Gausemeier, J., Dumitrescu, R., Steffen, D., Czaja, A., Wiederkehr, O., Tschirner, C.: Systems engineering in der industriellen praxis. Heinz Nixdorf Institut, Frauenhofer Institut, UNITY AG (2013)
Gebler, D., Hashemi, V., Turrini, A.: Computing behavioral relations for probabilistic concurrent systems. In: ROCKS 2012. pp. 117–155. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)
Group, O.O.M.: Business process model and notation (bpmn). Website (2014), https://www.omg.org/spec/BPMN
Hage, H., Hashemi, V., Mantwill, F.: Towards a systems engineering based automotive product engineering process. In: Software Architecture - 14th European Conference. Communications in Computer and Information Science, vol. 1269, pp. 527–541. Springer (2020)
Hahn, E.M., Hashemi, V., Hermanns, H., Turrini, A.: Exploiting robust optimization for interval probabilistic bisimulation. In: Agha, G., Van Houdt, B. (eds.) Quantitative Evaluation of Systems. pp. 55–71. Springer International Publishing, Cham (2016)
Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: Param: A model checker for parametric markov models. In: CAV. pp. 660–664 (2010)
Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscas m c: a web-based probabilistic model checker. In: International Symposium on Formal Methods. pp. 312–317. Springer (2014)
Hartmanns, A., Hermanns, H.: The modest toolset: An integrated environment for quantitative modelling and verification. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 593–598. Springer (2014)
Hashemi, V., Hermanns, H., Song, L., Subramani, K., Turrini, A., Wojciechowski, P.: Compositional bisimulation minimization for interval markov decision processes. In: Language and Automata Theory and Applications. pp. 114–126. Springer (2016)
Hebert, L.: Specification, verification and optimisation of business process. Technical University of Denmark (2014)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with prism: A hybrid approach. In: Katoen, J.P., Stevens, P. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 52–66. Springer Berlin Heidelberg, Berlin, Heidelberg (2002)
Lam, V.S.W.: Formal analysis of BPMN models: a nusmv-based approach. Int. J. Softw. Eng. Knowl. Eng. 20(7), 987–1023 (2010), https://doi.org/10.1142/S0218194010005079
Martin Glinz, S.F.: Software quality selected chapter, chapter 7, process quality. University of Zürich, Institut for Informatics (2007)
Mendoza Morales, L.: Business process verification: The application of model checking and timed automata. CLEI Electronic Journal 17,  3–3 (08 2014)
Ou-Yang, C., Lin, Y.D.: BPMN-based business process model feasibility analysis: a Petri net approach. vol. 46, pp. 3763–3781. Taylor and Francis (2008), https://doi.org/10.1080/00207540701199677
Parker, D.: Lecture 14 model checking for MDPs. University of Oxford, Department Science (2011)
SIG, V.Q.W.G...A.: Automotive SPICE Process Assessment/Reference Model. Automotive SPICE (2017)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Hage, H., Seferis, E., Hashemi, V., Mantwill, F. (2022). SMC4PEP: Stochastic Model Checking of Product Engineering Processes. In: Johnsen, E.B., Wimmer, M. (eds) Fundamental Approaches to Software Engineering. FASE 2022. Lecture Notes in Computer Science, vol 13241. Springer, Cham. https://doi.org/10.1007/978-3-030-99429-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-99429-7_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99428-0
Online ISBN: 978-3-030-99429-7
eBook Packages: Computer ScienceComputer Science (R0)