Formalizing and validating UML architecture description of web systems

ABSTRACT

Web systems are self-descriptive software components which can automatically be discovered and engaged, together with other web components, to complete tasks over the Internet. Unified Modeling Language (UML), a widely accepted object-oriented system modeling and design language, and adapted for software architecture descriptions for several years, has been used for the web system description recently. However, it is hard to detect the system problems, such as correctness, consistency etc., of the integration of Web services without a formal semantics of web services architecture. In this paper, we proposed an approach to solving this issue by translating the UML web service architecture description into a formal modeling language - SO-SAM, and verify the correctness of the web system design using model checking techniques. We presented this approach through an imaging processing scenario in the distributed web application.

REFERENCES

• 1: Business Process Execution Language for Web Services (BPEL4WS). http://www.ibm.com/developerworks/library/ws-bpel.
• 2: DAML-S and OWL-S. http://www.daml.org/services/owl-s/.
• 3: Simple Object Access Protocol (SOAP), W3C Note 08. http://www.w3.org/TR/SOAP/.
• 4: Unified modeling language (uml), version 2.0. http://www.omg.org/technology/documents/formal/uml.htm.
• 5: Web Service Choreography Interface (WSCI) 1.0. http://www.w3.org/TR/2002/NOTE-wsci-20020808/.
• 6: Web Services Description Language (WSDL) 1.1. http://www.w3.org/TR/wsdl.
• 7: Haresh S. Bhatt , V. H. Patel , Akshai K. Aggarwal, Web Enabled Client-Server Model for Development Environment of Distributed Image Processing, Proceedings of the First IEEE/ACM International Workshop on Grid Computing, p.135-145, December 17, 2000
• 8: S.-W. Cheng and D. Garlan. Mapping Architectural Concepts to UML-RT. In 2001 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'2001), June 2001.
• 9: M. Clavel, F. J. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. F. Quesada. Maude: Specification and Programming in Rewriting Logic. http://maude.csl.sri.com/papers, March 1999.
• 10: Z. Dong, Y. Fu, and X. He. Deriving Hierarchical Predicate/Transition Nets from Statechart Diagrams. In Proceedings of the The 15th International Conference on Software Engineering and Knowledge Engineering (SEKE2005), 2003.
• 11: A. Egyed. Automating Architectural View Integration in UML. Technical Report USCCSE-99511, Center for Software Engineering, University of Southern California, Los Angeles, CA, 1999.
• 12: A. Egyed and N. Medvidovic. Extending Architectural Representation in UML with View Integration. In Proceedings of the 2nd International Conference on the Unified Modeling Language, pages 2--16, October 1999.
• 13: Hartmut Ehrig , B. Mahr, Fundamentals of Algebraic Specification I, Springer-Verlag New York, Inc., Secaucus, NJ, 1985
• 14: H. Ehrig , Bernd Mahr, Fundamentals of algebraic specification 2: module specifications and constraints, Springer-Verlag New York, Inc., New York, NY, 1990
• 15: Hartmut Ehrig , Julia Padberg , Leila Ribeiro, Algebraic High-Level Nets: Petri Nets Revisited, Selected papers from the 9th Workshop on Specification of Abstract Data Types Joint with the 4th COMPASS Workshop on Recent Trends in Data Type Specification, p.188-206, October 26-30, 1992
• 16: Yujian Fu , Zhijiang Dong , Xudong He, An approach to web services oriented modeling and validation, Proceedings of the 2006 international workshop on Service-oriented software engineering, May 27-28, 2006, Shanghai, China [doi>10.1145/1138486.1138504]
• 17: Yujian Fu , Zhijiang Dong , Xudong He, Modeling, validating and automating composition of web services, Proceedings of the 6th international conference on Web engineering, July 11-14, 2006, Palo Alto, California, USA [doi>10.1145/1145581.1145626]
• 18: David Garlan , Shang-Wen Cheng , Andrew J. Kompanek, Reconciling the needs of architectural description with object-modeling notations, Science of Computer Programming, v.44 n.1, p.23-49, July 2002 [doi>10.1016/S0167-6423(02)00031-X]
• 19: X. He and Y. Deng. A Framework for Specifying and Verifying Software Architecture Specifications in SAM. volume 45 of The Computer Journal, pages 111--128, 2002.
• 20: Xudong He , Huiqun Yu , Tianjun Shi , Junhua Ding , Yi Deng, Formally analyzing software architectural specifications using SAM, Journal of Systems and Software, v.71 n.1-2, p.11-29, April 2004 [doi>10.1016/S0164-1212(02)00087-0]
• 21: R. Heckel, M. Lohmann, and S. Thöne. Towards a UML Profile for Service-Oriented Architectures. citeseer.csail.mit.edu/heckel03towards.html.
• 22: R. Heckel, H. Voigt, J. Küster, and S. Thöne. Towards Consistency of Web Service Architectures. http://www.upb.de/cs/agengels/Papers/2003/HeckelVoigtKuesterThoene-SCI03.pdf.
• 23: Christine Hofmeister , Robert Nord , Dilip Soni, Applied software architecture, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 24: Christine Hofmeister , Robert L. Nord , Dilip Soni, Describing Software Architecture with UML, Proceedings of the TC2 First Working IFIP Conference on Software Architecture (WICSA1), p.145-160, February 22-24, 1999
• 25: Richard Hull , Michael Benedikt , Vassilis Christophides , Jianwen Su, E-services: a look behind the curtain, Proceedings of the twenty-second ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, p.1-14, June 09-11, 2003, San Diego, California [doi>10.1145/773153.773154]
• 26: Diego Latella , Istvan Majzik , Mieke Massink, Towards a Formal Operational Semantics of UML Statechart Diagrams, Proceedings of the IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), p.465, February 15-18, 1999
• 27: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 28: N. Medvidovic, A. Egyed, and D. S. Rosenblum. Round-Trip Software Engineering Using UML: From Architecture to Design and Back. In Proceedings of the 2nd Workshop on Object-Oriented Reengineering, pages 1--8, September 1999.
• 29: Nenad Medvidovic , Richard N. Taylor, A Classification and Comparison Framework for Software Architecture Description Languages, IEEE Transactions on Software Engineering, v.26 n.1, p.70-93, January 2000 [doi>10.1109/32.825767]
• 30: Paul Clements , David Garlan , Len Bass , Judith Stafford , Robert Nord , James Ivers , Reed Little, Documenting Software Architectures: Views and Beyond, Pearson Education, 2002
• 31: J. Saldhana, S. M. Shatz, and Z. Hu. Formalization of Object Behavior and Interactions From UML Models. International Journal of Software Engineering and Knowledge Engineering, pages 643--673, 2001.
• 32: Mary Shaw , David Garlan, Software architecture: perspectives on an emerging discipline, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 33: J. Wang, X. He, and Y. Deng. Introducing Software Architecture Specification and Analysis in SAM through an Example. Information and Software Technology, 41(7):451--467, 1999.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.0 General

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Languages (e.g., description, interconnection, definition)
      D.2.4 Software/Program Verification

Keywords:
UML architecture description, petri nets, software architecture model, temporal logic, verification and validation