NASA Langley FM Publications

1. NASA Langley's Research and Technology Transfer Program in Formal Methods, an informal overview of our program is available in (PostScript and PDF). It is a bit out of date.
2. Ricky W. Butler, A Primer on Architectural Level Fault Tolerance, NASA/TM-2008-215108, Feb 2008.
3. Ricky Butler, Radu Siminiceanu and César Muñoz, The ANMLite Language and Logic for Specifying Planning Problems, NASA/TM-2007-215089 , Nov 2007.
4. Ricky Butler, César Muñoz, and Radu Siminiceanu, Solving the AI Planning Plus Scheduling Problem Using Model Checking via Automatic Translation from the Abstract Plan Preparation Language (APPL) to the Symbolic Analysis Laboratory (SAL), NASA/TM-2007-215089 , Nov 2007.
5. Kelly J. Hayhurst, Jeffrey M. Maddalon, Paul S. Miner, George N. Szatkowski, Michael L. Ulrey, Michael P. DeWalt, Cary R. Spitzer. Preliminary Considerations for Classifying Hazards of Unmanned Aircraft Systems. NASA Technical Memorandum (TM-2007-214539), February 2007.
6. Ricky Butler and César Muñoz, A Plan Preparation Language, NASA/TM-2006-214518, Nov 2006.
7. Hayhurst, Kelly J.; Maddalon, Jeffrey M.; Miner, Paul S.; DeWalt, Michael P.; McCormick, G. Frank Unmanned Aircraft Hazards and their Implications for Regulation , 15-19 Oct. 2006; 25th Digital Avionics Systems Conference; Portland, Oregon.

8. Songtao Xia, Ben Di Vito and César Muñoz. Predicate Abstraction of Programs Containing Non-linear Computation. In ATVA 2006, Fourth International Symposium on Automated Technology for Verification and Analysis, Beijing, China, October 2006.

9. T. Pressburger, L. Markosian, B. Di Vito, M. Feather, M. Hinchey and L. Treviño. Infusing Software Assurance Research Techniques into Use. In IEEE 2006 Aerospace Conference, IEEE, Big Sky, MT, March 2006.

10. Songtao Xia, Ben Di Vito and César Muñoz. Automated Test Generation for Engineering Applications. In Automated Software Engineering 2005, ACM, Long Beach, CA, November 2005.

11. Songtao Xia and Ben Di Vito. Software Certification for Temporal Properties with Affordable Tool Qualification. In Workshop on Software Certificate Management (SoftCeMent), Long Beach, CA, November 2005.

12. Lee Pike and Steven D. Johnson. The formal verification of a reintegration protocol. Accepted at the ACM Conference on Embedded Software (EMSOFT), 2005.
13. Holloway, C. Michael; Johnson, Chris W.: "On the Prevalence of Organizational Factors in Recent U.S. Transportation Accidents", to appear in Proceedings of the 23rd International System Safety Conference, 22-26 August 2005, San Diego, California.
14. Johnson, Chris W.; Holloway, C. Michael: "A Technique for Showing Causal Arguments in Accident Reports", to appear in Proceedings of the 23rd International System Safety Conference, 22-26 August 2005, San Diego, California.
15. Lee Pike. Real-time system verification by k-induction. NASA Technical Memorandum TM-2005-213751, April 2005.
16. Wilfredo Torres-Pomales, Mahyar R. Malekpour, and Paul S. Miner.  ROBUS-2: A fault-tolerant broadcast communication system.  NASA/TM-2005-213540, March 2005, pp. 201.
17. Lee Pike, Jeffrey Maddalon, Paul Miner, and Alfons Geser. Abstractions for fault-tolerant distributed system verification. In Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors, Theorem Proving in Higher Order Logics (TPHOLs), volume 3223 of Lecture Notes in Computer Science, pages 257--270. Springer, 2004.
18. Lee Pike, Paul Miner, Wilfredo Torres. Model Checking Failed Conjectures in Theorem Proving: A Case Study. NASA Technical Memorandum NASA/TM-2004-213278, October 2004.
    Proof files are available here.
19. Victor Carreño and César Muñoz, Implicit Intent Information for Conflict Detection and Alerting, Proceedings of the 23th Digital Avionics Systems Conference, DASC 2004, Salt Lake City, Utah, October 2004.

20. Ricky W. Butler, Formalization of the Integral Calculus in the PVS Theorem Prover, NASA/TM-2004-213279, October 2004

21. Paul Miner, Alfons Geser, Lee Pike, and Jeffrey Maddalon. A Unified Fault-tolerance Protocol.In Yassine Lakhnech and Sergio Yovine, editors, Formal Techniques, Modeling and Analysis of Timed and Fault-Tolerant Systems (FORMATS-FTRTFT), volume 3253 of Lecture Notes in Computer Science, pages 167--182. Springer, 2004.
22. M. Consiglio, C. Muñoz, and V. Carreño, Conflict Detection and Alerting in a Self Controlled Terminal Aerospace, 24th International Congress of the Aeronautical Sciences, Yokohama, Japan, August 2004.

23. Johnson, Chris W.; Holloway, C. Michael: "`Systemic Failures' and `Human Error' in Canadian TSB Aviation Accident Reports between 1996 and 2002," Proceedings of HCI in Aerospace 2004, 29 September - 1 October 2004, Toulouse, France.
24. Holloway, C. Michael; Johnson, Chris W.: "Distribution of Causes in Selected U.S. Aviation Accident Reports Between 1996 and 2003," Proceedings of the 22nd International System Safety Conference, 2-6 August 2004, Providence, Rhode Island.

25. César Muñoz, Gilles Dowek, and Victor Carreño, Modeling and Verification of an Air Traffic Concept of Operations, International Symposium on Software Testing and Analysis, Boston, Massachusetts, July 2004.

26. Jeffrey Maddalon, Ricky Butler, Alfons Geser and Cesar Munoz, Formal Verification of a Conflict Resolution and Recovery Algorithm , NASA/TP-2004-213015, April 2004, pp. 82.
27. Gerard Allwein, Hilmi Demir, Lee Pike, Logics for Classes of Boolean Monoids, Journal of Logic, Language and Information.  13-3: 2004 (Kluwer).  pp. 241-266.
    
28. Gilles Dowek, César A. Muñoz, and Victor Carreño, An Abstract Model of the SATS Concept of Operations: Initial Results and Recommendations, NASA/TM-2004-213006, March 2004.

29. Victor A. Carreno, Hanne Gottliebsen, Ricky Butler and Sara Kalvala, Formal Modeling and Analysis of a Preliminary Small Aircraft Transportation System (SATS) Concept, NASA/TM-2004-212999, March 2004, pp. 44.
30. Paul Miner, Alfons Geser, Lee Pike, and Jeffery Maddalon. A unified fault-tolerance protocol. In Yassine Lakhnech and Sergio Yovine, editors, Formal Techniques, Modeling and Analysis of Timed and Fault-Tolerant Systems (FORMATS-FTRTFT), volume 3253 of Lecture Notes in Computer Science, pages 167--182. Springer, 2004. Proof files are available here.
31. Lee Pike, Jeffery Maddalon, Paul Miner, and Alfons Geser. Abstractions for fault-tolerant distributed system verification. In Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors, Theorem Proving in Higher Order Logics (TPHOLs), volume 3223 of Lecture Notes in Computer Science, pages 257--270. Springer, 2004.  Proof files are available here.
32. Elizabeth Latronico, Paul Miner, and Philip Koopman. Quantifying the Reliability of Proven SPIDER Group Membership Service Guarantees. Dependable Systems and Networks (DSN), 2004. 

33. Ricky Butler, Alfons Geser, Jeffrey Maddalon, and César Muñoz: Formal Analysis of Air Traffic Management Systems: The case of Conflict Resolution and Recovery, Proceedings of Winter Simulation Conference (WSC'03), New Orleans, December 2003, pp. 906-914, ISBN 0-7803-8132-7.
34. Johnson, Chris W.; Holloway, C. Michael: "The ESA/NASA SOHO Mission Interruption: Using the STAMP Accident Analysis Technique for a Software Related `Mishap'", Software: Practice and Experience, Volume 33, Number 12, October 2003, pp. 1177-1198.
35. Victor A. Carreno: Concept for Multiple Operations at Non-Tower Non-Radar Airports During Instrument Meteorological Conditions, Proceeding of the 22nd Digital Avionics Systems Conference, DASC 2003, Indianapolis, Indiana, 12-16 October 2003.
36. Hayhurst, Kelly J.; Holloway, C. Michael: "Considering Object Oriented Technology in Aviation Applications", Proceedings of the 22nd Digital Avionics Systems Conference, 12-16 October 2003, Indianapolis, Indiana, paper 3.B.1.
37. Ben L. Di Vito: Strategy-Enhanced Interactive Proving and Arithmetic Simplification for PVS, 1st International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), Roma, Italy, September 8, 2003.
38. M. Archer, B. Di Vito and C. Muñoz, editors. Design and Application of Strategies/Tactics in Higher Order Logics. NASA Conference Publication NASA/CP-2003-212448, NASA Langley Research Center, Hampton, VA, September 2003.

39. César Muñoz, Ricky Butler, Víctor Carreño, and Gilles Dowek: Formal verification of conflict detection algorithms, International Journal on Software Tools for Technology Transfer, 2003.
40. Myla Archer, Ben Di Vito and Cesar Munoz, Editors, Design and Application of Strategies/Tactics in Higher Order Logics, NASA/CP-2003-212448, September 2003, pp. 118.
41. Proceedings of the Second Workshop on the Investigation and Reporting of Incidents and Accidents (IRIA 2003), NASA/CP-2003-212642, Kelly J. Hayhurst and C. Michael Holloway (compilers), September 2003.
42. Holloway, C. Michael; Hayhurst, Kelly J.: "Software System Safety & the NASA Aeronautics Blueprint", Proceedings of the 21st International System Safety Conference, 4-8 August 2003, Ottawa, Ontario, Canada, pp. 1183-1192.
43. Johnson, Chris W.; Holloway, C. Michael: "The Strengths and Weaknesses of Logic Formalisms to Support Mishap Analysis", Proceedings of the 21st International System Safety Conference, 4-8 August 2003, Ottawa, Ontario, Canada, pp. 1133-1142.
44. Johnson, Chris W.; Holloway, C. Michael: "A Survey of Logic Formalisms to Support Mishap Analysis", Reliability Engineering and Systems Safety, Volume 80, Issue 3, June 2003, pp 271-291.
45. Jeffrey M. Maddalon and Paul S. Miner: An Architectural Concept for Intrusion Tolerance in Air Traffic Networks, 3rd Integrated Communications, Navigation, and Surveillance (ICNS) Conference & Workshop, Annapolis, Maryland, May 19-22, 2003.
46. Victor A. Carreño, Evaluation of a Pair-Wise Conflict Detection and Resolution Algorithm in a Multiple Aircraft Scenario December 2002.

47. Alfons Geser and Paul Miner.   A New On-line Diagnosis Protocol for the SPIDER Family of Byzantine Fault Tolerant Architectures .  NASA TM, 2003.
48. Hayhurst, Kelly J; Holloway, C. Michael: "Aviation Software Guidelines", IEEE Software, Volume 19, Number 5, Sep/Oct 2002.
49. Holloway, C. Michael: " Issues in Software System Safety: Polly Ann Smith Co. v. Ned I. Ludd", in the Proceedings of the 20th International System Safety Conference, Aurora, CO, 5-9 August 2002, pp. 75-84.
50. Victor A. Carreño, Cesar Muñoz, and Sofiéne Tahar, Eds., Theorem Proving in Higher Order Logics Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, NASA/CP-2002-211736, August 2002, pages 198.

51. Ben L. Di Vito: A PVS Prover Strategy Package for Common Manipulations, NASA/TM-2002-211647, April 2002.
52. Alfons Geser, Paul Miner.   A Formal Correctness Proof of the SPIDER Diagnosis Protocol .  Theorem-Proving in Higher-Order Logics (TPHOLs), track B, 2002.
53. Paul S. Miner, Mahyar R. Malekpour, Wilfredo Torres.  A Conceptual Design For a Reliable Optical Bus (ROBUS).  Presented at the 21st Digital Avionics Systems Conference (DASC), Irvine, California, October 27-31, 2002.
54. Hayhurst, Kelly J; Holloway, C. Michael: "Challenges in Software Aspects of Aviation Systems", in the Proceedings of the 26 Annual NASA Goddard Software Engineering Workshop (IEEE/NASA SEW-26), 27-29 November 2001, Greenbelt, MD, pp. 7-13.
55. Kelly J. Hayhurst, Dan S. Veerhusen, John J. Chilenski, and Leanna K. Rierson, A Practical Tutorial on Modified Condition/Decision Coverage NASA/TM-2001-210876, NASA Langley Research Center,Hampton, Virginia, May 2001.
56. Cesar Munoz, Ricky W. Butler,Victor A. Carreño, and Gilles Dowek. On the Formal Verification of Conflict Detection Algorithms, NASA/TM-2001-210864, May 2001.
57. César Muñoz, Ricky Butler, Víctor Carreño, and Gilles Dowek, Verification of Conflict Detection Algorithms, Proceedings of the 11th Working Conference on Correct Hardware Design and Verification Methods, CHARME 2001. Extended version available as NASA/TM-2001-210864.
58. Victor Carreño and Cesar Muñoz, Formal Analysis of Parallel Landing Scenarios Proceedings of the 19th Digital Avionics Systems Conference, DASC 2000. (PostScript).

59. Carreno, Victor and Cesar Munoz, Aircraft trajectory modeling and alerting algorithm verification , ICASE Report 2000-16, 2000-04-01.
60. C. Michael Holloway (compiler). Lfm2000: Fifth NASA Langley Formal Methods Workshop. NASA/CP-2000-210100, NASA Langley Research Center, Hampton, Virginia, June 2000.

61. Kelly J. Hayhurst, Cheryl A. Dorsey, John C. Knight, Nancy G. Leveson and G. Frank McCormick, Streamlining Software Aspects of Certification: Report on the SSAC Survey, NASA/TM-1999-209519, August 1999, 100 pages. Information on the SSAC project is here.
62. C. Michael Holloway: From Bridges and Rockets, Lessons for Software Systems, in the Conference Proceedings of the 17th International System Safety Conference, August 16-21, 1999, Orlando, Florida, pages 598-607.
63. Luettgen, Gerald; Carreno, Victor: Analyzing mode confusion via model checking , ICASE Report 99-18, 1999-05-01.
64. Steven P. Miller and James N. Potts. Detecting Mode Confusion Through Formal Modeling and Analysis. NASA Contractor Report CR-1999-208971, January 1999, 69 pages.
65. Ben L. Di Vito. A Model of Cooperative Noninterference for Integrated Modular Avionics. In Proceedings of Dependable Computing for Critical Applications (DCCA-7), San Jose, CA, January 1999.
66. Ricky W. Butler, Steven P. Miller, James N. Potts, and Victor A. Carreño. A Formal Methods Approach to the Analysis of Mode Confusion. In 17th AIAA/IEEE Digital Avionics Systems Conference, October 31-November 6 1998. (PostScript)
67. Ben L. Di Vito. A Formal Model of Partitioning for Integrated Modular Avionics. NASA Contractor Report CR-1998-208703, NASA Langley Research Center, Hampton, Virginia, August 1998.
68. Kelly J. Hayhurst. Framework for Small-Scale Experiments in Software Engineering. NASA Technical Memorandum TM-1998-207666, NASA Langley Research Center, Hampton, Virginia, May 1998.
69. K. J. Hayhurst, C. M. Holloway, C. A. Dorsey, J. C. Knight, N. G. Leveson, G. F. McCormick, and J. C. Yang. Streamlining Software Aspects of Certification: Technical Team Report on the First Industry Workshop. NASA Technical Memorandum TM-1998-207648, NASA Langley Research Center, Hampton, Virginia, April 1998. Information on the SSAC project is here.
70. Ricky W. Butler and J. A. Sjogren. A PVS Graph Theory Library. NASA Technical Memorandum TM-1998-206923, NASA Langley Research Center, Hampton, Virginia, February 1998.
71. C. Michael Holloway. Why Engineers Should Consider Formal Methods. In 16th AIAA/IEEE Digital Avionics Systems Conference, Volume 1, pages 1.3-16 -- 1.3-22, October 26-30 1997. Presentation slides are available.
72. C. Michael Holloway and Kelly J. Hayhurst (compilers). Lfm97: Fourth NASA Formal Methods Workshop. NASA Conference Publication 3356, NASA Langley Research Center, Hampton, Virginia, September 1997.
73. Ben L. Di Vito. Using Formal Methods to Assist in the Requirements Analysis of the Space Shuttle GPS Change Request. NASA Contractor Report 4752, NASA Langley Research Center, Hampton, Virginia, August 1996.
74. Ricky W. Butler. An Introduction to Requirements Capture Using PVS: Specification of a Simple Autopilot. NASA Technical Memorandum 111025, NASA Langley Research Center, Hampton, Virginia, May 1996. ( Revised Paper(PostScript))
75. C. Michael Holloway and Ricky W. Butler. Impediments to Industrial Use of Formal Methods. IEEE Computer, 29(4):25-26, April 1996. (PostScript)
76. Ben L. Di Vito. Formalizing New Navigation Requirements for NASA's Space Shuttle. In Formal Methods Europe (FME '96), pages 160-178, Oxford, England, March 1996. Also Lecture Notes in Computer Science 1051, Springer.
77. Judith Crow and Ben L. Di Vito. Formalizing Space Shuttle Software Requirements. In Workshop on Formal Methods in Software Practice (FMSP '96), pages 40-48, San Diego, California, January 1996.
78. C. Michael Holloway. Ada 95 and Safety-Critical Software. In 14th AIAA/IEEE Digital Avionics Systems Conference, pages 504-509, November 1995. Presentation slides are available.
79. Victor A. Carreño. Interpretation of IEEE-854 Floating-Point Standard and Definition in the HOL System. NASA Technical Memorandum 110189, NASA Langley Research Center, Hampton, Virginia, September 1995.
80. C. Michael Holloway, (editor). Third NASA Formal Methods Workshop 1995. NASA Conference Publication 10176, NASA Langley Research Center, Hampton, Virginia, June 1995.
81. Paul S. Miner. Defining the IEEE-854 Floating-Point Standard in PVS. NASA Technical Memorandum 110167, NASA Langley Research Center, Hampton, Virginia, June 1995.
82. Ricky W. Butler, James L. Caldwell, Victor A. Carreño, C. Michael Holloway, Paul S. Miner, and Ben L. Di Vito. NASA Langley's Research and Technology Transfer Program in Formal Methods. In Tenth Annual Conference on Computer Assurance (COMPASS 95), Gaithersburg, MD, June 1995. A revised version is viewable here in PostScript and PDF. (PostScript)
83. C. Michael Holloway, Ben Di Vito, David Guaspari, and Michael Smith. Formal Methods: Fact vs. Fiction. In Tri-Ada '94, November 1994. Panel Summary and Position Papers.
84. C. Michael Holloway. Epistemology, Software Enginering, and Formal Methods. In The Role of Computers in Research and Development at Langley Research Center, pages 570-595, October 1994. NASA Conference Publication 10159.
85. Ricky W. Butler, Ben L. Di Vito, and C. Michael Holloway. Formal Design and Verification of a Reliable Computing Platform For Real-Time Control (Phase 3 Results). NASA Technical Memorandum 109140, NASA Langley Research Center, Hampton, Virginia, August 1994.
86. Ricky W. Butler. An Elementary Tutorial on Formal Specification and Verification Using PVS. NASA Technical Memorandum 108991, NASA Langley Research Center, Hampton, Virginia, September 1993. Revised in 1995.
87. Ricky W. Butler and Sally C. Johnson. Formal Methods For Life-Critical Software. In Computing in Aerospace 9 Conference, pages 319-329, San Diego, California, October 1993.
88. Paul S. Miner. Verification of Fault-Tolerant Clock Synchronization Systems. NASA Technical Paper 3349, NASA Langley Research Center, Hampton, Virginia, November 1993. (PostScript)
89. Ricky W. Butler">Ricky W. Butler and George B. Finelli. The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software. IEEE Transactions on Software Engineering, 19(1):3-12, January 1993.
90. Ben L. Di Vito and Ricky W. Butler. Provable Transient Recovery for Frame-Based, Fault-Tolerant Computing Systems. In Real-Time Systems Symposium, Phoenix, Arizona, December 1992.
91. Sally C. Johnson, C. Michael Holloway, and Ricky W. Butler (editors). Second NASA Formal Methods Workshop 1992. NASA Conference Publication 10110, NASA Langley Research Center, Hampton, Virginia, November 1992.
92. Paul S. Miner, Peter A. Padilla, and Wilfrbsp;A. Padilla, and Wilfredo Torres. A Provably Correct Design of a Fault-Tolerant Clock Synchronization Circuit. In 11th Digital Avionics Systems Conference, pages 341-346, Seattle, Washington, October 1992.
93. Ben L. Di Vito and Ricky W. Butler. Formal Techniques for Synchronized Fault-Tolerant Systems. In Dependable Computing for Critical Applications 3, Dependable Computing and Fault-Tolerant Systems, pages 279-306. Springer Verlag, New York, 1993. Also presented at 3rd IFIP Working Conference on Dependable Computing for Critical Applications, Mondello, Sicily, Italy, Sept. 14-16, 1992.
94. Paul S. Miner. A Verified Design of a Fault-Tolerant Clock Synchronization Circuit: Preliminary Investigations. NASA Technical Memorandum 107568, NASA Langley Research Center, Hampton, Virginia, March 1992.
95. Ben L. ito-os-IFIP">Ben L. Di Vito, Ricky W. Butler, and James L. Caldwell. High Level Design Proof of a Reliable Computing Platform. In Dependable Computing for Critical Applications 2, Dependable Computing and Fault-Tolerant Systems, pages 279-306. Springer Verlag, New York, 1992. Also presented at 2nd IFIP Working Conference on Dependable Computing for Critical Applications, Tucson, Arizona, Feb. 18-20, 1991, pp. 124-136.
96. Paul S. Miner. An Extension to Schneider's General Paradigm for Fault-Tolerant Clock Synchronization. NASA Technical Memorandum 107634, NASA Langley Research Center, Hampton, Virginia, 1992.
97. Sally C. Johnson and Ricky W. Butler. Design For Validation. IEEE Aerospace and Electronics Systems, pages 38-43, January 1992. Also appeared in the AIAA/IEEE 10th Digital Avionics Systems Conference, Los Angeles, California, Oct. 7-11, 1991, pp. 487-492. (PostScript)
98. Ricky W. Butler and Ben L. Di Vito. Formal Design and Verification of a Reliable Computing Platform For Real-Time Control (Phase 2 Results). NASA Technical Memorandum 104196, NASA Langley Research Center, Hampton, Virginia, January 1992.
99. Ricky W. Butler and George B. Finelli. The Infeasibility of Experimental Quantification of Life-Critical Software Reliability. In Proceedings of the ACM SIGSOFT '91 Conference on Software for Critical Systems, pages 66-76, New Orleans, Louisiana, December 1991.na, December 1991. (PostScript)
100. Victor A. Carreño and Rob K. Angellatta. A Case Study for the Real-Time Experimental Evaluation of the VIPER Microprocessor. NASA Technical Memorandum 104098, NASA Langley Research Center, Hampton, Virginia, September 1991.
101. Ricky W. Butler. NASA Langley's Research Program in Formal Methods. In 6th Annual Conference on Computer Assurance (COMPASS 91), Gaithersburg, Maryland, June 1991.
102. Ricky W. Butler, James L. Caldwell, and Ben L. Di Vito. Design Strategy for a Formally Verified Reliable Computing Platform. In 6th Annual Conference on Computer Assurance (COMPASS 91), Gaithersburg, Maryland, June 1991.
103. Ricky W. Butler and Jon A. Sjogren. Formal Design Verification of Digital Circuitry. Reliability Engineering and System Safety, 32(1 and 2):67-93, 1991.
104. Ricky W. Butler, (editor). NASA Formal Methods Workshop 1990. NASA Conference Publication 10052, NASA Langley Research Center, Hampton, Virginia, November 1990.
< p>
105. Ben L. Di Vito, Ricky W. Butler, and James L. Caldwell, II. Formal Design and Verification of a Reliable Computing Platform For Real-Time Control (Phase 1 Results). NASA Technical Memorandum 102716, NASA Langley Research Center, Hampton, Virginia, October 1990.
< p>
106. Ricky W. Butler and Jon A. Sjogren. Hardware Proofs Using EHDM and the RSRE Verification Methodology. NASA Technical Memorandum 100669, NASA LangleMemorandum 100669, NASA Langley Research Center, Hampton, Virginia, December 1988.

Note: The tag identifies links that are outside of the NASA domain.