Spin Model Checker, The: Primer and Reference Manual

Chapter 4. Defining Correctness Claims

	If the odds are a million to one against something occurring, chances are fifty-fifty that it will.
	--(Folklore wisdom)

The goal of system verification is to establish what is possible and what is not. Often, this assessment of what is logically possible will be subject to some set of assumptions about the context in which a system executes, such as the possible behavior of external components that the system will be interacting with. When performing logical verification we are especially interested in determining whether design requirements could possibly be violated, not necessarily in how likely or unlikely such violations might be. Dramatic system failures are almost always the result of seemingly unlikely ...