symbolic execution and model-checking

Question

What is the difference between symbolic execution and model checking (for example in model transformation)? I don't understand difference of them. Are they the same?!

Answer 1

In model checking, you have to encode your system as a Finite State Machine and provide that FSM to the model checker as well as a specification. The model checker will then make sure that the specification always holds in that system.

In symbolic execution you only provide your program and the symbolic execution engine will examine all the feasible paths to generate test inputs or check assertions.

A simple example of their difference: concurrency. Model checking can handle multi-thread systems because it is specified in the FSM provided as input, however, symbolic execution cannot handle more than one thread.

Answer 2

Model Checking: A method to formally verify that a program satisfies a specification. The specification is usually given in a temporal logic formula like: "if input is x output must be y - holds for all executions (globally) of the program" (see e.g. Edward A Lee).

Symbolic model checking versus explicit state checking: Programs can be finite state machines (FSM). Here explicit state checking is sufficient. But luckily model-checkers exist also for extended FSM's, concurrent, probabilistic, real-time applications. To help prevent state explosion in those systems with very large (infinite) number of states, symbolic model checking is used. In symbolic model checking the states and inputs etc. are treated as symbols and as propositional formulas (or sets of states, set operations etc.). To perform model checking a reachability analysis is needed and to do this the program transitions are executed symbolically. These checkers can't make use of the normal execution of instrumented native code.

Symbolic execution: There exist different methods of encoding during symbolic execution. Some are very specific to model checking and some are modular and used in a stand-alone symbolic execution framework, as it was defined by the inventors of symbolic execution. A symbolic execution framework often uses also some elements (exploration, search) of symbolic model checking to be usable for testing etc.

Finally some examples:

JPF, Java-Pathfinder: Model-checker, explicit state checking, input: java byte code

SPF, Symbolic Pathfinder: Symbolic execution, extension of JPF

JCBMC: Bounded Model Checker, extension of JPF, SPF

XRTs: Exploration and symbolic execution, input: CIL byte code

IntelliTest: Parameterized Unit Tests uses XRTs

Spec Explorer: Model-based Testing uses XRTs