Spin Model Checker, The: Primer and Reference Manual

Chapter 3. An Overview of PROMELA

	“What we see depends on mainly what we look for.”
	--(Sir John Lubbock, 1834–1913)

In the last chapter we saw that the emphasis in PROMELA models is placed on the coordination and synchronization aspects of a distributed system, and not on its computational aspects. There are some good reasons for this choice. First, the design and verification of correct coordination structures for distributed systems software tends to be much harder in practice than the design of a non-interactive sequential computation, such as the computation of compound interest or square roots. Second, the curious situation exists that the logical verification of the interaction in a distributed system, though often computationally expensive, ...