Formal Verification of Transmission Window Timing for the Time-Triggered Architecture

John Rushby

Technical Report, March 2001

Abstract

We formally verify the parameters on the timing of message windows in transmitters, receivers, and bus guardians for the Time-Triggered Architecture.

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

BibTeX Entry


@TECHREPORT{Rushby01:windowtiming,
	TITLE = {Formal Verification of Transmission Window Timing for the
		Time-Triggered Architecture},
	AUTHOR = {John Rushby},
	INSTITUTION = csl,
	ADDRESS = mp,
	MONTH = mar,
	YEAR = 2001
}


Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page