Approaches

Knowledge Source

Strength

Limitation

Explicit-state Model Checking

State graph or state transition system

Detect errors in highly concurrent design

State explosion problem.

Symbolic Model Checking (Boolean Encoding for State Machine and Set of States)

Ordered Binary Decision Diagram (OBDD) + Fix-point characterization of temporal operators

1) It can handle systems with large state spaces more efficiently.

2) It can verify properties that are specified in rich formal languages, such as temporal logic or mu-calculus spaces more efficiently.

3) It can verify systems that have unbounded data domains, such as integer and real variables.

4) It can verify parameterized systems, where the number of components or processes in the system is not fixed.

Many functions do not have a succinct BDD representation.

Model Checking with Abstraction

Predicate abstraction

Ability to balance the trade-off between accuracy and efficiency in formal verification.

1) Risk of losing important information or details that are necessary for detecting certain types of errors or properties.

2) Difficulty of ensuring the soundness and completeness of the verification results.

Bounded Model Checking

Formal language such as temporal logic or automata, and the design or implementation of the system being verified

1) Effectively handle systems with a large number of states and transitions.

2) Detect errors and violations quickly, without having to explore the entire state space of the system.

1) Cannot detect errors or violations that occur beyond the bound.

2) If the model does not accurately capture the behavior of the system, BMC may produce false negatives or false positives, which can lead to incorrect verification results.

3) State explosion problem.

Dynamic Model Checking

Program code and its associated documentation, such as requirements and design specifications

1) It can handle systems with dynamic or continuous behavior, such as control systems, analog circuits, and hybrid systems.

2) It detects errors and violations in real-time during system execution.

1) It only verifies the behavior of the system during execution.

2) It requires a set of inputs that exercise the system’s behavior adequately.

3) It suffers from the state explosion problem.