Modular Certification
John Rushby
Technical Report, September 2001
Also available as
NASA Contractor Report CR-2002-212130 (pdf)
Abstract
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
@TECHREPORT{Rushby01:modcert,
TITLE = {Modular Certification},
AUTHOR = {John Rushby},
INSTITUTION = csl,
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