Coverability Analysis Using Symbolic Model Checking
In simulation based verification of hardware, as well as in software testing, one is faced with the challenge of maximizing coverage of testing while minimizing testing cost. To this end, sophisticated techniques are used to generate clever test cases, and equally sophisticated techniques are employed by engineers to determine the quality - a.k.a. coverage - attained by the tests. The latter activity is called Test Coverage Analysis.
While it is an essential component of the development process, test coverage can only be analyzed late in the design cycle when the tested entity and the test harness are both stable. To address this serious restriction, we introduce the notion of coverability, which intuitively refers to the degree to which a model can be covered when subjected to testing. We also show an implementation of coverability checking using Model Checking. The notion of coverability highlights a distinction between (1) whether a model has been covered by some test suite and (2) whether the model can ever be covered by any test suite. Coverability Analysis can be performed as soon as the hardware or software are written, before the test harness has been written.
KeywordsModel Check Coverability Model Symbolic Model Check Dead Code Test Harness
- [AZ97]Adnan Aziz, Example of Hardware Verification Using VIS, The benchmark PCI local BUS, http://www-cad.eecs.berkeley.edu/Respep/Research/vis/texas-97/.
- [BBEL96]I. Beer, S. Ben-David, C. Eisner, A. Landver, “RuleBase: an Industry-Oriented Formal Verification Tool”, Proc. DAC’96, pp. 655–660.Google Scholar
- [Beizer90]Boris Beizer, Software Testing Technique, 2/e. New York: Van Nostrand Reinhold, 1990.Google Scholar
- [CGP99]E.M. Clarke, O. Grumberg. D.A. Peled. Model Checking, MIT Press, 1999.Google Scholar
- [CFSM]D. Geist, M. Farkas, A. Landver, Y. Licthenstein, S. Ur and Y Wolfsthal, Coverage Directed Test Generation using Symbolic Techniques, FMCAD 96: Int. Conf. On Formal Methods in Computer-Aided Design, November 1996.Google Scholar
- [Hol91]G. J. Holtzman, Design and Validation of Computer Protocols, Prentice Hall, 1991.Google Scholar
- [Kaner95]C. Kaner, Software Negligence & Testing Coverage, Software QA Quarterly, Vol 2,#2, pp 18, 1995.Google Scholar
- [KN96]M. Kantrowitz, L. M. Noack, “I’m Done Simulating; Now What? Verification Coverage Analysis and Correctness Checking of the DECchip 21164 Alpha Microprocessor”, Proc. DAC’96.Google Scholar
- [KPKR94]S. Kajihara, I. Pomerantz, K. Kinoshita and S. M. Reddy, “Cost Effective Generation of Minimal Test Sets for Stack-At Faults in Combinatorial logic Circuits”, 30th ACM/IEEE DAC, pp. 102–106, 1993.Google Scholar
- [LLU96]D. Levin, D. Lorentz and S. Ur, “A Methodology for Processor Implementation Verification”, FMCAD 96: Int. Conf. on Formal Methods in Computer-Aided Design, November 1996.Google Scholar
- [Marick95]B. Marick, The Craft of Software Testing: Subsystem Testing Including Object-Based and Object-Oriented Testing, Prentice-Hall, 1995.Google Scholar
- [McM93]K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.Google Scholar
- [Mil90]Raymond E. Miller, Protocol Verification: The first ten years, the next ten years; some personal observations, in Protocol specification, Testing, and Verification X, 1990.Google Scholar
- [RB]RuleBase User Manual V1.0, IBM Haifa Research Laboratory, 1996.Google Scholar
- [TCE]I. Beer, M. Dvir, B. Kozitsa. Y Lichtenstein, S. Mach, W.J. Nee, E. Rappaport. Q. Schmierer, Y Zandman, VHDL TEST COVERAGE in BDLS/AUSSIM Environment, IBM HRL Technical Report 88.342, December 1993.Google Scholar
- [VHDL93]D. L. Perry, VHDL Second Edition, McGraw-Hill Series on Computer Engineering, 1993.Google Scholar
- [Weyuker94]E. Weyuker, T. Goradia and A. Singh, Automatically Generating Test Data from a Boolean Specification, IEEE Transaction on Software Engineering, Vol 20, No 5 May 1994.Google Scholar