CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Formal Specification and Verification of a Protocol for Consistent Diagnosis in Real-Time Embedded Systems

Raul Barbosa (Institutionen för data- och informationsteknik, Nätverk och system (Chalmers) ) ; Johan Karlsson (Institutionen för data- och informationsteknik, Nätverk och system (Chalmers) )
Proceedings of the 3rd IEEE International Symposium on Industrial Embedded Systems (SIES'2008) p. 216-223. (2008)
[Konferensbidrag, refereegranskat]

This paper proposes a membership protocol for fault-tolerant distributed systems and describes the usage of formal verification methods to ascertain its correctness. The protocol allows nodes in a synchronous system to maintain consensus on the set of operational nodes, i.e., the membership, in the presence of omission failures and node restarts. It relies on nodes observing the transmissions of other nodes to detect failures. Consensus is maintained by exchanging a configurable number of acknowledgements for each node's message. Increasing this number makes the protocol resilient to a greater number of simultaneous or near-coincident failures. We used the SPIN model checker to formally verify the correctness of the membership protocol. This paper describes how we modeled the protocol and presents the results of the exhaustively verified model instances.



Denna post skapades 2008-12-09. Senast ändrad 2016-08-16.
CPL Pubid: 80605

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Nätverk och system (Chalmers)

Ämnesområden

Datorteknik

Chalmers infrastruktur