ABSTRACT
This chapter show a case study based on a distributed multi-master election protocol that has been deployed in industry for real-time communication. The main purpose of multi-master election protocol is to elect the highest-priority master connected to the segment at the moment, make it the new active master, and allow it to operate on the bus until the next election round. The chapter also shows how formal verification through model checking can be used to verify industrial real-time communication protocols. It demonstrates how model checking can be used to identify low-probability issues which may never occur in practice and how counterexamples found by the Spin model checker can be helpful to correct them. The chapter describes that model checking can be profitably used to identify low-probability issues which involves complex interleaving among multiple nodes in a concurrent system. It describes how to handle the concept of time and how to model a multi-drop, inherently broadcast physical channel.
