Visible to the public Formal Verification of Fault-Tolerant and Recovery Mechanisms for Safe Node Sequence Protocol

TitleFormal Verification of Fault-Tolerant and Recovery Mechanisms for Safe Node Sequence Protocol
Publication TypeConference Paper
Year of Publication2014
AuthorsRui Zhou, Rong Min, Qi Yu, Chanjuan Li, Yong Sheng, Qingguo Zhou, Xuan Wang, Kuan-Ching Li
Conference NameAdvanced Information Networking and Applications (AINA), 2014 IEEE 28th International Conference on
Date PublishedMay
Keywordsevent-triggered protocol, failure modes, fault classes, fault model, Fault tolerance, Fault tolerant systems, fault-tolerance, fault-tolerant prototype system, fault-tolerant system, formal verification, machine, model checking, protocol state machine, Protocols, Real-time Systems, recovery mechanisms, Redundancy, safe node sequence protocol, SNSP, Tunneling magnetoresistance

Fault-tolerance has huge impact on embedded safety-critical systems. As technology that assists to the development of such improvement, Safe Node Sequence Protocol (SNSP) is designed to make part of such impact. In this paper, we present a mechanism for fault-tolerance and recovery based on the Safe Node Sequence Protocol (SNSP) to strengthen the system robustness, from which the correctness of a fault-tolerant prototype system is analyzed and verified. In order to verify the correctness of more than thirty failure modes, we have partitioned the complete protocol state machine into several subsystems, followed to the injection of corresponding fault classes into dedicated independent models. Experiments demonstrate that this method effectively reduces the size of overall state space, and verification results indicate that the protocol is able to recover from the fault model in a fault-tolerant system and continue to operate as errors occur.

Citation Key6838748