NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Real-Time System Verification by Kappa-InductionWe report the first formal verification of a reintegration protocol for a safety-critical, fault-tolerant, real-time distributed embedded system. A reintegration protocol increases system survivability by allowing a node that has suffered a fault to regain state consistent with the operational nodes. The protocol is verified in the Symbolic Analysis Laboratory (SAL), where bounded model checking and decision procedures are used to verify infinite-state systems by k-induction. The protocol and its environment are modeled as synchronizing timeout automata. Because k-induction is exponential with respect to k, we optimize the formal model to reduce the size of k. Also, the reintegrator's event-triggered behavior is conservatively modeled as time-triggered behavior to further reduce the size of k and to make it invariant to the number of nodes modeled. A corollary is that a clique avoidance property is satisfied.
Document ID
20050170449
Acquisition Source
Langley Research Center
Document Type
Technical Memorandum (TM)
Authors
Pike, Lee S.
(NASA Langley Research Center Hampton, VA, United States)
Date Acquired
September 7, 2013
Publication Date
April 1, 2005
Subject Category
Cybernetics, Artificial Intelligence And Robotics
Report/Patent Number
L-19110
NASA/TM-2005-213751
Funding Number(s)
OTHER: 23-063-30-RF
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
No Preview Available