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 ...
Get Spin Model Checker, The: Primer and Reference Manual now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
