The Formal Verification of a Reintegration Protocol

• ABSTRACT:
  
  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.

• BIBTEX:
  

  @inproceedings{pike_johnson:emsoft,
    author = {Lee Pike and Steven D. Johnson},
    title = {The formal verification of a reintegration protocol},
    booktitle = {EMSOFT '05: Proceedings of the 5th ACM international conference on Embedded software},
    year = {2005},
    pages = {286--289},
    location = {Jersey City, NJ, USA},
    publisher = {ACM Press},
    address = {New York, NY, USA},
    note = {Available at \url{https://leepike.github.io/pub_pages/emsoft.html}}}
  

• PAPER DOWNLOAD: pdf 

• SLIDES DOWNLOAD: pdf

• SAL FILES DOWNLOAD:
  • reintegration (reintegration proof script)
  • STA model of the Train-Gate-Controller
  • clockless STA model of the Train-Gate-Controller

• NOTES:
  • An expanded version of this paper is available here.
  • The SMT verification conditions from this work are some of the SMT-LIB quantifier-free linear real-arithmetic benchmarks.