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 14. A Verification Model of a Telephone Switch

 

“For when the actual facts show a thing to be impossible we are instantly convinced that it is so.”

 
 --(Polybius, The Histories, Book XII)

When faced with a software verification problem, it is often tempting to build a model that is as close to reality as possible. If an implementation exists, the temptation is to duplicate its functionality as faithfully as possible within the language of the model checker used. If only a design exists, the attempt can be to build a trial implementation for verification purposes. The purpose of this chapter is to show that this is not the best approach. The proper management of computational complexity is a key issue in all but the simplest applications ...

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