Formal Verification of Time-Triggered Systems

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 methodolog