Verification of Workflow Specifications in UML Using Automated Transformations to WF-nets

• Lígia Maria Soares Passos UFU
• Tarcísio Abadio de Magalhães Júnior UFU
• Marcelo de Almeida Maia UFU
• Stéphane Julia UFU

DOI: https://doi.org/10.5753/sbsi.2013.5731

Resumo

This article proposes the transformation of UML Activity Diagrams that models workflow processes into WF-nets (WorkFlow nets). The transformation is automated using the ATL transformation language, well-known in the model-driven development context. This transformation enables the verification of the soundness property for workflows using linear logic proofs in WF-net specifications. The generated proof trees also help finding possible causes for unsound diagrams. An illustrative case study is presented to demonstrate the approach effectiveness. The results from this paper could motivate the typical software company to introduce the rigor of formal verification using Petri Nets associated with linear logic without sacrificing the common practice of developers who can continue using UML notation integrated with industrial tools such as ATL.

Referências

Atlas Group. ATL: Atlas Transformation Language. http://www.eclipse.org/ m2m/atl/.

Diaz, M. (2009). Petri Nets: Fundamental Models, Verication and Applications. Wiley-IEEE Press.

Dumas, M. and ter Hofstede, A. H. M. (2001). UML activity diagrams as a workow specication language. In Proc. of the 4th Intl. Conf. on The Unied Modeling Language, pages 76–90, London, UK. Springer-Verlag.

Gehrke, T., Goltz, U., and Wehrheim, H. (1998). The dynamic models of UML: Towards a semantics and its application in the development process. Technical report, Institut für Informatik, Universität Hildeshein.

Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science, 50(1):1–102.

Jouault, F., Allilaire, F., Bézivin, J., and Kurtev, I. (2008). ATL: A model transformation tool. Science Compututer Programming, 72(1-2):31–39.

Leymann, F. and Roller, D. (1997). Workow-based applications. IBM Systems Journal, 36(1):102–123.

Meena, H. K., Saha, I., Mondal, K. K., and Prabhakar, T. V. (2005). An approach to workow modeling and analysis. In Eclipse’05: Proceedings of the 2005 OOPSLA Workshop on Eclipse technology eXchange, pages 85–89, New York, NY, USA. ACM.

Murata, T. (1989). Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–580.

OMG (2008). OMG Unied Modeling Language Specication – Version 2.2. Object Management Group. http://www.omg.org/spec/UML/2.2/ Superstructure.

Passos, L. M. S. and Julia, S. (2009). Qualitative analysis of workow nets using linear logic: soundness verication. In Proceedings of the 2009 IEEE international conference on Systems, Man and Cybernetics, SMC’09, pages 2843–2847, Piscataway, NJ, USA. IEEE Press.

Petri, C. A. (1962). Kommunikation mit Automaten. PhD thesis, Institut für instrumentelle Mathematik, Bonn.

Riviere, N., Valette, R., Pradin-Chezalviel, B., and Ups, I. A. . (2001). Reachability and temporal conicts in t-time Petri nets. In PNPM ’01: Proc. of the 9th Intl. Workshop on Petri Nets and Performance Models (PNPM’01), page 229, Washington, DC. IEEE.

Soares Passos, L. M. and Julia, S. (2009). Análise qualitativa e quantitativa de workow nets utilizando lógica linear. In SBSI 2009: Proceedings of the V Simpósio Brasileiro de Sistemas de Informação. SBC.

Störrle, H. and Hausmann, J. H. (2005). Towards a formal semantics of UML 2.0 activities. In Liggesmeyer, P., Pohl, K., and Goedicke, M., editors, Software Engineering, volume 64 of LNI, pages 117–128. GI.

Trickovié, I. (2000). Formalizing activity diagram of UML by Petri nets. Novi Sad Journal of Mathematics, 30(3):161–171.

van der Aalst, W. M. P. (1998). The application of Petri nets to Workow Management. In The Journal of Circuits, Systems and Computers, pages 21–66.

van der Aalst, W. M. P. and van Hee, K. (2004). Workow Management: Models, Methods, and Systems. The MIT Press.

van der Aalst, W. M. P., van Hee, K. M., ter Hofstede, A. H. M., Sidorova, N., Verbeek, H. M. W., Voorhoeve, M., and Wynn, M. T. (2011). Soundness of workow nets: classication, decidability, and analysis. Form. Asp. Comput., 23:333–363.