Abstract
In today’s industries, similar process models are typically reused in different application contexts. These models result in a number of process model variants sharing several commonalities and exhibiting some variations. Configurable process models came to represent and group these variants in a generic manner. These processes are configured according to a specific context through configurable elements. Considering the large number of possible variants as well as the potentially complex configurable process, the configuration may be a tedious task and errors may lead to serious behavioral issues. Since achieving configuration in a correct manner has become of paramount importance, the analysts undoubtedly need assistance and guidance in configuring process variants. In this work, we propose a formal behavioral model based on the Symbolic Observation Graph (SOG) allowing to find the set of deadlock-free configuration choices while avoiding the well-known state-space explosion problem and considering loops and OR-join semantics. These choices are used to support business analysts in deriving deadlock-free variants.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
BPMN 2.0 specification http://www.omg.org/spec/BPMN/2.0/.
- 2.
Note that our approach does not rely on specific Petri nets properties but can be applied to any formal model as soon as states and transition relations are well defined.
- 3.
- 4.
For more details see http://www-inf.it-sudparis.eu/SIMBAD/tools/SOGImplementation.
- 5.
References
van der Aalst, W.M.P., Dreiling, A., Gottschalk, F., Rosemann, M., Jansen-Vullers, M.H.: Configurable process models as a basis for reference modeling. In: Bussler, C.J., Haller, A. (eds.) BPM 2005. LNCS, vol. 3812, pp. 512–518. Springer, Heidelberg (2006). https://doi.org/10.1007/11678564_47
Aalst, W.V.D., et al.: Preserving correctness during business process model configuration. Form. Asp. Comput. 22(3–4), 459–482 (2008)
Aalst, W.V.D., et al.: Soundness of workflow nets: classification, decidability, and analysis. Formal Asp. Comput. 23(3), 333–363 (2011)
Aalst, W.V.D., Lohmann, N., Rosa, M.L.: Ensuring correctness during process configuration via partner synthesis. Inf. Syst. 37(6), 574–592 (2012)
Assy, N.: Automated support of the variability in configurable process models. Ph.D. thesis, University of Paris-Saclay, France (2015)
Assy, N., Gaaloul, W.: Extracting configuration guidance models from business process repositories. In: Motahari-Nezhad, H.R., Recker, J., Weidlich, M. (eds.) BPM 2015. LNCS, vol. 9253, pp. 198–206. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23063-4_14
Boubaker, S., Mammar, A., Graiet, M., Gaaloul, W.: A formal guidance approach for correct process configuration. In: Sheng, Q.Z., Stroulia, E., Tata, S., Bhiri, S. (eds.) ICSOC 2016. LNCS, vol. 9936, pp. 483–498. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46295-0_30
Boubaker, S., Klai, K., Schmitz, K., Graiet, M., Gaaloul, W.: Deadlock-freeness verification of business process configuration using SOG. In: Maximilien, M., Vallecillo, A., Wang, J., Oriol, M. (eds.) ICSOC 2017. LNCS, vol. 10601, pp. 96–112. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-69035-3_7
Dijkman, R., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Softw. Technol. 50(12), 1281–1294 (2008)
Gottschalk, F., Aalst, W.V.D., Jansen-Vullers, M., Rosa, M.L.: Configurable workflow models. Int. J. Coop. Inf. Syst. 17, 177–221 (2008)
Haddad, S., Ilié, J.-M., Klai, K.: Design and evaluation of a symbolic and abstraction-based model checker. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 196–210. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30476-0_19
Hallerbach, A., Bauer, T., Reichert, M.: Guaranteeing soundness of configurable process variants in Provop. In: IEEE Conference on Commerce and Enterprise Computing, CEC, pp. 98–105 (2009)
Hallerbach, A., Bauer, T., Reichert, M.: Capturing variability in business process models: the Provop approach. J. Softw. Maint. 22(6–7), 519–546 (2010)
Klai, K., Tata, S., Desel, J.: Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol. 5701, pp. 294–309. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03848-8_20
Klai, K., Tata, S., Desel, J.: Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes. Data Knowl. Eng. 70(5), 467–482 (2011)
La Rosa, M., et al.: Questionnaire-based variability modeling for system configuration. Softw. Syst. Model. 8(2), 251–274 (2008)
Razavian, M., Khosravi, R.: Modeling variability in business process models using UML. In: Fifth International Conference on Information Technology: New Generations. ITNG 2008, pp. 82–87, April 2008
Rosemann, M., Aalst, W.V.D.: A configurable reference modelling language. Inf. Syst. 32(1), 1–23 (2007)
Verbeek, H., Basten, T., Aalst, W.V.D.: Diagnosing workflow processes using Woflan. Comput. J. 44(4), 246–279 (2001)
Weske, M.: Business Process Management: Concepts, Languages, Architectures. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Boubaker, S., Klai, K., Kortas, H., Gaaloul, W. (2018). A Formal Model for Business Process Configuration Verification Supporting OR-Join Semantics. In: Panetto, H., Debruyne, C., Proper, H., Ardagna, C., Roman, D., Meersman, R. (eds) On the Move to Meaningful Internet Systems. OTM 2018 Conferences. OTM 2018. Lecture Notes in Computer Science(), vol 11229. Springer, Cham. https://doi.org/10.1007/978-3-030-02610-3_35
Download citation
DOI: https://doi.org/10.1007/978-3-030-02610-3_35
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02609-7
Online ISBN: 978-3-030-02610-3
eBook Packages: Computer ScienceComputer Science (R0)