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