Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Coverability Analysis Using Symbolic Model Checking

Gil RatzabyContact Information, Shmuel UrContact Information and Yaron WolfsthalContact Information

(6)  IBM Haifa Research Laboratory, Israel
Abstract
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.

Contact Information Gil Ratzaby
Email: rgil@il.ibm.com

Contact Information Shmuel Ur
Email: ur@il.ibm.com

Contact Information Yaron Wolfsthal
Email: wolfstal@il.ibm.com
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.105 • Server: mpweb18
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)