Debugging Paxos in the UML Multiverse

In this paper, we present experience feedback on the use of animation and debugging tools to build, improve, and verify a UML model of the Paxos consensus algorithm. The need for consensus appears in our IoT industrial context, where we need to switch between several service providers for message passing, depending on their availability and quality of service. However, Paxos is notoriously difficult to understand, and as we plan to expand on the original idea to adapt it to our needs, we have to make sure that the base model is correct as well as fully understood by the developers. To this end, we developed an AnimUML model of Paxos, making it interactive and thus easier to work with. During its construction, we tried to understand how to verify that our requirements are met. By replicating existing scenarios step by step, we found that our model was incomplete. To validate how further model modifications changed this, we wanted to write breakpoints to reach these specific situations, but we found that configuration-based breakpoints were not sufficient in this regard. This led us to leverage the possibilities offered by a temporal multiverse debugger, allowing the creation of temporal breakpoints breaking on scenarios described by different languages of temporal logic. With these tools, we can not only correct the model faster, but also prove that some scenarios are possible or not, allowing for a first step in the model formal verification while keeping it accessible to non-experts of the domain.