Abstract
Dynamic workflow applications are increasingly used in many enterprises to satisfy the variable enterprise requirements. Cloud computing has gained a particular attention to run these applications. However, due to lack of formal description of the resource perspective, the behavior of Cloud resource allocation cannot be correctly managed. This paper fills this gap by proposing a formal model which verifies the correctness of dynamic workflow changes in a Cloud environment using the Event-B method. Our model considers properties related to control flow, data flow and resource perspectives. It aims to preserve the correctness of workflow properties at both design time and runtime.
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
Notes
- 1.
Business Process Modeling Notation: http://www.bpmn.org/.
- 2.
The transitive closure of a simple oriented graph is the graph obtained by keeping the nodes and adding the arcs (x, y) for which there is a path from x to y in the initial graph.
References
Sadiq, S.W., Orlowska, M.E., Sadiq, W.: Specification and validation of process constraints for flexible workflows. Inf. Syst. 30(5), 349–378 (2005)
Ly, L.T., Rinderle, S., Dadam, P.: Semantic correctness in adaptive process management systems. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 193–208. Springer, Heidelberg (2006). https://doi.org/10.1007/11841760_14
Kumar, A., Yao, W., Chu, C.-H., Li, Z.: Ensuring compliance with semantic constraints in process adaptation with rule-based event processing. In: Dean, M., Hall, J., Rotolo, A., Tabet, S. (eds.) RuleML 2010. LNCS, vol. 6403, pp. 50–65. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16289-3_6
Asadi, M., Mohabbati, B., Grner, G., Gasevic, D.: Development and validation of customized process models. Syst. Softw. 96, 73–92 (2014)
Barron, M.A.Z., Ruiz-Vanoye, J.A., Díaz-Parra, O., Fuentes-Penna, A., Loranca, M.B.B.: A mathematical model for optimizing resources of scientific projects. Computación y Sistemas 20(4) (2016)
Kumar, A., Yao, W., Chu, C.H.: Flexible process compliance with semantic constraints using mixed-integer programming. INFORMS J. Comput. 25(3), 543–559 (2013)
Ahmed, E., Naveed, A., Hamid, S.H.A., Gani, A., Salah, K.: Formal analysis of seamless application execution in mobile cloud computing. Supercomputing 73(10), 4466–4492 (2017)
Boubaker, S., Mammar, A., Graiet, M., Gaaloul, W.: Formal verification of cloud resource allocation in business processes using Event-B. In: Advanced Information Networking and Applications, pp. 746–753. IEEE (2016)
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Rezaee, A., Rahmani, A.M., Movaghar, A., Teshnehlab, M.: Formal process algebraic modeling, verification, and analysis of an abstract fuzzy inference cloud service. Supercomputing 67(2), 345–383 (2014)
Van Dongen, B., Mendling, J., Van Der Aalst, W.: Structural patterns for soundness of business process models. In: Enterprise Distributed Object Computing, pp. 116–128. IEEE (2006)
Weber, B., Reichert, M., Rinderle-Ma, S.: Change patterns and change support features-enhancing flexibility in process-aware information systems. Data Knowl. Eng. 66(3), 438–466 (2008)
Fakhfakh, F., Kacem, H.H., Kacem, A.H., Fakhfakh, F.: Preserving the correctness of dynamic workflows within a cloud environment. In: Knowledge-Based and Intelligent Information & Engineering Systems (2018)
Hollingsworth, D., Hampshire, U.: Workflow management coalition: the workflow reference model. Document Number TC00-1003 19 (1995)
Song, W., Ma, X., Cheung, S.C., Hu, H., Lü, J.: Preserving data flow correctness in process adaptation. In: Services Computing, pp. 9–16. IEEE (2010)
Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)
Boubaker, S., Mammar, A., Graiet, M., Gaaloul, W.: An Event-B based approach for ensuring correct configurable business processes. In: Web Services, pp. 460–467 (2016)
Ly, L.T., Rinderle, S., Dadam, P.: Integration and verification of semantic constraints in adaptive process management systems. Data Knowl. Eng. 64(1), 3–23 (2008)
Hallerbach, A., Bauer, T., Reichert, M.: Guaranteeing soundness of configurable process variants in provop. In: Commerce and Enterprise Computing, pp. 98–105. IEEE (2009)
van der Aalst, W.M., Dumas, M., Gottschalk, F., Ter Hofstede, A.H., Rosa, M.L., Mendling, J.: Preserving correctness during business process model configuration. Formal Aspects Comput. 22(3), 459–482 (2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Fakhfakh, F., Kacem, H.H., Kacem, A.H. (2019). Towards a Formal Approach for Verifying Dynamic Workflows in the Cloud. In: Themistocleous, M., Rupino da Cunha, P. (eds) Information Systems. EMCIS 2018. Lecture Notes in Business Information Processing, vol 341. Springer, Cham. https://doi.org/10.1007/978-3-030-11395-7_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-11395-7_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-11394-0
Online ISBN: 978-3-030-11395-7
eBook Packages: Computer ScienceComputer Science (R0)