The FeaVer System
The four main components of the Feature Verification System were:
Model extraction
The conversion of C code into a verification model takes
a fraction of a second and is a virtually invisible part of
the complete verification process on FeaVer.
To setup the extraction capability, the user defines (once)
a simple lookup table that identifies the source code statements
that are relevant to the properties being checked.
The rest of the process is automated.
(More detail.)
Model checking
FeaVer generates code that can be analyzed efficiently
by the Bell Labs model checker
Spin.
The application within FeaVer has lead to
extensions of the Spin system that makes it possible
to support the required level of interactive feedback.
Searches can either be initiated by the user, or can be
autonomously triggered by FeaVer itself when it detects
a change in either the software, or in one or more of its
required properties.
(More detail.)
Hardware support
Multiprocessing hardware made it possible to
execute a series of increasingly precise searches
on 16 computers in parallel, so that
property violations could be reported with unprecedented speed.
(More detail.)
| ||
Back to Main Page | ||
return |