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

Appendix B. The Great Debates

 

“It is not necessary to understand things in order to argue about them.”

 
 --(Pierre Augustin Caron de Beaumarchais, 1732–1799)

Quite a few issues in formal verification have sparked heated debates over the years, without ever coming to a clear resolution. Perhaps the first such issue came up when temporal logic was first being explored, in the late seventies, as a suitable formalism for reasoning about concurrent systems. The issue was whether it was better to use a branching-time or a linear-time logic. Much later, the debate was between symbolic or explicit verification methods. Many of these issues directly relate to design decisions that have to be made in any verifier, including SPIN. We discuss the more important ...

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