Formal verification of fault-tolerant and recovery mechanisms for safe node sequence protocol

doi:10.1109/AINA.2014.99

IR > 理学院

	Formal verification of fault-tolerant and recovery mechanisms for safe node sequence protocol
	Zhou, Rui 1; Min, Rong 1; Yu, Qi 1; Li, Chanjuan 1; Sheng, Yong 1; Zhou, Qingguo ; Wang, Xuan2 ; Li, Kuan-Ching 3
	2014
会议名称	28th IEEE International Conference on Advanced Information Networking and Applications, IEEE AINA 2014
会议录名称	Proceedings - International Conference on Advanced Information Networking and Applications, AINA
页码	813-820
会议日期	May 13, 2014 - May 16, 2014
会议地点	Victoria, BC, Canada
出版地	345 E 47TH ST, NEW YORK, NY 10017 USA
出版者	Institute of Electrical and Electronics Engineers Inc.
摘要	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. © 2014 IEEE.
关键词	Embedded systems Formal verification Model checking Recovery Safety engineering Event-triggered Fault tolerant systems Protocol state machines Recovery mechanisms Safety critical systems Sequence protocols System robustness Verification results
DOI	10.1109/AINA.2014.99
收录类别	EI
语种	英语
WOS研究方向	Computer Science ; Engineering
WOS类目	Computer Science, Hardware & Architecture ; Engineering, Electrical & Electronic
WOS记录号	WOS:000358605300108
EI入藏号	20142817932201
EI主题词	Fault tolerance
ISSN	1550445X
来源库	Compendex
分类代码	721.1 Computer Theory, Includes Formal Logic, Automata Theory, Switching Theory, Programming Theory - 723.5 Computer Applications - 914 Safety Engineering
引用统计	被引频次：2[WOS] [WOS记录] [WOS相关记录]
文献类型	会议论文
条目标识符	https://ir.lut.edu.cn/handle/2XXMBERH/117843
专题	理学院
通讯作者	Zhou, Qingguo
作者单位	1.Lanzhou Univ, Sch Informat Sci & Engn, Lanzhou 730000, Peoples R China 2.Lanzhou Univ Technol, Sch Sci, Lanzhou 730050, Gansu, Peoples R China 3.Providence Univ, Dept Comp Sci & Informat Engn CSIE, Taichung, Taiwan
推荐引用方式 GB/T 7714	Zhou, Rui,Min, Rong,Yu, Qi,et al. Formal verification of fault-tolerant and recovery mechanisms for safe node sequence protocol[C]. 345 E 47TH ST, NEW YORK, NY 10017 USA:Institute of Electrical and Electronics Engineers Inc.,2014:813-820.