 | 13.3 Writing transition systems and LTL assertions |
| 
| 13 SAL Translator |
| 
| 13.5 Using the tool |
|
| 13.4 Confidence condition verification |
13.4 Confidence condition verification
The tool take an RSL file and it generates three SAL versions. The first
version was described in previous sections, this section talks about the other two versions.
The first version allows one to do the verification under the assumption of
CC satisfaction. But the tool allows one to use the
automatic verification power of model checking to first certify the
satisfaction of CC.
The tool generates therefore other two versions: A "CC" version that checks
confidence conditions and another one "simple CC" that also checks
CC but gives less diagnostic information.
In order to
provide CC verification, basically the translator
does the following:
A deeper embedding of type system is used, all types are “lifted” to
new system types. This new type system includes in all SAL
types a special
datatype, called Not_a_value_type (also it includes
user-defined ones).
The extended type system allows one easily to translate partial functions,
to support explicit subtypes and to verify preconditions with model
checking tools.
A new set of prefix functions must be used in the model. They provide
the basic operations on each type, with the proper extensions to
handle values of type Not_a_value_type (these values are called
navs).
Code is added at the beginning of the function's body (i.e. the SAL
conditional statement IF - THEN - ELSE) in order to verify the
precondition satisfaction.
All functions take values of lifted types as arguments and return
values of lifted types.
If any function's argument is a nav then the nav is returned. A nav is returned if any argument is not in its subtype, or if the precondition is violated, or if the
result of the function is not in its subtype.
In the simple CC version Not_a_value_type is reduced
to the single constant nav. This reduces the sizes of all the lifted types, and hence the size of the model, but
provides less diagnostic information.
A single LTL assertion is generated for each transition system, in
order to check for CC violation. This says that all the local
variables in the transition system are not navs, and if this is not true then
SAL will produce a trace showing how the nav was generated. If a CC check succeeds then no CC
violation occurs in the evolution of the transition system.
Chris George, April 17, 2008
| 13.4 Confidence condition verification |
| 13.3 Writing transition systems and LTL assertions |
| |
| 13 SAL Translator |
| |
| 13.5 Using the tool |
|