NDLI: On design and formal verification of SNSP: a novel real-time communication protocol for safety-critical applications

Content Provider	Springer Nature Link
Author	Zhou, Rui Li, Chanjuan Min, Rong Yu, Qi Gu, Fei Zhou, Qingguo Hung, Jason C. Li, Kuan Ching Wang, Xuan
Copyright Year	2014
Abstract	The correct operation of time-triggered protocols highly depends on the well-synchronized clocks of the system. To maintain the global time, one strict constraint must be exerted on communication activities (e.g. temporal padding and sparse time base etc.), which not only increases complexity of the protocol design but also incurs a penalty in the network utilization. While for event-triggered protocols, it is difficult to achieve the real-time requirement and determinism. Therefore, it is necessary to explore the combination of the advantages of these two categories of protocol for applications in different scenarios. This paper proposes the Safe Node Sequence Protocol (SNSP), which is a variant of full time-triggered protocol TTP/C. In SNSP, a strict node sequence is defined and the order of communication events is established by this pre-configured order without binding to global time, so the protocol changes communication activities and error detection to an event-triggered model. Therefore, SNSP possesses the characteristics of both time-triggered and event-triggered model. Also, the potential impact of global time, such as byzantine clock failure, on the protocol is eliminated. At the same time, the formal verification of SNSP is much easier in the absence of global time. Moreover, we model the protocol and use formal checker SPIN to validate the basic fault-tolerant requirement of SNSP. The simulation results show the protocol enables better resource utilization and is more effective.
Starting Page	1254
Ending Page	1283
Page Count	30
File Format	PDF
ISSN	09208542
Journal	The Journal of Supercomputing
Volume Number	69
Issue Number	3
e-ISSN	15730484
Language	English
Publisher	Springer US
Publisher Date	2014-03-18
Publisher Place	Boston
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Event-triggered protocol Safe node sequence protocol Safety Fault-tolerance Formal verification Programming Languages, Compilers, Interpreters Processor Architectures Computer Science
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Information Systems Hardware and Architecture Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Application-Level Fault Tolerance as a Complement to System-Level Fault Tolerance

Formal Verification of Fault-Tolerant and Recovery Mechanisms for Safe Node Sequence Protocol

A fault-tolerant architecture for parallel applications in tiled-CMPs

Dynamic camouflage event based malicious node detection architecture

Fault tolerance of hypercubes and folded hypercubes

Parallel reconfiguration algorithms for mesh-connected processor arrays

Embedded Fault-Tolerant Systems

A family of Hamiltonian and Hamiltonian connected graphs with fault tolerance

A fault-tolerant strategy for virtualized HPC clusters

On design and formal verification of SNSP: a novel real-time communication protocol for safety-critical applications

Similar Documents

Application-Level Fault Tolerance as a Complement to System-Level Fault Tolerance

Formal Verification of Fault-Tolerant and Recovery Mechanisms for Safe Node Sequence Protocol

A fault-tolerant architecture for parallel applications in tiled-CMPs

Dynamic camouflage event based malicious node detection architecture

Fault tolerance of hypercubes and folded hypercubes

Parallel reconfiguration algorithms for mesh-connected processor arrays

Embedded Fault-Tolerant Systems

A family of Hamiltonian and Hamiltonian connected graphs with fault tolerance

A fault-tolerant strategy for virtualized HPC clusters

On design and formal verification of SNSP: a novel real-time communication protocol for safety-critical applications