Formal verification is another way to check several quality characteristics of a system. The aim is to explore all the possible states of the system to check for properties of interest such as safety (nothing bad will happen), liveness (something good will happen), and fairness (independent subsystems make progress), or common design flaws such as deadlock (the system should not reach a state in which no further action is possible), and livelock/starvation (when a subsystem is prevented from taking any action because of resource contention).

Chapter Contents:

• 11.1 Introduction and background
• 11.2 Formal specification
• 11.2.1 Ambient calculus and ambient logic
• 11.2.2 Linear temporal logic
• 11.3 Model checking
• 11.4 Static and dynamic (formal) verification
• 11.5 Summary

Inspec keywords: software quality; formal verification

Other keywords: formal verification; system quality characteristics; design flaws

Subjects: Software engineering techniques; Formal methods