Abstract
Graph transformation has recently become more and more popular as a general visual language to formally state the dynamic semantics of the designed models. Using this technique, we present a highly understandable yet precise approach to formally model the behavioral semantics of UML 2.0 Activity diagrams. Automated formal verification and analysis of UML Activities is the main advantage of our approach. In our proposal, AGG toolset is used to design Activities, then using our previous approach to model checking graph transformation systems, designers can verify and analyze designed Activity diagrams. One of the main application areas of the Activities is workflow modeling; hence to illustrate our approach, we use our proposed semantics for modeling and verification of workflows.
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
Preview
Unable to display preview. Download preview PDF.
References
Eshuis, R., Jansen, D., Andwieringa, R.: Requirements-level Semantics and Model Checking of Object-Oriented Statecharts. Requirements Eng. J. 7, 243–263 (2002)
Alonso, G., Casati, F., Kuno, H., Machiraju, V.: Web Services: Concepts, Architectures and Applications. Springer, Heidelberg (2004)
Object Management Group: UML Specification V2.0. (2005), http://www.omg.org/technology/documents/modelingspeccatalog.htm
Baresi, L., Heckel, R.: Tutorial Introduction to Graph Transformation: A Software Engineering Perspective. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 402–429. Springer, Heidelberg (2002)
Ehrig, H., Engels, G., Kreowski, H.j., Rozenberg, G. (eds.): Handbook on Graph Grammars and Computing by Graph Transformation. Applications, Languages and Tools, vol. 2. World Scientific, Singapore (1999)
Kuske, S.: A Formal Semantics of UML State Machines Based on Structured Graph Transformation. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185. Springer, Heidelberg (2001)
Beyer, M.: AGG1.0 – Tutorial. Technical University of Berlin, Department of Computer Science (1992)
Baresi, L., Rafe, V., Rahmani, A.T., Spoletini, P.: An Efficient Model Checking Approach for Graph Transformation Systems. In: Proc. of 3th International Workshop on Graph Transformation for Verification and Concurrency (GT-VC 2007)
Robby, D.M., Hatcliff, J.: Bogor: An Extensible and Highly-Modular Software Model Checking Framework. In: Proc. of the 9th European software engineering Confference, pp. 267–276 (2003)
Eshuis, R.: Semantics and Verification of UML Activity Diagrams for Workflow Modelling, Ph.D. Thesis, University of Twente, Netherlands (2005)
Bolton, C., Davies, J.: On Giving a Behavioural Semantics to Activity Graphs. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000. LNCS, vol. 1939. Springer, Heidelberg (2000)
Soltenborn, C.: Analysis of UML Workflow Diagrams with Dynamic Meta Modeling Techniques, Master’s Thesis, University of Paderborn, Germany (2006)
Hausmann, J.H.: Dynamic Meta Modeling: A Semantics Description Technique for Visual Modeling Languages, Ph.D. Thesis, University of Paderborn, Germany (2005)
Engels, G., Soltenborn, C., Wehrheim, H.: Analysis UML Activities Using Dynamic Meta Modeling. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 76–90. Springer, Heidelberg (2007)
Rensink, A.: The GROOVE Simulator: A Tool for State Space Generation, In Applications of Graph Transformations with Industrial Relevance (AGTIVE). In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004)
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)
Eshuis, R.: Symbolic Model Checking of UML Activity Diagrams. ACM Transaction on Software Engineering Methodology 15(1), 1–38 (2006)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: A New Symbolic Model Checker. International Journal on Software Tools for Technology Transfer 2(4), 410–425 (2000)
Börger, E., Cavarra, A., Riccobene, E.: An ASM Semantics for UML Activity Diagrams. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 293–308. Springer, Heidelberg (2000)
Baldan, P., Corradini, A., Gadducci, F.: Specifying and Verifying UML Activity Diagrams via Graph Transformation. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 18–33. Springer, Heidelberg (2005)
Schmidt, Á., Varró, D.: CheckVML: A tool for model checking visual modeling languages. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003. LNCS, vol. 2863, pp. 92–95. Springer, Heidelberg (2003)
Störrle, H.: Semantics of Control-Flow in UML 2.0 Activities. In: N.N. (ed.) Proc. IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC) (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rafe, V., Rahmani, A.T. (2008). Formal Analysis of Workflows Using UML 2.0 Activities and Graph Transformation Systems. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds) Theoretical Aspects of Computing - ICTAC 2008. ICTAC 2008. Lecture Notes in Computer Science, vol 5160. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85762-4_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-85762-4_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85761-7
Online ISBN: 978-3-540-85762-4
eBook Packages: Computer ScienceComputer Science (R0)