There are two types of model checking: explicit state and symbolic model checking. We suggest symbolic analysis as an alternative for focused verification, a novel paradigm with a simulation capability.

Explicit State Model Checking

  • states are enumerated on-the-fly
  • Forwards analysis
  • Stores visited states in a hashtable
Characteristics of explicit state model checking:
  • Memory intensive
  • Good for finding concurrency errors
  • Short execution paths are better, but long execution paths can also be handled
  • Can handle dynamic creation of objects/threads
  • Mostly used in software

Symbolic Model Checking

  • Sets of states are manipulated at a time
  • Typically a backwards analysis
  • Transition relation encoded by (some variant of) Binary Decision Diagrams (BDDs) or as a satisfiability problem
Characteristics of Symbolic Model Checking:
  • Can handle very large state spaces
  • Not as good for asynchronous systems
  • Cannot deal well with long execution traces
  • Works best with a static transition relation, hence doesn’t deal well with dynamic creation of objects/threads
  • Mostly used in hardware
An example about a Kripke graph in Fig.  below (see Kripke Structure, also called as a Kripke model or a Kripke graph).
Kripke_Graph

How symbolic analysis differs from Symbolic and Explicit Model Checking?

Atomistic model and symbolic analysis, presented in this blog do not provide any complete model checking strategy. Instead, symbolic analysis provides a simulation methodology (SimulationWare), which estimates one use scenario of the code at a time. By repeating numerous scenarios it is possible for the user to evaluate alternative paths, but the purpose of it is not automatic proving, complete verification, but proving partial correctness in  co-operation with the tool and the user. The characteristics of symbolic analysis are:

  • Focused approach, not holistic
  • Symbolic execution traces. It is possible to use these outputs for verification purposes.
  • Mostly used for troubleshooting purposes
  • States are modeled using side effect elements (internal state variables)
  • Formwards analysis, but after analysis also backwards analysis is possible
  • Transition relations are code inside symbolic elements (command-field and links between elements).

Some links:

Advertisements