used the BDD-based model checker
NuSMV5 to analyze models with over
10120 reachable states.
More recent model checkers, such
as SAL11 and Prover Plug-In, 9 use
sat-isfiability modulo theories (SMT) solv-ers for reasoning about infinite state
models containing real numbers and
unbounded arrays. These checkers
use a form of induction over the state
transition relation to automatically
prove that a property holds over all
executable paths in a model. While
these tools can handle a larger class of
models, the properties to be checked
must be written to support inductive
proof.
the translator framework
As part of NASA’s Aviation Safety Program (AvSP), Rockwell Collins and the
University of Minnesota developed
a product family of translators that
bridge the gaps between some of the
most popular commercial modeling
languages and several model checkers
and theorem provers. 8 An overview of
this framework is shown in Figure 1.
These translators work primarily with the Lustre formal specification
language, 3 but this is hidden from the
users. The starting point for translation is a design model in MATLAB Sim-ulink/Stateflow or Esterel Technologies SCADE Suite/Safe State Machines.
SCADE Suite produces Lustre models
directly. Simulink or Stateflow models
can be imported using SCADE Suite or
the Reactis10 tool and a translator developed by Rockwell Collins. To ensure
each Simulink or Stateflow construct
has a well-defined semantics, the translator restricts the models that it will
accept to those that can be translated
unambiguously into Lustre.
Once in Lustre, the specification
is loaded into an abstract syntax tree
(AST) and a number of transformation
passes are applied to it. Each transformation pass produces a new Lustre AST
that is syntactically closer to the target
specification language and preserves
the semantics of the original Lustre
specification. This allows all Lustre
type checking and analysis tools to be
used as debugging aids during the development of the translator. When the
AST is sufficiently close to the target
language, a pretty printer is used to
output the target specification.
A model checker
will consider
every possible
combination of
inputs and state,
making the
verification
equivalent to
exhaustive testing
of the model.
if a property is not
true, the model
checker produces
a counterexample
showing how
the property can
be falsified.
We refer to our translator framework
as a product family since most transformation passes are reused in the translators for each target language. Reuse
of the transformation passes makes it
much easier to support new target languages; we have developed new translators in a matter of days. The number
of transformation passes depends on
the similarity of the source and target
languages and on the number of optimizations to be made. Our translators
range in size from a dozen to over 60
passes.
The translators produce highly optimized specifications appropriate for
the target language. For example, when
translating to NuSMV, the translator
eliminates as much redundant internal state as possible, making it very efficient for BDD-based model checking.
When translating to the PVS theorem
prover, the specification is optimized
for readability and to support the development of proofs in PVS. When generating executable C or Ada code, the
code is optimized for execution speed
on the target processor. These optimizations can have a dramatic effect on
the target analysis tools. For example,
optimization passes incorporated into
the NuSMV translator reduced the
time required for NuSMV to check one
model from over 29 hours to less than
a second.
However, some optimizations are
better incorporated into the verification tools rather than the translator.
For example, predicate abstraction1 is
a well-known technique for reducing
the size of the reachable state space,
but automating this during translation
would require a tight interaction between our translator and the analysis
tool to iteratively refine the predicates
counterexample.
step 1
Inputs
Start 0
Clear 0
door Closed 0
Steps to Cook 0
Outputs
Mode
Steps
remaining 0
2
3
1
0
1
1
0
0
0
1
Setup Cooking Cooking
1