Authors : Aliouat Zibouda and Ferhat Abbes
Abstract: Time-Triggered Architecture (TTA) is distributed computer architecture for highly dependable real-time systems. The communication between nodes of this architecture is achieved by a key module that implements a Time-Triggered Communication Protocol (TTC/P). TTP/C integrates a set of fault-tolerant services like : message transmissions, clocks synchronization and Group Membership Protocol (GMP). The complexity and criticity of GMP and its sensitive interaction with other system components has led to the development of many versions. These different versions of GMP included more formalism in its analysis and verification but none of them, in our best knowledge, has dealt with the problem of node reintegration after recovery. We report the first formal modelling of a reintegration for a safety-critical distributed embedded system. A reintegration node increases system survivability by allowing a transiently-faulty node to regain a group. The group membership algorithm is formally specified by a set of guarded commands.
Aliouat Zibouda and Ferhat Abbes , 2006. Formal Modeling and Analysis of A Node Reintegration in The Time-Triggered Architecture. Asian Journal of Information Technology, 5: 706-711.