Paper Info
Title
Formal analysis for dependability properties: the time-triggered architecture example
Abstract
This paper describes the mechanized formal veri- fication we have performed on some of the crucial algorithms used in the Time-Triggered Architecture (TTA) for safety- critical distributed control. We outline the approach taken to formally analyse the clock synchronization algorithm and the group membership service of TTA, summarize our experience and describe remaining challenges.
Year
DOI
Venue
2001
10.1109/ETFA.2001.996387
Antibes-Juan les Pins, France
Keywords
Field
DocType
computer architecture,formal verification,safety-critical software,synchronisation,Time-Triggered Architecture,clock synchronization,formal verification,group membership,safety-critical distributed control
Dependability,Applications architecture,Distributed System Security Architecture,Computer science,Real-time computing,Formal methods,Reference architecture,Time-triggered architecture,Enterprise architecture framework,Formal verification,Distributed computing
Conference
ISBN
Citations 
PageRank 
0-7803-7241-7
1
0.38
References 
Authors
12
2
Name
Order
Citations
PageRank
Holger Pfeifer117912.77
Friedrich W. Von Henke242549.05