Specification and verification of a multi-agent coordination protocol with TLA+ - Paiva, Pedro Yuri Arbs; Saotome, Osamu; Brandauer, Christof (Anais do Simpósio Brasileiro de Engenharia de Sistemas Computacionais (SBESC); 2018: Anais do VIII Simpósio Brasileiro de Engenharia de Sistemas Computacionais, 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.