Formal Analysis of Fault-tolerant Algorithm in the Time-triggered Architecture
- 1 ,
Copyright: © 2020 Aliouat Zibouda, Aliouat Makhlouf and Batouche Chawki. This is an open access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.
Time-Triggered architecture (TTA) provides a computing infrastructure for the design and implementation of dependable distributed systems. The core building block of the TTA is the communication protocol TTP/C. This protocol has been designed to provide no faulty nodes. TTP/C integrates a set of fault-tolerant services like: message transmissions, clocks synchronization and Group Membership Protocol (GMP). The GMP protocol ensures that each TTA node maintains a private membership set, which records all the nodes that are believed to be nonfaulty. In the GMP protocol previously studied in the literature, any detected faulty node was immediately excluded from the group. This gradual exclusion process risks invalidating the protocol after N-3 successive failures if the ability of faulty node reintegration was not implemented. Our contribution in this paper was to remedy this serious problem. A node reintegration increases system survivability by allowing a (recovering) transiently-faulty node to regain a group. Our proposal algorithm, devoted to node reintegration inside the group membership protocol, was formally specified and verified using a diagrammatic representation. The verification of the proposal has been checked with the well known PVS theorem prover.
- 1,077 Views
- 1,333 Downloads
- 0 Citations
- Time-triggered Architecture
- deductive verification