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).
Formal verification, Page 1 of 2
< Previous page Next page > /docserver/preview/fulltext/books/he/pbhe012e/PBHE012E_ch11-1.gif /docserver/preview/fulltext/books/he/pbhe012e/PBHE012E_ch11-2.gif