Sunday, 24 December 2017

Verification of Invariant Properties by Bounded Model Checking

Bounded model-checking is a technique applied in handling of large state space problems.
The basic principle of bounded model-checking is that  we do not handle the state space all at once. The checking is performed by  restricting the length of the paths.
Partial verification can then be carried out within a given bound that consists of path of a definite length. The length of the paths can then be iteratively increased to accommodate more areas in the state space.

Diameter of the State Space can be defined a the length of the longest loop-free path. Therefore a checking a bound that is equal to the diameter of the state space would result in a complete check.

Approach and Goals
The approach to bounded model checking problem is to map the problem to an appropriate SAT problem.
A model checking problem consists of a model and a property.

Model: Paths of bounded length are mapped onto boolean formula based on a characteristic function which takes into consideration the initial state and the State transition.
Property: Invariant properties are mapped to Boolean formula as a characteristic function of that formula for all possible states

The Boolean formula would evaluate to either true or false such that:
If the SAT solver does not find a substitution in the formula, then the property holds true
But if the SAT solver finds a substitution for the formula, then the substitution induces counterexample for that property.

How to Describe a Path of Bounded Length
Beginning from the initial states: choose a characteristic function, say L(s) where s is the state
Transit along potential transitions: s0 > s1 > s2 > s0 >....
The characteristic function is Cr(s0, s1) for path between s0 and s1

How to Describe the Property
Another characteristic function p(s)

Summary of Bounded Model Checking
  • Bounded Model checking is applied in checking invariant properties
  • It is very efficient in loop-free paths
  • If there is a counterexample up to a certain bound, it could be found
  • Handling Large State Space
  • SAT solver: this is a symbolic technique that uses Boolean formulas
  • For up to a given length of paths, only a partial result is obtained
  • Can be used for test-case generation
  • Tools that can be used:
  • Symbolic Analysis Laboratory(SAL)
  • SAL sal-alg used for automatic test generating
  • CBMC: bounded model checker for C source code