Model checking the composition of hypermedia design components

ABSTRACT

Component-based software development aims at building software system by assembling software components to reduce cost, risk and time-to-market. However, conflicts among components constitute a crucial barrier to successful software composition. In this paper, we present an approach to analyze the properties of components and their compositions in order to detect and correct composition errors. We also demonstrate how model checking can be used to verify properties about the composition of design components. Furthermore, using a hypermedia case study, we show how to represent, instantiate, and integrate design components, and how to find composition errors by applying model checking techniques.

REFERENCES

• 1: Paulo S. C. Alencar , Donald D. Cowan , Jing Dong , Carlos José Pereira de Lucena, A Pattern-Based Approach to Structural Design Composition, 23rd International Computer Software and Applications Conference, p.160-165, October 19-26, 1999
• 2: Paulo S. C. Alencar , Donald D. Cowan , Carlos José Pereira de Lucena, A Formal Approach to Architectural Design Patterns, Proceedings of the Third International Symposium of Formal Methods Europe on Industrial Benefit and Advances in Formal Methods, p.576-594, March 18-22, 1996
• 3: J. M. Atlee , J. Gannon, State-Based Model Checking of Event-Driven System Requirements, IEEE Transactions on Software Engineering, v.19 n.1, p.24-40, January 1993 [doi>10.1109/32.210305]
• 4: Geoff Barrett, Model Checking in Practice: The T9000 Virtual Channel Processor, IEEE Transactions on Software Engineering, v.21 n.2, p.69-78, February 1995 [doi>10.1109/32.345823]
• 5: {5} Samik Basu, Scott A. Smolka, and Orson R. Ward. Model Checking the Java Meta-Locking Algorithm. Proceedings of the 7th Annual IEEE International Conference and Workshop on Engineering of Computer Based Systems (ECBS), pages 342-350, April 2000.
• 6: Don Batory , Bart J. Geraci, Validating Component Compositions in Software System Generators, Proceedings of the 4th International Conference on Software Reuse, p.72, April 23-26, 1996
• 7: M C Browne , E M Clarke , D L Dill , B Mishra, Automatic verification of sequential circuits using temporal logic, IEEE Transactions on Computers, v.35 n.12, p.1035-1044, Dec. 1986 [doi>10.1109/TC.1986.1676711]
• 8: {8} Donald D. Cowan. Personal Homepage. http://csg.uwaterloo.ca/~dcowan.
• 9: {9} Darren Dalcher. Disaster in London: The LAS Case Study. Proceedings of the 6th Annual IEEE International Conference and Workshop on Engineering of Computer Based Systems (ECBS), pages 41-52, April 1999.
• 10: {10} Jing Dong. A Transformational Process-Based Approach to Object-Oriented Design. Master's Thesis, Computer Science Department, University of Waterloo, 1997.
• 11: {11} Jing Dong, Paulo Alencar, and Donald Cowan. Ensuring Structure and Behavior Correctness in Design Composition. Proceedings of the 7th Annual IEEE International Conference and Workshop on Engineering of Computer Based Systems(ECBS), Edinburgh UK, pages 279-287, April 2000.
• 12: {12} E. Emerson and E.M. Clarke. Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Science of Computer Programming, 2:241-266, 1982.
• 13: Martin S. Feather, Rapid Application of Lightweight Formal Methods for Consistency Analyses, IEEE Transactions on Software Engineering, v.24 n.11, p.949-959, November 1998 [doi>10.1109/32.730544]
• 14: B. Fraser , J. Roberts , G. Pianosi , P. Alencar , D. Cowan , D. German , L. Nova, Dynamic views of SGML tagged documents, Proceedings of the 17th annual international conference on Computer documentation, p.93-98, September 12-14, 1999, New Orleans, Louisiana, United States [doi>10.1145/318372.318564]
• 15: Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 16: David Garlan , Robert Allen , John Ockerbloom, Architectural mismatch or why it's hard to build systems out of existing parts, Proceedings of the 17th international conference on Software engineering, p.179-185, April 24-28, 1995, Seattle, Washington, United States [doi>10.1145/225014.225031]
• 17: D. M. Germán , D. D. Cowan, Towards a Unified Catalog of Hypermedia Design Patterns, Proceedings of the 33rd Hawaii International Conference on System Sciences-Volume 6, p.6067, January 04-07, 2000
• 18: Scott A. Hissam, Experience Report: Correcting System Failure in a COTS Information System, Proceedings of the International Conference on Software Maintenance, p.170, March 16-19, 1998
• 19: Jean-Marc Jézéquel , Bertrand Meyer, Design by Contract: The Lessons of Ariane, Computer, v.30 n.1, p.129-130, January 1997 [doi>10.1109/2.562936]
• 20: Rudolf K. Keller , Reinhard Schauer, Design components: toward software composition at the design level, Proceedings of the 20th international conference on Software engineering, p.302-311, April 19-25, 1998, Kyoto, Japan
• 21: {21} D. Kozen. Results on the Propositional µ-calculus. Theoretical Computer Science, 27:333-354, 1983.
• 22: Christian Kramer , Lutz Prechelt, Design Recovery by Automated Search for Structural Design Patterns in Object-Oriented Software, Proceedings of the 3rd Working Conference on Reverse Engineering (WCRE '96), p.208, November 08-10, 1996
• 23: Tommi Mikkonen, Formalizing design patterns, Proceedings of the 20th international conference on Software engineering, p.115-124, April 19-25, 1998, Kyoto, Japan
• 24: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 25: {25} Partha pratim Pal. Law-Governed Support for Realizing Design Patterns. Technology of Object-Oriented Languages and Systems (TOOLS), USA, pages 25-34, July 1995.
• 26: Y. S. Ramakrishna , C. R. Ramakrishnan , I. V. Ramakrishnan , Scott A. Smolka , Terrance Swift , David Scott Warren, Efficient Model Checking Using Tabled Resolution, Proceedings of the 9th International Conference on Computer Aided Verification, p.143-154, June 22-25, 1997
• 27: Dirk Riehle, Composite design patterns, Proceedings of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.218-228, October 05-09, 1997, Atlanta, Georgia, United States
• 28: Gustavo Rossi , Daniel Schwabe , Alejandra Garrido, Design reuse in hypermedia applications development, Proceedings of the eighth ACM conference on Hypertext, p.57-66, April 06-11, 1997, Southampton, United Kingdom [doi>10.1145/267437.267444]
• 29: {29} Colin Stirling. An Introduction to Modal and Temporal Logics for CCS. Lecture Notes in Computer Science 491, Springer-Verlag , pages 1-20, 1991.
• 30: Kevin J. Sullivan , John Socha , Mark Marchukov, Using formal methods to reason about architectural standards, Proceedings of the 19th international conference on Software engineering, p.503-513, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253433]
• 31: Clemens Szyperski, Component software: beyond object-oriented programming, ACM Press/Addison-Wesley Publishing Co., New York, NY, 1998
• 32: Andrew S. Tanenbaum, Computer Networks, Prentice Hall PTR, Upper Saddle River, NJ, 1985
• 33: James C. Widmaier, Producing more reliable software: mature software engineering process vs. state-of-the-art technology?, Proceedings of the 22nd international conference on Software engineering, p.88-93, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337192]
• 34: Jeannette M. Wing , Mandana Vaziri-Farahani, A case study in model checking software systems, Science of Computer Programming, v.28 n.2-3, p.273-299, April 1997 [doi>10.1016/S0167-6423(96)00020-2]
• 35: {35} XSB. The XSB Logic Programming System, Version 2.1. Available from http://www.cs.sunysb.edu/~sbprolog, 1999.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

  H. Information Systems
  H.5 INFORMATION INTERFACES AND PRESENTATION (I.7)
      H.5.4 Hypertext/Hypermedia
          Subjects: Architectures

General Terms:
Algorithms, Design, Experimentation, Measurement, Theory, Verification