The formal verification of a reintegration protocol
Lee Pike, Steven Johnson · 2005
We report the first formal verification of a reintegration protocol for a safety-critical distributed embedded system. A reintegration protocol increases system survivability by allowing a transiently-faulty node to regain state. 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 using a recently-developed explicit real-time model. Because k-induction has exponential complexity, we optimize this model to reduce the size of k necessary for the verification and to make $k$ invariant to the number of nodes. A corollary of the verification is that a clique avoidance property is satisfied.