Evaluating and improving the automatic analysis of implicit invocation systems

ABSTRACT

Model checking and other finite-state analysis techniques have been very successful when used with hardware systems and less successful with software systems. It is especially difficult to analyze software systems developed with the implicit invocation architectural style because the loose coupling of their components increases the size of the finite state model. In this paper we provide insight into the larger problem of how to make model checking a better analysis and verification tool for software systems. Specifically, we will extend an existing approach to model checking implicit invocation to allow for the modeling of larger and more realistic systems. Our focus will be on improving the representation of events, event delivery policies and event-method bindings. We also evaluate our technique on two non-trivial examples. In one of our examples, we will show how with iterative analysis a system parameter can be chosen to meet the appropriate system requirements.

REFERENCES

• 1: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 2: D. Garlan , S. Jha , D. Notkin , J. Dingel, Reasoning about implicit invocation, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.209-221, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 3: J. Dingel, D. Garlan, S. Jha, and D. Notkin. Towards a formal treatment of implicit invocation using rely/guarantee reasoning. Formal Aspects of Computing, 10:193--213, 1998.
• 4: David Garlan , Serge Khersonsky, Model Checking Implicit-Invocation Systems, Proceedings of the 10th International Workshop on Software Specification and Design, p.23, November 05-07, 2000
• 5: D. Garlan, S. Khersonsky, and J. S. Kim. Model checking publish-subscribe systems. In Proc. of the 10th Int'l SPIN Workshop on Model Checking of Software, May 2003.
• 6: G. J. Holzmann , M. H. Smith, An Automated Verification Method for Distributed Systems Software Based on Model Extraction, IEEE Transactions on Software Engineering, v.28 n.4, p.364-377, April 2002 [doi>10.1109/TSE.2002.995426]
• 7: K. L. McMillan. The SMV Language. Cadence Berkeley Labs, Mar. 1999.
• 8: Peyman Oreizy , Nenad Medvidovic , Richard N. Taylor, Architecture-based runtime software evolution, Proceedings of the 20th international conference on Software engineering, p.177-186, April 19-25, 1998, Kyoto, Japan
• 9: Sylvia Stuurman , Jan van Katwijk, On-line change mechanisms: the software architectural level, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.80-86, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 10: Kevin J. Sullivan , David Notkin, Reconciling environment integration and software evolution, ACM Transactions on Software Engineering and Methodology (TOSEM), v.1 n.3, p.229-268, July 1992 [doi>10.1145/131736.131744]
• 11: Roy Want , Andy Hopper , Veronica Falcão , Jonathan Gibbons, The active badge location system, ACM Transactions on Information Systems (TOIS), v.10 n.1, p.91-102, Jan. 1992 [doi>10.1145/128756.128759]
• 12: Michel Wermelinger , José Luiz Fiadeiro, Algebraic software architecture reconfiguration, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.393-409, September 06-10, 1999, Toulouse, France

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Verification

Keywords:
XML, architectural styles, formal methods, implicit invocation, linear temporal logic, model checking, publish subscribe