Formal Verification – Model Checking
Model Checking,
one of many formal verification methods, is an attractive and
increasingly appealing alternative to simulation and testing to
validate and verify systems. Given a system model and desired
system properties, the Model Checker explores the full state space
of the system model to check whether the given system properties are
satisfied by the model. The Model Checker either verifies the given
properties or generates counter examples.
While simulation
and testing explore some of the possible behaviors of the systems,
model checking conducts an exhaustive exploration of all possible
behaviors. Thus, when the model checker verifies a given system
property, it implies that all behaviors have been explored, and the
question of adequate coverage or a missed behavior become
irrelevant.
There are two main
advantages of using model checking compared to other formal
verification methods; (1) it is fully automatic, and (2) it provides
a counter example whenever the system fails to satisfy a given
property.
We use model checking technique to verify safety properties of
systems based on models specified in RSML-e. We
have built a translator, as part of the Nimbus Toolset, translating
requirements specifications from RSML-e into the
input language of the NuSMV model checker. This has giving us
the capability to perform automatic “one stop” verification of
translated requirements specifications. We have successfully
verified over 300 safety properties on a representative Flight
Guidance System (FGS) model automatically.
In the process,
proper use of abstraction techniques plays an important role as the
use of model checking techniques are hindered by the state-space
explosion problem, where the size of the representation of the
behavior of a system grows exponentially with the size of the
systems. Often, software systems have infinite state spaces,
including real and integer input variables and timing constraints,
and thus, model checking software systems without abstraction is
almost always impossible.
We are developed theoretically sound “domain abstraction”
techniques for model checking software systems, in particular
software systems with numeric constraints. The abstraction process
is automatic and incorporated with the translation process. Several
iterations of abstractions may be required, and the verification
result will be fed back to the Nimbus simulator by invoking a
back-conversion process, which converts the counter examples in
abstracted form into the original form in RSML-e. |
