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