Real-Time System Verification by k-Induction

• ABSTRACT:
  
  We 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 property is satisfied.

• BIBTEX:
  

  @TechReport{pike:kind,
    author =       {Lee Pike},
    title =        {Real-Time System Verification by $k$-Induction},
    institution =  {NASA Langley Research Center},
    year =         {2005},
    number =       {TM-2005-213751},
    month =        {May},
    note =         {Available at \url{https://leepike.github.io/pub_pages/reint.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

• ERRATA: Page 29: In the Architectures Verified paragraph,"Byzantine fault" should read "value fault".

• NOTES:
  • A revised and shortened 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.