Abstract
In simulation-based verification users are faced with the challenge of maximizing test coverage while minimizing testing costs. Sophisticated techniques are used to generate clever test cases and to determine the quality attained by the tests. The latter activity, which is essential for locating areas of the design that need to have more tests, is called test coverage analysis.
We have previously introduced the notion of coverability, which refers to the degree to which a model can be covered when subjected to testing. We showed how a coverability analyzer enables naive users to take advantage of the power of symbolic model checking with a ’one-button’ interface for coverability analysis. In this work, we present several heuristics, based on static program analysis and on simulation of counter examples, for improving the efficiency of coverability analysis by symbolic model checking. We explain each heuristic independently and suggest a way to combine them. We present an experiment that shows improvements based on using random simulation in the analysis of coverability.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A.V. Aho, R. Sethi, J.D. Ullman. Compilers: Principles, Techniques and Tools. Addison-Wesley, 1986.
Adnan Aziz. Example of Hardware Verification Using VIS, The benchmark PCI Local BUS, URL http://www-cad.eecs.berkeley.edu/Respep/Research/vis/texas-97/.
I. Beer, S. Ben-David, C. Eisner, A. Landver. RuleBase: an Industry-Oriented Formal Verification Tool. Proc. DAC’96, pp. 655–660.
I. Beer, M. Yoeli, S. Ben-David, D. Geist and R. Gewirtzman. Methodology and System for Practical Formal Verification of Reactive Systems. CAV94, LNCS 818, pp 182–193.
Boris Beizer. Software Testing Technique. New York: Van Nostrand Reinhold, second edition, 1990.
G Ratzaby, S. Ur and Y. Wolfsthal. Coverability Analysis Using Symbolic Model Checking. CHARME2001, September, 2001.
E. Buchink and S. Ur. Compacting Regression Suites On-The-Fly. Joint Asia Pacific Software Engineering Conference and International Computer Science Conference, Hong Kong, December, 1997.
E.M. Clarke, O. Grumberg. D.A. Peled. Model Checking, MIT Press, 1999.
D. Geist, M. Farkas, A. Landver, Y. Lictenstein, S. Ur and Y Wolfsthal. Coverage-directed test generation using symbolic techniques. In Proc. Int. Conf. Formal methods in Computer-Aided Design, pages 143–158, 1996.
Y Abarbanel, I. Beer, L. Gluhovsky, S. Keidar, and Y Wolfsthal. FoCs-Automatic Generation of Simulation Checkers from Formal Specifications. In Proc. 12thInternational Conference on Computer Aided Verification (CAV), 2000.
Y Hoskote, T. Kam, P. Ho and X. Zhao. Coverage Estimation for Symbolic Model Checking. DAC’99, pp300–305, June 1999.
M.R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman, 1979.
G. J. Holtzman. Design and Validation of Computer Protocols. Prentice Hall, 1991.
D.S. Hochbaum. An Optimal Test Compression Procedure for Combinational Circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 15:10, 1294–1299, 1996.
C. Kaner. Software Negligence & Testing Coverage. Software QA Quarterly, Vol 2,#2, pp18, 1995.
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.
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.
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.
B. Marick. The Craft of Software Testing: Subsystem Testing Including Object-Based and Object-Oriented Testing. Prentice-Hall, 1995.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
Raymond E. Miller. Protocol Verification: The first ten years, the next ten years; some personal observations. In Protocol specification, Testing, and Verification X, 1990.
Y.V. Hoskote, D. Moundanos and J.A. Abraham. Automatic Extraction of the Control Flow Machine and Application to Evaluating Coverage of Verification Vectors. IEEE International Conference on Computer Design (ICCD ‘95), October 1995.
A. J. Offutt. Investigation of the software testing coupling effect. ACM Transactions on Software Engineering Methodology, 1(1):3–18, January 1992.
F. Orava. Formal Semantics of SDL Specifications. In Protocol Specification, Testing, and Verification VIII, 1988.
RuleBase User Manual V1.0, IBM Haifa Research Laboratory, 1996.
I. Beer, S. Ben-David, C. Eisner, D. Geist, L. Gluhovsky, T. Heyman, A. Landver, P. Paanah, Y Rodeh, G. Ronin, and Y Wolfsthal. RuleBase: Model Checking at IBM. Proc. 9th International Conference on Computer Aided Verification (CAV), 1997.
I. Beer, S. Ben-David, C. Eisner, D. Fisman, A. Gringauze, and Y Rodeh. The Temporal Logic Sugar. Proc. 13th International Conference on Computer Aided Verification (CAV), 2001.
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.
D. L. Perry. VHDL Second Edition. McGraw-Hill Series on Computer Engineering, 1993.
Telecordia Software Visualization and Analysis Tool. URL http://xsuds.argreenhouse.com/.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ratsaby, G., Sterin, B., Ur, S. (2002). Improvements in Coverability Analysis. In: Eriksson, LH., Lindsay, P.A. (eds) FME 2002:Formal Methods—Getting IT Right. FME 2002. Lecture Notes in Computer Science, vol 2391. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45614-7_3
Download citation
DOI: https://doi.org/10.1007/3-540-45614-7_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43928-8
Online ISBN: 978-3-540-45614-8
eBook Packages: Springer Book Archive