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 13. The Timeline Editor

 

A design without requirements cannot be incorrect. It can only be surprising.

 
 --(Willem L. van der Poel, 1926–)

Although SPIN provides direct support for the formalization of correctness requirements in terms of linear temporal logic formulae, the use of this logic is not always as intuitive as one would like. The precise meaning of a temporal logic formula is sometimes counterintuitive, and can confound even the experts.

An alternative method, that we will explore in this chapter, is to express properties visually, with the help of a graphical tool. The tool we discuss here is called the timeline editor, created by Margaret Smith at Bell Labs. The inspiration for this tool came directly from lengthy discussions ...

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