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.

Formal Verification of a Distributed Master Election Protocol / Cena, Gianluca; CIBRARIO BERTOLOTTI, Ivan; Hu, Tingting. - STAMPA. - (2012), pp. 245-254. (Intervento presentato al convegno IEEE International Workshop on Factory Communication Systems (WFCS 2012)) [10.1109/WFCS.2012.6242572].

Formal Verification of a Distributed Master Election Protocol

CENA, Gianluca;CIBRARIO BERTOLOTTI, IVAN;HU, TINGTING
2012

Abstract

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/2503324
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo