Modeling Time-Triggered Protocols and Verifying Their Real-Time Schedules

• ABSTRACT:
  
  Time-triggered systems are distributed systems in which the nodes are independently-clocked but maintain synchrony with one another. Time-triggered protocols depend on the synchrony assumption the underlying system provides, and the protocols are often formally verified in an untimed or synchronous model based on this assumption. An untimed model is simpler than a real-time model, but it abstracts away timing assumptions that must hold for the model to be valid. In the first part of this paper, we extend previous work by Rushby [Rus, 1999] to prove, using mechanical theorem-proving, that for an arbitrary time-triggered protocol, its real-time implementation satisfies its untimed specification. The second part of this paper shows how the combination of a bounded model-checker and a satisfiability modulo theories (SMT) solver can be used to prove that the timing characteristics of a hardware realization of a protocol satisfy the assumptions of the time-triggered model. The upshot is a formally-verified connection between the untimed specification and the hardware realization of a time-triggered protocol with respect to its timing parameters.

• BIBTEX:
  

  @inproceedings{pike:fmcad07,
    author = {Lee Pike},
    title = {Modeling Time-Triggered Protocols and Verifying Their Real-Time Schedules},
    booktitle = {Proceedings of Formal Methods in Computer Aided Design (FMCAD'07)},
    year = {2007},
    publisher = {IEEE},
    note = {Best paper award.  Available at \url{http://www.cs.indiana.edu/~lepike/pub_pages/fmcad.html}.}
  }

• PAPER DOWNLOAD: pdf

• SLIDES DOWNLOAD: pdf

• FILES DOWNLOAD:
  
  
  • Time-Triggered Model and Theory Interpretation (PVS dump file, consistent with PVS 4.0)
  • Verified SPIDER Distributed Diagnosis Protocol Schedule (SAL file)
  • Verified SPIDER Clock Synchronization Protocol Schedule (SAL file)
  • Optimized Schedule (SAL file)