An Overview of Formal Verification for the Time-Triggered Architecture

John Rushby

Invited paper, presented at FTRTFT'02, Oldenburg, Germany, September 2002. Copyright Springer Verlag LNCS

Abstract

We describe formal verification of some of the key algorithms in the Time-Triggered Architecture (TTA) for real-time safety-critical control applications. Some of these algorithms pose formidable challenges to current techniques and have been formally verified only in simplified form or under restricted fault assumptions. We describe what has been done and what remains to be done and indicate some directions that seem promising for the remaining cases and for increasing the automation that can be applied. We also describe the larger challenges posed by formal verification of the interaction of the constituent algorithms and of their emergent properties.

gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)

Slides

gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)

BibTeX Entry


@inproceedings{Rushby02:FTRTFT,
	AUTHOR = {John Rushby},
	TITLE = {An Overview of Formal Verification for the Time-Triggered Architecture},
	BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems},
	PAGES = {83--105},
	SERIES = {Lecture Notes in Computer Science},
	PUBLISHER = {Springer-Verlag},
	VOLUME = 2469,
	EDITOR = {Werner Damm and Ernst-R\"{u}diger Olderog},
	ADDRESS = {Oldenburg, Germany},
	YEAR = 2002, 
	MONTH = sep
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page