Modular Certification

John Rushby

Technical Report, September 2001

Also available as NASA Contractor Report CR-2002-212130 (pdf)


Airplanes are certified as a whole: there is no established basis for separately certifying some components, particularly software-intensive ones, independently of their specific application in a given airplane. The absence of separate certification inhibits the development of modular components that could be largely ``precertified'' and used in several different contexts within a single airplane, or across many different airplanes. In this report, we examine the issues in modular certification of software components and propose an approach based on assume-guarantee reasoning. We extend the method from verification to certification by considering behavior in the presence of failures. This exposes the need for partitioning, and separation of assumptions and guarantees into normal and abnormal cases. We then identify three classes of property that must be verified within this framework: safe function, true guarantees, and controlled failure.

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

BibTeX Entry

	TITLE = {Modular Certification},
	AUTHOR = {John Rushby},
	ADDRESS = mp,
	MONTH = sep,
	YEAR = 2001

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