Assume-guarantee testing

ABSTRACT

Verification techniques for component-based systems should ideally be able to predict properties of the assembled system through analysis of individual components before assembly. This work introduces such a modular technique in the context of testing. Assume-guarantee testing relies on the (automated) decomposition of key system-level requirements into local component requirements at design time. Developers can verify the local requirements by checking components in isolation; failed checks may indicate violations of system requirements, while valid traces from different components compose via the assume-guarantee proof rule to potentially provide system coverage. These local requirements also form the foundation of a technique for efficient predictive testing of assembled systems: given a correct system run, this technique can predict violations by alternative system runs without constructing those runs. We discuss the application of our approach to testing a multi-threaded NASA application, where we treat threads as components.

REFERENCES

• 1: Rajeev Alur , Thomas A. Henzinger , Freddy Y. C. Mang , Shaz Qadeer , Sriram K. Rajamani , Serdar Tasiran, MOCHA: Modularity in Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.521-525, June 28-July 02, 1998
• 2: H. Barringer, D. Giannakopoulou, and C. S. Pǎsǎreanu. Proof rules for automated compositional verification through learning. In International Workshop on Specification and Verification of Component-Based Systems, Sept. 2003.
• 3: H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Rule-based runtime verification. In International Conference on Verification, Model Checking and Abstract Interpretation, Jan. 2004.
• 4: E. Clarke , D. Long , K. McMillan, Compositional model checking, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.353-362, June 1989, Pacific Grove, California, United States
• 5: J. M. Cobleigh, D. Giannakopoulou, and C. S. Pǎsǎreanu. Learning assumptions for compositional verification. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr. 2003.
• 6: Luca de Alfaro , Thomas A. Henzinger, Interface automata, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 7: Juergen Dingel, Computer-assisted assume/guarantee reasoning with VeriSoft, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 8: Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Thread-Modular Verification for Shared-Memory Programs, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.262-277, April 08-12, 2002
• 9: Dimitra Giannakopoulou , Corina S. Psreanu , Howard Barringer, Assumption Generation for Software Component Verification, Proceedings of the 17th IEEE international conference on Automated software engineering, p.3, September 23-27, 2002
• 10: Dimitra Giannakopoulou , Corina S. Pasareanu , Jamieson M. Cobleigh, Assume-Guarantee Verification of Source Code with Design-Level Assumptions, Proceedings of the 26th International Conference on Software Engineering, p.211-220, May 23-28, 2004
• 11: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 12: Wolfgang Grieskamp , Yuri Gurevich , Wolfram Schulte , Margus Veanes, Generating finite state machines from abstract state machines, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 13: Orna Grumberg , David E. Long, Model Checking and Modular Verification, Proceedings of the 2nd International Conference on Concurrency Theory, p.250-265, August 26-29, 1991
• 14: Lalita Jategaonkar Jagadeesan , Adam Porter , Carlos Puchol , J. Christopher Ramming , Lawrence G. Votta, Specification-based testing of reactive software: tools and experiments: experience report, Proceedings of the 19th international conference on Software engineering, p.525-535, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253435]
• 15: C. B. Jones. Specification and design of (parallel) programs. In IFIP World Computer Congress, Sept. 1983.
• 16: J. Levy, H. Saidi, and T. E. Uribe. Combining monitors for run-time system verification. Electronic Notes in Theoretical Computer Science, 70(4), Dec. 2002.
• 17: A. Pnueli, In transition from global to modular temporal reasoning about programs, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 18: P. Raymond , X. Nicollin , N. Halbwachs , D. Weber, Automatic Testing of Reactive Systems, Proceedings of the IEEE Real-Time Systems Symposium, p.200, December 02-04, 1998
• 19: K. Sen, G. Rosu, and G. Agha. Detecting errors in multithreaded programs by generalized predictive analysis of executions. In Conference on Formal Methods for Open Object-Based Distributed Systems, 2005.
• 20: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 21: Willem Visser , Corina S. Pǎsǎreanu , Sarfraz Khurshid, Test input generation with java PathFinder, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
      D.2.5 Testing and Debugging
      D.2.9 Management
          Subjects: Software quality assurance (SQA)

General Terms:
Verification

Keywords:
assume-guarantee reasoning, predictive analysis, testing, verification