Specification and verification of a multi-agent coordination protocol with TLA+

There is a general rule which says that about 50 percent of the elapsed time in a project is expended in testing. Finding bugs in software might be an awkward task, especially when there are design errors. The common sense, however, frequently has a biased view of formal methods, associating it with high complexity and low return on investment. That would supposedly be worth only for critical parts of a system. TLA(+) is a formal specification language that is based on first-order logic and set theory. In this paper, we describe how we used it to formally specify a coordination protocol and how we applied model checking technique to verify correctness properties. We also discuss the advantages of TLA(+) and the relatively low overhead to get used to it.