Formal analysis for dependability properties: the time-triggered architecture example
Holger Pfeifer, Friedrich W. von Henke · 2002
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.