Excellence in Research and Innovation for Humanity

International Science Index

Select areas to restrict search in scientific publication database:
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.
Digital Article Identifier (DAI):


[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)
Vol:12 No:10 2018Vol:12 No:09 2018Vol:12 No:08 2018Vol:12 No:07 2018Vol:12 No:06 2018Vol:12 No:05 2018Vol:12 No:04 2018Vol:12 No:03 2018Vol:12 No:02 2018Vol:12 No:01 2018
Vol:11 No:12 2017Vol:11 No:11 2017Vol:11 No:10 2017Vol:11 No:09 2017Vol:11 No:08 2017Vol:11 No:07 2017Vol:11 No:06 2017Vol:11 No:05 2017Vol:11 No:04 2017Vol:11 No:03 2017Vol:11 No:02 2017Vol:11 No:01 2017
Vol:10 No:12 2016Vol:10 No:11 2016Vol:10 No:10 2016Vol:10 No:09 2016Vol:10 No:08 2016Vol:10 No:07 2016Vol:10 No:06 2016Vol:10 No:05 2016Vol:10 No:04 2016Vol:10 No:03 2016Vol:10 No:02 2016Vol:10 No:01 2016
Vol:9 No:12 2015Vol:9 No:11 2015Vol:9 No:10 2015Vol:9 No:09 2015Vol:9 No:08 2015Vol:9 No:07 2015Vol:9 No:06 2015Vol:9 No:05 2015Vol:9 No:04 2015Vol:9 No:03 2015Vol:9 No:02 2015Vol:9 No:01 2015
Vol:8 No:12 2014Vol:8 No:11 2014Vol:8 No:10 2014Vol:8 No:09 2014Vol:8 No:08 2014Vol:8 No:07 2014Vol:8 No:06 2014Vol:8 No:05 2014Vol:8 No:04 2014Vol:8 No:03 2014Vol:8 No:02 2014Vol:8 No:01 2014
Vol:7 No:12 2013Vol:7 No:11 2013Vol:7 No:10 2013Vol:7 No:09 2013Vol:7 No:08 2013Vol:7 No:07 2013Vol:7 No:06 2013Vol:7 No:05 2013Vol:7 No:04 2013Vol:7 No:03 2013Vol:7 No:02 2013Vol:7 No:01 2013
Vol:6 No:12 2012Vol:6 No:11 2012Vol:6 No:10 2012Vol:6 No:09 2012Vol:6 No:08 2012Vol:6 No:07 2012Vol:6 No:06 2012Vol:6 No:05 2012Vol:6 No:04 2012Vol:6 No:03 2012Vol:6 No:02 2012Vol:6 No:01 2012
Vol:5 No:12 2011Vol:5 No:11 2011Vol:5 No:10 2011Vol:5 No:09 2011Vol:5 No:08 2011Vol:5 No:07 2011Vol:5 No:06 2011Vol:5 No:05 2011Vol:5 No:04 2011Vol:5 No:03 2011Vol:5 No:02 2011Vol:5 No:01 2011
Vol:4 No:12 2010Vol:4 No:11 2010Vol:4 No:10 2010Vol:4 No:09 2010Vol:4 No:08 2010Vol:4 No:07 2010Vol:4 No:06 2010Vol:4 No:05 2010Vol:4 No:04 2010Vol:4 No:03 2010Vol:4 No:02 2010Vol:4 No:01 2010
Vol:3 No:12 2009Vol:3 No:11 2009Vol:3 No:10 2009Vol:3 No:09 2009Vol:3 No:08 2009Vol:3 No:07 2009Vol:3 No:06 2009Vol:3 No:05 2009Vol:3 No:04 2009Vol:3 No:03 2009Vol:3 No:02 2009Vol:3 No:01 2009
Vol:2 No:12 2008Vol:2 No:11 2008Vol:2 No:10 2008Vol:2 No:09 2008Vol:2 No:08 2008Vol:2 No:07 2008Vol:2 No:06 2008Vol:2 No:05 2008Vol:2 No:04 2008Vol:2 No:03 2008Vol:2 No:02 2008Vol:2 No:01 2008
Vol:1 No:12 2007Vol:1 No:11 2007Vol:1 No:10 2007Vol:1 No:09 2007Vol:1 No:08 2007Vol:1 No:07 2007Vol:1 No:06 2007Vol:1 No:05 2007Vol:1 No:04 2007Vol:1 No:03 2007Vol:1 No:02 2007Vol:1 No:01 2007