Formal Modeling and Verification of Software Models
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.
[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)
[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)
@article{"International Journal of Information, Control and Computer Sciences:63255", author = "Siamak Rasulzadeh", title = "Formal Modeling and Verification of Software Models", 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.", volume = "2", number = "6", pages = "2213-7", }
