I know that Symbolic Model Checking is state space traversal based on representations of states sets and transition relations as formulas like in CTL using models like Kripke Model. I know the theory. But I'm finding it hard to understand the actual application. Where exactly is it used? What exactly does it do and how does it work?
Can someone explain with a real example and relate theory to practice?
Symbolic Model Checking is Model Checking that works on symbolic states. That is, they encode the states into symbolic representations, typically Ordered Binary Decision Diagrams (OBDDs).
The question is what do they do and how do they work.
You first have your source code for some application. You then transform your source code into some state-transition graph like a Kripke Structure. The states are filled with atomic propositions which describe what is true in that particular state. In Symbolic Model Checking the atomic propositions are encoded as OBDDs to save on space and improve performance.
The Model Checker then starts at some initial state, and explores the states, looking for errors in the state-transition graph. If it finds an error it will often generate a test case demonstrating the error. It uses the symbolic OBDDs to somewhat optimally navigate the state space. Wish I could explain more there but still learning.
But that's basically it. You have a program converted into a formal model (state-transition graph), and then you use symbolic optimizations to navigate the state space to look for errors (by comparing it against an LTL/CTL specification). And if an error is found, the Model Checker gives you some stuff to help document and solve it.
Symbolic model checking can be very useful for verifying the correctness of communications and security protocols. For example:
This works by writing a symbolic description of all the primitive functions and protocol algorithms, and then having a symbolic model checker, such as ProVerif, traverse the state space and attempt to detect state combinations that produce unfavorable results. In the case of ProVerif, symbolic models are described using the applied Pi calculus as the modeling language. This allows the description of protocols in a functional, ML-like syntax.
