Formal Modeling and Verification of Software Models

Authors: Siamak Rasulzadeh

Abstract:

Graph transformation has recently become more and more popular as a general visual modeling language to formally state the dynamic semantics of the designed models. Especially, it is a very natural formalism for languages which basically are graph (e.g. UML). Using this technique, we present a highly understandable yet precise approach to formally model and analyze the behavioral semantics of UML 2.0 Activity diagrams. In our proposal, AGG is used to design Activities, then using our previous approach to model checking graph transformation systems, designers can verify and analyze designed Activity diagrams by checking the interesting properties as combination of graph rules and LTL (Linear Temporal Logic) formulas on the Activities.

Keywords: UML 2.0 Activity, Verification, Model Checking, Graph Transformation, Dynamic Semantics.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1082635

References:

[1] Eshuis, R., Jansen, D. and Andwieringa, R.: Requirements-level Semantics and Model Checking of Object-Oriented Statecharts. Requirements Eng. J. 7, 243-263, (2002)
[2] Alonso, G., Casati, F., Kuno, H. and Machiraju, V.: Web Services: Concepts, Architectures and Applications. Springer, (2004)
[3] Object Management Group: UML Specification V2.0. http://www.omg.org/ technology/documents/modeling spec catalog.htm (2005)
[4] Baresi, L. and Heckel, R.: Tutorial Introduction to Graph Transformation: A Software Engineering Perspective, In proc. of first International Conference on Graph Transformation (ICGT), vol 2505 of LNCS, 402-429, (2002)
[5] Ehrig, H., Engels, G., Kreowski, H.j. and Rozenberg, G. (eds.): Handbook on Graph Grammars and Computing by Graph Transformation, vol. 2: Applications, Languages and Tools. World Scientific, (1999)
[6] Kuske, S.: A Formal Semantics of UML State Machines Based on Structured Graph Transformation, In Proc. of UML 2001, vol. 2185, Springer-Verlag, (2001)
[7] Beyer, M.: AGG1.0 - Tutorial. Technical University of Berlin, Department of Computer Science, (1992)
[8] Baresi, L., Rafe, V., Rahmani, A.T. and Spoletini, P.: An Efficient solution for Model Checking Graph Transformation Systems. Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 213, PP. 3-21, (2008)
[9] Robby, Dwyer, M. and Hatcliff, J.: Bogor: An Extensible and Highly- Modular Software Model Checking Framework, In Proc. of the 9th European software engineering Conference, 267-276, (2003)
[10] Eshuis, R.: Semantics and Verification of UML Activity Diagrams for Workflow Modelling, Ph.D. Thesis, University of Twente, Netherlands, (2005)
[11] Bolton, C., Davies, J.: On Giving a Behavioural Semantics to Activity Graphs. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000. vol. 1939 of LNCS, Springer, Heidelberg (2000)
[12] Soltenborn, C.: Analysis of UML Workflow Diagrams with Dynamic MetaModeling Techniques, Master-s Thesis, University of Paderborn, Germany,( 2006)
[13] Hausmann, J. H.: Dynamic Meta Modeling: A Semantics Description Technique for Visual Modeling Languages, Ph.D. Thesis, University of Paderborn, Germany, (2005)
[14] Engels, G., Soltenborn, C. and Wehrheim, H.: Analysis UML Activities Using Dynamic Meta Modeling, In Proc. of 9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), vol 4468 of LNCS, 76-90, (2007)
[15] Rensink, A.: The GROOVE Simulator: A Tool for State Space Generation, In Applications of Graph Transformations with Industrial Relevance (AGTIVE), vol. 3062 of Lecture Notes in Computer Science, 479-485, (2004)
[16] Störrle, H., Hausmann, J.H.: Towards a Formal Semantics of UML 2.0 Activities. In: Liggesmeyer, P., Pohl, K., Goedicke, M. (eds) Software Engineering. LNI., GI, vol. 64 pp. 117-128 (2005)
[17] Eshuis, R.: Symbolic Model Checking of UML Activity Diagrams. ACM Transaction on Software Engineering Methodology, 15(1), 1-38 (2006)
[18] Cimatti, A., Clarke, E., Giunchiglia, F. and Roveri, M.: NuSMV: A New Symbolic Model Checker," International Journal on Software Tools for Technology Transfer, 2(4):410-425, (2000)
[19] Börger, E., Cavarra, A., Riccobene, E.: An ASM Semantics for UML Activity Diagrams. In: Rus, T. (ed.) AMAST 2000. vol. 1816 of LNCS, pp. 293-308. Springer, Heidelberg (2000)
[20] Baldan, P., Corradini, A., and Gadducci, F.: Specifying and Verifying UML Activity Diagrams via Graph Transformation. In Proc. of Global Computing, vol. 3267 of LNCS, 18-33, (2004)
[21] Störrle, H.: Semantics of Control-Flow in UML 2.0 Activities, In: N.N., editor, Proc. IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC) (2004)
[22] Bock, C.: UML 2 Activity and Action Models Part 4: Object Nodes, In Journal of Object Technology, vol. 3, no. 1, pp. 27-41. (2004)