Formal Verification of Time-Triggered Systems

• ABSTRACT:
  
  Fault-tolerant real-time distributed control systems are being developed for next-generation aircraft and automobiles. They employ numerous complex protocols; because their uses are safety-critical, the design and implementation of these protocols must be error-free. The following modeling considerations make the formal verification of these protocols difficult: faults, real-time constraints, distributed control, nonfunctional behavioral requirements, and intricate protocol interactions. We describe a methodology for the formal verification of time-triggered systems, a class of synchronized fault-tolerant control and communication architectures.
  
  The methodology centers around the distinct timing assumptions made in time-triggered systems. First, we describe a set of abstractions for specifying time-triggered protocols in an untimed synchronous model of computation that is particularly well-suited for mechanical theorem-proving. The abstractions systematically abstract faults, data, communication, and fault-masking. An untimed synchronous specification simplifies the specification and verification overhead, but a large semantic gap exists between the timing characteristics of an untimed protocol specification and its implementation. We therefore extend previous work to formally demonstrate via mechanical theorem-proving that under certain assumptions, a simulation exists between a time-triggered implementation of a protocol and its untimed synchronous specification. We then use a combination of bounded model-checking and automated solvers to verify that realized protocol schedules satisfy the necessary time-triggered assumptions. Finally, some protocols do not satisfy the time-triggered model constraints due to the fact they execute when the system is unsynchronized, such as during startup or restart. We also use bounded model-checking and automated solvers to verify explicit real-time models of such protocols.
  
  The methodology is demonstrated by verifying NASA Langley's SPIDER fly-by-wire bus architecture.

• BIBTEX:
  

  @PhdThesis{pike_diss,
    author = {Lee Pike},
    title  = {Formal Verification of Time-Triggered Systems},
    school = {Indiana University},
    year   = {2006},
    note   = {Available at \url{https://leepike.github.io/phd.html}}}
  

• DISSERTATION DOWNLOAD: pdf
  The dissertation is also available directly from Indiana University here under the Creative Commons Attribution 3.0 Unported License.

• SLIDES DOWNLOAD: pdf

• FILES DOWNLOAD:
  
  
  • Chapter 3: Synchronous Protocol Verification
    • Abstractions Specification and Verification (PVS dump file)
  • Chapter 4: Time-Triggered Protocol Verification
    • Rushby's Original Theory Mended with an Interpretation (PVS dump file)
    • Enhanced Time-Triggered Specification and Interpretation (PVS dump file)
    • Verified SPIDER Distributed Diagnosis Protocol Schedule (SAL file)
    • Verified SPIDER Clock Synchronization Protocol Schedule (SAL file)
    • Optimized Schedule (SAL file)
  • Chapter 5: Partially-Synchronous Protocol Verification
    • reintegration (SAL file)
    • reintegration proof script
    • STA model of the Train-Gate-Controller (SAL file)
    • clockless STA model of the Train-Gate-Controller (SAL file)

• ADDENDUM:
  
  Portions of Chapter 3 and most of Chapter 4 (and their supporting files) have been revised, shortened, and small errors have been corrected in a FMCAD, 2007 paper. The paper and files are available here. I suggest that paper be consulted in lieu of Chapter 4.