Abstract
Much research work has been done on formalizing UML Activity Diagrams for process modeling to verify different kinds of soundness properties (deadlock, unreachable activities and so on) on process models. However, these works focus mainly on the control-flow aspects of the process and have done some assumptions on the precise execution semantics defined in natural language in the UML specification. In this paper, we define a first-order logic formalization of fUML (Foundational Subset of Executable UML), the official and precise operational semantics of UML, in order to apply model checking techniques and therefore verify the correctness of fUML-based process models. Our formalization covers the control-flow, data-flow, resources, and timing dimensions of processes in a unified way. A working implementation based on the Alloy language has been developed. The implementation showed us that many kinds of behavioral properties not commonly supported by other approaches and implying multiple dimensions of the process can be efficiently checked.
Chapter PDF
Similar content being viewed by others
References
Mendling, J.: Empirical studies in process model verification. In: Jensen, K., van der Aalst, W.M.P. (eds.) Transactions on Petri Nets and Other Models of Concurrency II. LNCS, vol. 5460, pp. 208–224. Springer, Heidelberg (2009)
Mendling, J., Verbeek, H., van Dongen, B.F., van der Aalst, W.M., Neumann, G.: Detection and prediction of errors in epcs of the sap reference model. Data & Knowledge Engineering 64(1), 312–329 (2008)
Bendraou, R., Gervais, M.-P., Blanc, X.: UML4SPM: A UML2.0-based metamodel for software process modelling. In: Briand, L.C., Williams, C. (eds.) MoDELS 2005. LNCS, vol. 3713, pp. 17–38. Springer, Heidelberg (2005)
Bendraou, R., Jézéquel, J., Gervais, M., Blanc, X.: A comparison of six uml-based languages for software process modeling. IEEE Transactions on Software Engineering 36(5), 662–675 (2010)
Russell, N., van der Aalst, W.M., Ter Hofstede, A.H., Wohed, P.: On the suitability of uml 2.0 activity diagrams for business process modelling In: Proceedings of the 3rd Asia-Pacific Conference on Conceptual Modelling, vol. 53
van Der Aalst, W.M., Ter Hofstede, A.H., Kiepuszewski, B., Barros, A.P.: Workflow patterns. Distributed and Parallel Databases 14(1), 5–51 (2003)
Dong, Y., ShenSheng, Z.: Using π-calculus to formalize uml activity diagram for business process modeling. In: ECBS, pp. 47–54. IEEE (2003)
Eshuis, R.: Symbolic model checking of uml activity diagrams. TOSEM (2006)
Guelfi, N., Mammar, A.: A formal semantics of timed activity diagrams and its promela translation. In: APSEC. IEEE (2005)
OMG: Uml version 2.4.1 (2011), http://www.omg.org/spec/UML/
OMG: Fuml version 1.1 (2013), http://www.omg.org/spec/FUML/
van der Aalst, W., Van Hee, K., ter Hofstede, A., Sidorova, N., Verbeek, H., Voorhoeve, M., Wynn, M.: Soundness of workflow nets: classification, decidability, and analysis. Formal Aspects of Computing 23(3), 333–363 (2011)
Jackson, D.: Software Abstractions: logic, language and analysis. MIT Press (2011)
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE (1977)
Trčka, N., van der Aalst, W.M.P., Sidorova, N.: Data-flow anti-patterns: Discovering data-flow errors in workflows. In: van Eck, P., Gordijn, J., Wieringa, R. (eds.) CAiSE 2009. LNCS, vol. 5565, pp. 425–439. Springer, Heidelberg (2009)
Jung, H.T., Joo, S.H.: Transformation of an activity model into a colored petri net model. In: TISC, pp. 32–37. IEEE (2010)
Motogna, S., Cr Ciun, F., Lazar, I.: Pârv: Formal definition of fuml in k-framework. Studia Universitatis Babes-Bolyai, Informatica 58(3) (2013)
Abdelhalim, I., Sharp, J., Schneider, S., Treharne, H.: Formal verification of tokeneer behaviours modelled in fUML using CSP. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 371–387. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Laurent, Y., Bendraou, R., Baarir, S., Gervais, MP. (2014). Formalization of fUML: An Application to Process Verification. In: Jarke, M., et al. Advanced Information Systems Engineering. CAiSE 2014. Lecture Notes in Computer Science, vol 8484. Springer, Cham. https://doi.org/10.1007/978-3-319-07881-6_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-07881-6_24
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07880-9
Online ISBN: 978-3-319-07881-6
eBook Packages: Computer ScienceComputer Science (R0)