Formal verification of a distributed master election protocol

Although the basic Modbus protocol is based on the master-slave communication paradigm with a single master, along the years it has been extended in various ways, in order to provide additional features such as, for instance, the coexistence of multiple masters on the same TIA/EIA-485 fieldbus segment. The design of a master election protocol in this environment is seemingly straightforward and the designer may believe that its correctness can be assessed satisfactorily by intuition and testing. However, in this paper is it shown how formal verification can help to identify and fix subtle and low-probability issues, which seldom occur in practice, and therefore, may be extremely difficult to detect during pre-production testing.