Formal Verification – Theorem Proving
Theorem proving is
another method for performing verification on formal specifications
of system models. Theorem provers apply rules of inference to a
specification in order to derive new properties of interest. The
theorem proving tools consist of a powerful collection of inference
steps that can be used to reduce a proof goal to simpler sub-goals
that can be discharged automatically by the primitive proof steps of
the prover.
Given a property
and a model, the user is either able to verify the property by
completing the proof or else given back un-dismissed subgoals that
give scenarios in which the property is violated. Theorem proving is
generally harder requiring considerable technical expertise and
understanding of the specification. But it gives the user a lot more
flexibility and control in doing the proofs. This can give the user
greater insights into the specification. One of the major
disadvantages of using theorem provers is that if you fail to
complete the proof of a property, the tool will not tell you whether
the property is indeed unprovable or whether the user is not
providing it with enough information to complete the proof.
One of the
advantages of theorem provers is that they are not limited by the
size of the state space. Large systems that cannot be verified using
the model checker, can still be verified by the theorem prover.
Since state space explosion is not a problem, no abstraction
techniques need to be applied and the verification can be done on
the complete model. Most theorem provers are highly expressive. Some
properties that cannot be easily specified using model checkers
(such as comparing properties of two arbitrary states that are not
temporally related) can be easily specified in the languages of most
theorem provers. These are some of the major advantages of using
theorem provers.
In addition to the translator to the NuSMV
model checker, we have also built a translator, as part of our
verification framework in the Nimbus Toolset, translating
requirements specifications from RSML-e into the
input language of the PVS theorem prover [18
]. This has giving us the capability to perform verification
of translated requirements specifications using both theorem proving
and model checking techniques. We have used theorem proving to
verify safety properties of systems based on models specified in
RSML-e.
We have made extensive use of the theorem prover in an exploratory
type of analysis activity. We have primarily used the PVS theorem
prover to perform “Mode Confusion” analysis of a representative
Flight Guidance System (FGS) model specified in RSML-e.
Mode confusion is a critical safety concern, in which the pilots
believe that the automation is operating in a different mode than it
is actually in. In this type of analysis, we are interesting in
exploring new scenarios that can be sources of potential mode
confusion. In this analysis, we successfully identified a number of
sources of potential mode confusion sources.
|
