Formal analysis for dependability properties: the time-triggered architecture example

This paper describes the mechanized formal verification we have performed on some of the crucial algorithms used in the Time-Triggered Architecture (ITA) for safety-critical distributed control. We outline the approach taken to formally analyse the dock synchronization algorithm and the group membership service of TTA, summarize our experience and describe remaining challenges.