Abstract
Business Process Modeling Notation (BPMN) has acquired increasing relevance in business process modeling. However, it suffers, as all semi-formal languages, from the lack of rigorous semantic which hinder its full adoption and makes impossible the verification of relevant properties. In this paper, a model-driven approach for the verification of BPMN2.0 models using the Event B method is proposed. When the complexity of the target system increases, the traceability of Event B model elements back to the original BPMN model becomes a tedious task and failures to verify properties can be difficult to understand. For this reason, the proposed approach is adapted to keep trace of the transformation process in the format of a serialized file. It is automated through mapping rules implemented in a first prototype tool called BPMN2EVENTB.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Meghzili S, Chaoui A, Strecker M, Kerkouche E (2020) An approach for the transformation and verification of BPMN models to colored petri nets models. Int J Softw Innov 8:17–49. https://doi.org/10.4018/IJSI.2020010102
Abrial J (2007) The event-B modelling notation
Snook C, Butler M (2001) Using a graphical design tool for formal specification. In: the 13th annual workshop of the psychology of programming interest group, pp 311–321, Bournemouth, UK
Younes AB, Ben Daly Hlaoui Y, Ben Ayed L, Bessifi M (2019) From BPMN2 to event B: A specification and verification approach of workflow applications. In: Proceedings—international computer software and applications conference. https://doi.org/10.1109/COMPSAC.2019.10266
Morimoto S (2008) A survey of formal verification for business process modeling. In: Bubak M, van Albada GD, Dongarra J, Sloot PMA (eds) Computational science—ICCS 2008. Springer, Berlin Heidelberg, Berlin, Heidelberg, pp 514–522
Dijkman RM, Dumas M, Ouyang C (2008) Semantics and analysis of business process models in BPMN. Inf Softw Technol 50:1281–1294. https://doi.org/10.1016/j.infsof.2008.02.006
Kheldoun A, Barkaoui K, Ioualalen M (2017) Formal verification of complex business processes based on high-level Petri nets. Inf Sci (Ny) 385–386:39–54. https://doi.org/10.1016/j.ins.2016.12.044
Ayari S, Ben Dali Hlaoui Y, Ben Ayed L (2018) A new approach for the verification of BPMN models using refinement patterns. In: Proceedings of international computer software and applications conference, vol 1, pp 807–808. https://doi.org/10.1109/COMPSAC.2018.00130
Kossak F, Illibauer C, Geist V, Kubovy J, Natschläger C, Ziebermayr T (2014) A rigorous semantics for BPMN 2.0 process diagrams. Springer
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Bessifi, M., Younes, A.B., Ayed, L.B. (2022). BPMN2EVENTB Supporting Transformation from BPMN2.0 to Event B Using Kermeta. In: Zhang, YD., Senjyu, T., So-In, C., Joshi, A. (eds) Smart Trends in Computing and Communications. Lecture Notes in Networks and Systems, vol 286. Springer, Singapore. https://doi.org/10.1007/978-981-16-4016-2_24
Download citation
DOI: https://doi.org/10.1007/978-981-16-4016-2_24
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-16-4015-5
Online ISBN: 978-981-16-4016-2
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)