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 10. Notes on Model Extraction

 

“In all affairs it’s a healthy thing now and then to hang a question mark on the things you have long taken for granted.”

 
 --(Bertrand Russell, 1872–1970)

Arguably, the most powerful tool we have in our arsenal for the verification of software applications is logical abstraction. By capturing the essence of a design in a mathematical model, we can often demonstrate conclusively that the design has certain inevitable properties. The purpose of a verification model, then, is to enable proof. If it fails to do so, within the resource limits that are available to the verification system, the model should be considered inadequate.

The Role of Abstraction

The type of abstraction that is appropriate for a given application ...

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