O'Reilly logo

Spin Model Checker, The: Primer and Reference Manual by Gerard J. Holzmann

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required