Browse Prior Art Database

Coverability Analysis Using Symbolic Model Checking

IP.com Disclosure Number: IPCOM000122993D
Original Publication Date: 1998-Mar-01
Included in the Prior Art Database: 2005-Apr-04
Document File: 2 page(s) / 97K

Publishing Venue

IBM

Related People

Ur, S: AUTHOR [+2]

Abstract

Disclosed is a new testing concept - coverability analysis - and it is shown how a number of coverability metrics, corresponding to some commonly-used coverage metrics (statement, multi-condition), can be implemented via Symbolic Model Checking (1). The same ideas can be used to implement many other coverability metrics (e.g. define-use, mutation, and loop).

This text was extracted from an ASCII text file.
This is the abbreviated version, containing approximately 52% of the total text.

Coverability Analysis Using Symbolic Model Checking

      Disclosed is a new testing concept - coverability analysis -
and it is shown how a number of coverability metrics, corresponding
to some commonly-used coverage metrics (statement, multi-condition),
can be implemented via Symbolic Model Checking (1).  The same ideas
can be used to implement many other coverability metrics (e.g.
define-use, mutation, and loop).

Given a state-machine model and simulation event, the corresponding
coverage event indicator is a binary function on the set of
simulation test patterns.  This function specifies whether the event
would occur when the state-machine model is simulated against a test
pattern.  A coverage model is a set of event indicators.  The
statement well known coverage model, for example, is a model
containing an event indicator for every statement which indicates if
this statement has been executed in simulation.  The define-use
coverage model is a model containing an indicator for every
combination of a variable definition (e.g. "a = 5") and use (e.g. "if
(a)").  A specific define-use combination is satisfied if there is a
simulation run in which the definition was invoked and no other
definition of the same variable was invoked before the variable was
used.

Every coverage model has a corresponding coverability model.  A
coverability model is defined by creating, for every coverage event
indicator in coverage model, a coverability event indicator which is
binary function on the state-machine model.  The coverability event
indicator is true if there exists a test on the state-machine model
for which the corresponding coverage event indicator is true.

The approach is based on two key observations.  First, as described
above, a coverage model is in fact composed of coverage event
indicators, each of which is mappable to a corresponding coverability
indicator.  The second observation is that a state-machine model can
be instrumented with control variables and related transitions which,
on one hand, retain the original model behavior as reflected on the
original state variables, and, on the other hand, can be used for
coverability analysis of the model.  The analysis is carried out by
formulating special rules on the instrumented model, and presenting
these rules (with the instrumented model) to a Symbolic Model
Checker.

Because our approach exploit Symbolic Model Checking, there is no
need for test generation.  Consider,...