{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T15:51:17Z","timestamp":1743090677947,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030994280"},{"type":"electronic","value":"9783030994297"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/978-3-030-99429-7_9","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"155-162","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SMC4PEP: Stochastic Model Checking of Product Engineering Processes"],"prefix":"10.1007","author":[{"given":"Hassan","family":"Hage","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emmanouil","family":"Seferis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vahid","family":"Hashemi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Mantwill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Daclin, N., Vallespir, B., Vincent, C.: Enabling model checking for collaborative process analysis: from bpmn to \u2018network of timed automata\u2019. In: Enterprise Inforation Systems. vol.\u00a09, pp. 279\u2013299. Taylor and Francis (2015)","DOI":"10.1080\/17517575.2013.879211"},{"key":"9_CR2","unstructured":"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"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Duran, F., Rocha, C., Sala\u00fcn, G.: Stochastic analysis of bpmn with time in rewriting logic. In: Science of Computer Programming. pp. 168, pp. 1\u201317. Elsevier (2018)","DOI":"10.1016\/j.scico.2018.08.007"},{"key":"9_CR4","unstructured":"Europe, S.S.C.: Enterprise Architect 15.2 [Software] (2021), https:\/\/www.sparxsystems.de"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.3139\/9783446439467.012"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Gebler, D., Hashemi, V., Turrini, A.: Computing behavioral relations for probabilistic concurrent systems. In: ROCKS 2012. pp. 117\u2013155. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)","DOI":"10.1007\/978-3-662-45489-3_5"},{"key":"9_CR7","unstructured":"Group, O.O.M.: Business process model and notation (bpmn). Website (2014), https:\/\/www.omg.org\/spec\/BPMN"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"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.\u00a01269, pp. 527\u2013541. Springer (2020)","DOI":"10.1007\/978-3-030-59155-7_38"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Hashemi, V., Hermanns, H., Turrini, A.: Exploiting robust optimization for interval probabilistic bisimulation. In: Agha, G., Van\u00a0Houdt, B. (eds.) Quantitative Evaluation of Systems. pp. 55\u201371. Springer International Publishing, Cham (2016)","DOI":"10.1007\/978-3-319-43425-4_4"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: Param: A model checker for parametric markov models. In: CAV. pp. 660\u2013664 (2010)","DOI":"10.1007\/978-3-642-14295-6_56"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"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\u2013317. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_22"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"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\u2013598. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"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\u2013126. Springer (2016)","DOI":"10.1007\/978-3-319-30000-9_9"},{"key":"9_CR14","unstructured":"Hebert, L.: Specification, verification and optimisation of business process. Technical University of Denmark (2014)"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"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\u201366. Springer Berlin Heidelberg, Berlin, Heidelberg (2002)","DOI":"10.1007\/3-540-46002-0_5"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Lam, V.S.W.: Formal analysis of BPMN models: a nusmv-based approach. Int. J. Softw. Eng. Knowl. Eng. 20(7), 987\u20131023 (2010), https:\/\/doi.org\/10.1142\/S0218194010005079","DOI":"10.1142\/S0218194010005079"},{"key":"9_CR17","unstructured":"Martin\u00a0Glinz, S.F.: Software quality selected chapter, chapter 7, process quality. University of Z\u00fcrich, Institut for Informatics (2007)"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Mendoza\u00a0Morales, L.: Business process verification: The application of model checking and timed automata. CLEI Electronic Journal 17, \u00a03\u20133 (08 2014)","DOI":"10.19153\/cleiej.17.2.2"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Ou-Yang, C., Lin, Y.D.: BPMN-based business process model feasibility analysis: a Petri net approach. vol.\u00a046, pp. 3763\u20133781. Taylor and Francis (2008), https:\/\/doi.org\/10.1080\/00207540701199677","DOI":"10.1080\/00207540701199677"},{"key":"9_CR20","unstructured":"Parker, D.: Lecture 14 model checking for MDPs. University of Oxford, Department Science (2011)"},{"key":"9_CR21","unstructured":"SIG, V.Q.W.G...A.: Automotive SPICE Process Assessment\/Reference Model. Automotive SPICE (2017)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99429-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:17:05Z","timestamp":1648498625000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99429-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030994280","9783030994297"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99429-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"61","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}