Specification and Verification of a Multi-agent Coordination Protocol with TLA+
Pedro Yuri Arbs Paiva, Osamu Saotome, Christof Brandauer · 2018
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.