Colin Blundell
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.
- R. Alur, T. A. Henzinger, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. MOCHA: Modularity in model checking. In International Conference on Computer-Aided Verification, June-July, 1998. Google Scholar
Digital Library
- 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.Google Scholar
- 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.Google ScholarCross Ref
- E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In Symposium on Logic in Computer Science, June 1989. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- L. de Alfaro and T. A. Henzinger. Interface automata. In Symposium on the Foundations of Software Engineering, Sept. 2001. Google ScholarDigital Library
- J. Dingel. Computer assisted assume guarantee reasoning with VeriSoft. In International Conference on Software Engineering May 2003. Google ScholarDigital Library
- C. Flanagan, S. N. Freund, and S. Qadeer. Thread-modular verification for shared-memory programs. In European Symposium on Programming, Apr. 2002. Google ScholarDigital Library
- D. Giannakopoulou, C. S. Pǎsǎreanu, and H. Barringer. Assumption generation for software component verification. In International Conference on Automated Software Engineering, Sept. 2002. Google ScholarDigital Library
- D. Giannakopoulou, C. S. Pǎsǎreanu, and J. M. Cobleigh. Assume-guarantee verification of source code with design-level assumptions. In International Conference on Software Engineering, May 2004. Google ScholarDigital Library
- P. Godefroid. Model checking for programming languages using VeriSoft. In Symposium on Principles of Programming Languages, Jan. 1997. Google ScholarDigital Library
- W. Grieskamp, Y. Gurevich, W. Schulte, and M. Veanes. Generating finite state machines from abstract state machines. In International Symposium on Software Testing and Analysis, July 2002. Google ScholarDigital Library
- O. Grumberg and D. E. Long. Model checking and modular verification. In International Conference on Concurrency Theory, Aug. 1991. Google ScholarDigital Library
- L. J. Jagadeesan, A. A. Porter, C. Puchol, J. C. Ramming, and L. G. Votta. Specification-based testing of reactive software: Tools and experiments (experience report). In International Conference on Software Engineering, May 1997. Google ScholarDigital Library
- C. B. Jones. Specification and design of (parallel) programs. In IFIP World Computer Congress, Sept. 1983.Google Scholar
- 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.Google Scholar
- A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. Apt, editor, Logic and Models of Concurrent Systems, volume 13, New York, 1984. Springer-Verlag. Google ScholarDigital Library
- P. Raymond, X. Nicollin, N. Halbwachs, and D. Weber. Automatic testing of reactive systems. In Real-Time Systems Symposium, Dec. 1998. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- W. Visser, K. Havelund, G. Brat, and S.-J. Park. Model checking programs. In International Conference on Automated Software Engineering, Sept. 2000. Google ScholarDigital Library
- W. Visser, C. S. Pǎsǎreanu, and S. Khurshid. Test input generation with Java PathFinder. In International Symposium on Software Testing and Analysis, July 2004. Google ScholarDigital Library
Index Terms
- Assume-guarantee testing
Recommendations
Assume-guarantee testing
SAVCBS '05: Proceedings of the 2005 conference on Specification and verification of component-based systemsVerification 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. ...
Symbolic assume-guarantee reasoning through BDD learning
ICSE 2014: Proceedings of the 36th International Conference on Software EngineeringBoth symbolic model checking and assume-guarantee reasoning aim to circumvent the state explosion problem. Symbolic model checking explores many states simultaneously and reports numerous erroneous traces. Automated assume-guarantee reasoning, on the ...
Counterexample-Guided Assume-Guarantee Synthesis through Learning
Assume-guarantee reasoning (AGR) is a promising compositional verification technique that can address the state space explosion problem associated with model checking. Since the construction of assumptions usually requires nontrivial human efforts, a ...
Comments