ABSTRACT
Formal methods should be part of the education of every computer scientist and software engineer, just as the appropriate branch of applied mathematics is a necessary part of the education of all other engineers. A formal design can provide more than verification. It should be possible to generate the requisite software automatically from a validated formal design. The intention of formal design verification is to produce a mathematically complete definition of the design and then prove that the design is correct according to chosen invariants that must remain true irrespective of the sequence of events to which the system is subjected. Spin is a mature tool whose origins can be traced back to the 1980s, and it can be used in simulation and verification modes to debug a design and then prove its correctness. The contexts and machines are then progressively made more concrete by refining algorithms, interactions, and events.
