Formal Verification of Time-Triggered Systems

Loading...
Thumbnail Image
Date
2010-06-01
Journal Title
Journal ISSN
Volume Title
Publisher
[Bloomington, Ind.] : Indiana University
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.
Description
Thesis (PhD) - Indiana University, Computer Sciences, 2006
Keywords
Citation
DOI
Link(s) to data and video for this item
Relation
Rights
This work is licensed under the Creative Commons Attribution 3.0 Unported License.
Type
Doctoral Dissertation