Analyzing Cockpit Interfaces Using Formal Methods
John Rushby
Abstract
Modern passenger aircraft are highly automated, and problems at the
interface between the automation and the pilot are implicated in
several accidents. I use a simple example taken from the autopilot
of a widely used aircraft type to demonstrate how formal methods can be used
to analyze some aspects of these interfaces, and to expose potential problems.
This example serves to illustrate the wider thesis that formal methods
can find application in domains outside those traditionally associated
with it, provided only that the phenomena of interest can be modeled
effectively in discrete mathematics.
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{Rushby00:fm-elsewhere,
AUTHOR = {John Rushby},
TITLE = {Analyzing Cockpit Interfaces Using Formal Methods},
BOOKTITLE = {Proceedings of {FM-Elsewhere}},
YEAR = 2000,
EDITOR = {H. Bowman},
ORGANIZATION = {Elsevier},
ADDRESS = {Pisa, Italy},
MONTH = oct,
VOLUME = 43,
SERIES = {Electronic Notes in Theoretical Computer Science},
NOTE = {Available at \url{http://www.elsevier.nl/locate/entcs/volume43.html}}
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page