Model Checking
System Verification
This specification prescribes what the system has to do and what not, and thus constitutes the basis for any verification activity. A defect is found once the system does not fulfill one of the specification’s properties. The system is considered to be "correct" whenever it satisfies all properties obtained from its specification. So correctness is always relative to a specification, and is not an absolute property of a system.
- A process that asserts the correctness of a computer system (hardware, software or both).
- Software Verification Techniques: Peer reviewing and testing.
- Hardware Verification Techniques:
- Structural Analysis
- Comprises several specific techniques such as synthesis, timing analysis, and equivalence checking.
- Emulation
Can be seem as the hardware-analogous to Software Testing. A reconfigurable generic hardware system (the emulator) is configured such that it behaves like the circuit under consideration and is then extensively tested.
For complex hardware it becomes impractical and the number of tests needs to be reduced significantly, yielding potential undiscovered errors.
- Simulation
- A widely used method that verifies a design model by comparing its output with a golden model (which represents expected behavior). While flexible, simulation is slow and may not cover enough input scenarios in a reasonable time.
Model Checking
Let us first briefly discuss the role of Formal Methods. To put it in a nutshell, formal methods can be considered as "the applied mathematics for modeling and analyzing ICT systems". Their aim is to establish system correctness with mathematical rigor. Their great potential has led to an increasing use by engineers of formal methods for the verification of complex software and hardware systems.
(…)
Model-based verification techniques are based on models describing the possible system behavior in a mathematically precise and unambiguous manner. It turns out that - prior to any form of verification - the accurate modeling of systems often leads to the discovery of incompleteness, ambiguities, and inconsistencies in informal system specifications.
(…)
As the startingpoint of these techniques is a model of the system under consideration, we have as a given fact that: any verification using model-based techniques is only as good as the model of the system.
Characteristics of Model Checking
Model checking is an automated technique that, given a finite-state model of a system and a formal property, systematically checks whether this property holds for (a given state in) that model.
The Model-Checking Process
- Modeling Phase
- Describe the system using the model checker's language (usally a combination of finite-state atomata and temporal logic), perform initial simulations for sanity checks, and formalize the properties to be verified.
- Running Phase
- Execute the model checker to verify whether the specified properties hold in the system model.
- Analysis
- Interpret results, if properties hold, proceed; if something got violated, analyze counterexamples, refine the model or properties, and rerun; if memory issues occur, reduce the model and retry.
Properties
- Safety
- Nothing bad ever happens.
- Liveness
- Good things eventually happen.
- Fairness
- Something happens infinetely often or repeatedly.