Formal Analysis of Fault-Tolerant
Algorithms in the
Time-Triggered Architecture

This thesis is about formal analysis of fault-tolerant algorithms implemented in the Time-Triggered Protocol TTP/C. The services provided by this communication protocol are characterized by a deep integration and mutual dependencies, which constitute significant sources of complicacy for formal analysis in addition to the inherent difficulty of analyzing fault-tolerant distributed algorithms. Consequently, the main goal of this thesis is to explore and develop techniques to structure and organize the formal models that describe the protocol services and the fault assumptions, as well as the proofs in a way that enables the required correctness properties be established. Due to their central role for TTP/C we concentrate the formal analysis on the two most important algorithms of the protocol, namely clock synchronization and group membership. Because of the immense complexity and detail of TTP/C a formal approach must try to isolate the core algorithms from the integrated protocol and analyse them separately. However, as the services are tightly intertwined, the process of isolating a particular service also amounts to identifying the dependencies on and suitable interfaces to other protocol parts. On the other hand, if the formal analysis of a particular service is carried out in isolation of other protocol aspects, the question arises whether any correctness statements are meaningful for the integrated protocol. Therefore, the formal models and proofs must be structured in a way that enables the various isolated analyses to be combined into a larger context. In order to do so, the formal models must provide interfaces through which other models or proofs can exchange information or other requirements. For the provision of these interfaces abstraction plays a crucial role. We show how two flavours of abstraction techniques can provide the required separation of protocol services of TTP/C without compromising the possibility of adequately integrating the different analyses. Altogether, the formal analysis contributes to providing an isolated formal model for the single services, a clear statement of the interfaces and mutual dependencies, the realization of correctness propositions for the individual services, and finally, the demonstration of the validity of these correctness arguments for the integrated protocol description.

Online Copy

Thesis is available as PDF-File (213 pages / 861 KB)

BibTeX Entry

@phdthesis{pfeifer03:phd, author = {Holger Pfeifer}, title = "{Formal Analysis of Fault-Tolerant Algorithms in the Time-Triggered Architecture}", school = {Universit{\"{a}}t Ulm}, address = {Germany}, year = 2003, url = {http://www.informatik.uni-ulm.de/ki/Papers/pfeifer03-diss.pdf}}