NASA Langley's research and technology-transfer program in formal methods

19 November 2002

proceedings article
Published by Institute of Electrical and Electronics Engineers (IEEE)

Vol. 697, 135-149
https://doi.org/10.1109/cmpass.1995.521893

Abstract

This paper presents an overview of NASA Langley's research program in formal methods. The major goals of this work are to make formal methods practical for use on high integrity systems, to orchestrate the transfer of this technology to U.S. industry through use of carefully designed demonstration projects, and to exploit this technology to help achieve NASA's goals in aeronautics. Several direct technology transfer eorts have been initiated that apply formal methods to critical subsystems of real aerospace computer systems.

Keywords

This publication has 28 references indexed in Scilit:

Formally specifying the logic of an automatic guidance controller
Published by Springer Nature ,2005
A formally verified algorithm for interactive consistency under a hybrid fault model
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
Formal verification of an interactive consistency algorithm for the Draper FTP architecture under a hybrid fault model
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
A formally verified algorithm for clock synchronization under a hybrid fault model
Published by Association for Computing Machinery (ACM) ,1994
Illustrative risks to the public in the use of computer systems and related technology
ACM SIGSOFT Software Engineering Notes, 1994
DDD-FM9001: Derivation of a verified microprocessor
Published by Springer Nature ,1993
Design for validation
IEEE Aerospace and Electronic Systems Magazine, 1992
Penelope, an Ada verification system
Published by Association for Computing Machinery (ACM) ,1989
Synchronizing clocks in the presence of faults
Journal of the ACM, 1985
Using Time Instead of Timeout for Fault-Tolerant Distributed Systems.
ACM Transactions on Programming Languages and Systems, 1984