Skip past navigation NASA Langley Formal Methods



quick page






  home > publications > ORApublications > ORA

Odyssey Research Associates Publications

  1. Naydich, Dimitri and Nowakowski, John: Flight Guidance System Validation using SPIN . NASA Contractor Report NASA/CR-1998-208434, June 1998.

  2. Fung, Francis, and Jamsek, Damir: Formal Specification of a Flight Guidance System . NASA Contractor Report CR-1998-206915, January 1998

  3. Hoover, D. N. A Mathematical Model for Railway Control Systems.way Control Systems. NASA Contractor Report 198353, June 1996.

  4. Hoover, D. N; Guaspari, and Humenn, Polar: Applications of Formal Methods to Specification and Safety of Avionics Software. NASA Contractor Report 4723, April 1996.

  5. Guaspari, David; McHugh, John; Polak, Wolfgang; and Saaltink, Mark: Towards a Formal Semantics for Ada 9X. NASA Contractor Report 195037, March 1995.

  6. Hoover, D. N.; and Chen, Zewei: TBell: A Mathematical Tool for Analyzing Decision Tables. NASA Contractor Report 195027, November 1994.

  7. Weber Doug; and Jamsek, Damir: Using Formal Specification in the Guidance and Control Software (GCS) Experiment. NASA Contractor Report 194884, April 1994.

  8. Bickford, Mark: A Formal Semantics for a Subset of VHDL and its Use in Analysis of the FTPP Scoreboard Circuit. NASA Contractor Report 191577, April 1994.

  9. Eichenlaub, Carl T.; Harper, C. Douglas; and Hird, Geoffrey: Using Penelope to Assess the Correctness of NASA Ada Software: A Demonstration of Formal Methods as a Counterpart to Testing. NASA Contractor Report 4509, May 1993.

  10. tor Report 4509, May 1993.

  11. Srivas, Mandayam; and Bickford, Mark: Verification of a Fault-Tolerant Property of a Multiprocessor System. In Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen, The Netherlands, June 1992.

  12. Srivas, Mandayam; and Bickford, Mark: Moving Formal Methods Into Practice: Verifying the FTPP Scoreboard: Phase 1 Results. NASA Contractor Report 189607, May 1992.

  13. Srivas, Mandayam; and Bickford, Mark: Verification of the FtCayuga Fault-Tolerant Microprocessor System (Volume 1: A Case Study in Theorem Prover-Based Verification). NASA Contractor Report 4381, July 1991.

  14. Bickford, Mark; and Srivas, Mandayam: Verification of the FtCayuga Fault-Tolerant Microprocessor System (Volume 2: Formal Specification and Correctness Theorems). NASA Contractor Report 187574, July 1991.

  15. Hird, Geoffrey: Formal Specification And Verification Of Ada Software. In AIAA Computing in Aerospace 8 Conference, Baltimore, MD., Oct. 1991.

  16. Guaspari, David: Formally Specifying the Logic of an Automatic Guidance Controller. In Ada-Europe Conference, Athens, GreAda-Europe Conference, Athens, Greece, May 1991.


  Skip past navigation  
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 6 August 2001 (15:23:37)
ts -->