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

Author

Pfeifer, Holger ; Henke, Friedrich V.

Author_Institution

Abt. Kunstliche Intelligenz, Ulm Univ., Germany

fYear

2001

fDate

15-18 Oct. 2001

Firstpage

343

Abstract

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.

Keywords

computer architecture; formal verification; safety-critical software; synchronisation; Time-Triggered Architecture; clock synchronization; formal verification; group membership; safety-critical distributed control; Algorithm design and analysis; Clocks; Computer architecture; Control systems; Distributed control; Embedded system; Formal languages; Logic; Process control; Synchronization;

fLanguage

English

Publisher

ieee

Conference_Titel

Emerging Technologies and Factory Automation, 2001. Proceedings. 2001 8th IEEE International Conference on

Conference_Location

Antibes-Juan les Pins, France

Print_ISBN

0-7803-7241-7

Type

conf

DOI

10.1109/ETFA.2001.996387

Filename

996387

Link To Document

https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=379193