|
abstract |
|
One of the chief adavantages of model checking is
the production of the counterexamples demonstrating
that a system does not satisfy a specification.
However the size and the complexity of the
counterexamples may cause a great deal of human
effort to extract the essence of an error from even
a detail source-level trace of a failing run.
In the talk methods of automizing the process of
finding the key elements of the error. The methods
are based on the identifications of portions of the
source code crucial to distinguishing failing and
succeeding runs, differences in invariants between
failing and nonfailing runs, and information on the
necessary changes in scheduling and environmental
actions needed to cause succesful runs to fail .
|
