NASA Langley Formal Methods


home

welcome

quick page

philosophy

team

research

quote

links

new?
  home > team > civil servants > rwb > publications

Ricky W. Butler's Publications

  1. Ricky W. Butler, A Primer on Architectural Level Fault Tolerance, NASA/TM-2008-215108, Feb 2008.

  2. Ricky Butler, Radu Siminiceanu and César Muñoz, The ANMLite Language and Logic for Specifying Planning Problems, NASA/TM-2007-215088, Nov 2007.

  3. 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.

  4. Ricky Butler and César Muñoz, A Plan Preparation Language, NASA/TM-2006-214518, Nov 2006.

  5. Ricky Butler, Formalization of the Integral Calculus in the PVS Theorem Prover NASA/TM-2004-213279, Oct-2004.

  6. 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.

  7. 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.

  8. 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.

  9. R.W. Butler; V. Carreno; G. Dowek and C. Munoz: Formal Verification of Conflict Detection Algorithms, Proceedings of the 11th Working Conference on Correct Hardware Design and Verification Methods CHARME 2001}, Lecture Notes in Computer Science, Vol. 2144, p. 403-417, 2001, Livingston, Scotland, UK. (Postscript, 15 pages). Also published in the International Journal on Software Tools for Technology Transfer in 2003.

  10. Johnson, Sally C.; and Butler, Ricky W.;: Formal Methods, Chapter 21 in The Avionics Handbook, edited by Cary R. Spitzer, CRC Press, 2001

  11. Cesar Munoz; Ricky W. Butler; Victor A. Carreno; and Gilles Dowek, On the Formal Verification of Conflict Detection Algorithms, NASA/TM-2001-210864, May 2001.

  12. Butler, Ricky W., WinSURE: A New Windows Interface to the SURE Program, 19th Digital Avionics Systems Conference; Oct 7-13, 2000 Philadelphia, PA. (PDF, 8 pages)

  13. Butler, Ricky W., Miller; Steven P., Potts, James N.; and Carreno, Victor A.: A Formal Methods Approach to the Analysis of Mode Confusion, 17th Digital Avionics Systems Conference, Bellevue, Washington, October 31--November 6, 1998. (PostScript or PDF, 8 pages)

  14. Ricky W. Butler, Kelly J. Hayhurst and Sally C. Johnson, A Note About HARP's State Trimming Methods, NASA/TM-1998-208427, May 1998. (PDF, 21 pages)

  15. Butler, Ricky W. and Sjogren, Jon A.: A PVS Graph Theory Library, NASA Technical Memorandum 1998-206923, NASA Langley Research Center, Hampton, Virginia, Feb 1998. 24 pages)

  16. Butler, Ricky W.; Miner, Paul S.; Srivas, Mandayam K.; Greve, Dave A.; and Miller, Steven P.: A Bitvectors Library For PVS, Aug 1996, NASA TM-110274.

  17. Butler, Ricky W. An Introduction to Requirements Capture Using PVS: Specification of a Simple Autopilot. NASA Technical Memorandum 111025, NASA Langley Research Center, Hampton, Virginia, May 1996. 32 pages, 257246 bytes)

  18. Holloway, C. Michael; Butler, Ricky W.: Impediments to Industrial Use of Formal Methods, in IEEE Computer, April 1996, pp. 25-26.

  19. Butler, Ricky W.; and Johnson, Sally C.: Techniques for Modeling the Reliability of Fault-Tolerant Systems Using the Markov State-Space Approach, NASA RP-1348, Sept 1995. (PostScript, 112 pages, 1115955 bytes)

  20. Butler, Ricky W.; Di Vito, Ben L.; and Holloway C. Michael: 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. (PostScript, 112 pages, 1115955 bytes)

  21. Butler, Ricky W.; Caldwell, James L.; Carreno, Victor A.; Holloway, C. Michael; Miner, Paul S.; and Vito, Ben L. Di: NASA Langley's Research and Technology Transfer Program in Formal Methods. In Tenth Annual Conference on Computer Assurance (COMPASS 95), Gaithersburg, MD, June 1995. (PostScript, 15 pages; updated version PostScript, 37 pages)

  22. Divito, Benedetto L.; and Butler, Ricky W.: Formal Techniques for Synchronized Fault-Tolerant Systems. In Dependable Computing and Faul-Tolerant Systems, Vol. 8, C. E. Landwehr, B. Randell, L. Simoncini, eds., 1993, p. 163-188. (Book) PostScript, 12 pages)

  23. Butler, Ricky W.; and Johnson, Sally C.: Formal Methods for Formal Methods For Life-Critical Software. In Computing in Aerospace 9 Conference , pages 319-329, San Diego, California, October 1993.

  24. Butler, Ricky W.: 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. (PostScript, 62 pages, 291921 bytes)

  25. Butler, Ricky W.; and Finelli, George B.: The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software. IEEE Transactions on Software Engineering, 19(1):3-12, January 1993. ( PDF , 11 pages)

  26. Di Vito, Benedetto L.; Butler, Ricky W.; and Caldwell, James L.: High Level Design Proof of a Reliable Computing Platform. In Dependable Computing for Critical Applications 2, J. F. Meyer and R. D. Schlichting, eds., p. 279-306, 1992. (PostScript, 12 pages)

  27. Di Vito, Benedetto L.; and Butler, Ricky W.: 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. (PostScript, 13 pages, 222753 bytes)

  28. Di Vito Benedetto L.; Butler, Ricky W.; and Caldwell, James L.: 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. (PostScript, 13 pages, 209527 bytes)

  29. Di Vito, Benedetto L.; and Butler, Ricky W.: Provable Transient Recovery for Frame-Based, Fault-Tolerant Computing Systems. In Real-Time Systems Symposium, Phoenix, Arizona, December 1992. ( PostScript, 4 pages, 103167 bytes)

  30. Johnson, Sally C.; Holloway, C. Michael; Butler, Ricky W.: Second NASA Formal Methods Workshop 1992. NASA Conference Publication 10110, NASA Langley Research Center, Hampton, Virginia, November 1992.

  31. Johnson, Sally C.; and Butler, Ricky W.: A Table-Oriented Interface for Reliability Modeling of Fault-Tolerant Architectures. Presented at the 11th Digital Avionics Systems Conference, Seattle, WA, October 5-8, 1992. In Proceedings, pg. 149-154.

  32. Butler, Ricky W.: The SURE Approach to Reliability Analysis. IEEE Transactions on Reliability, Vol. 41, No. 2, p. 210-218, June 1992. (Program available here.)

  33. Johnson, Sally C.; and Butler, Ricky W.: Design for Validation. IEEE Aerospace Electronic Systems, January 1992, Vol. 7, No. 1, p. 38-43 (PostScript, 6 pages)

  34. Butler, Ricky W.; and Di Vito, Ben L.: 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. (PostScript, 68 pages, 524562 bytes)

  35. Johnson, Sally C.; and Butler, Ricky W.: 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, 6 pages, 113097 bytes)

  36. Butler, Ricky W. and Sjogren, Jon A.: Formal Design Verification of Digital Circuitry. Reliability Engineering and System Safety, Vol. 32, p. 67-93, 1991.

  37. Butler, Ricky W.; and Finelli, George B.: The Infeasibility of Experimental Quantification of Life-Critical Software Reliability. Presented at the ACM SIGSOFT '91 Conference on Software for Critical Systems, New Orleans, LA, December 4-6, 1991. In Proceedings, Vol. 16, No. 5, p. 66-76.

  38. Butler, Ricky W.: NASA Langley's Research Program in Formal Methods. Presented at the IEEE Sixth Annual Conference on Computer Assurance Systems Integrity, Software Safety, and Process Security (COMPASS '91), Gaithersburg, MD, June 25-27, 1991.

  39. Butler, Ricky W.; Caldwell, James L.; and Di Vito, Ben L.: Design Strategy for a Formally Verified Reliable Computing Platform. Presented at the IEEE Sixth Annual Conference on Computer Assurance Systems Integrity, Software Safety, and Process Security (COMPASS '91), Gaithersburg, MD, June 25-27, 1991. In Proceedings, p. 125-133. (PostScript)

  40. Butler, Ricky W. (Ed.): NASA Formal Methods Workshop 1990. NASA CP-10052, November 1990.

  41. Ramanathan, P.; Shin, K. G.; and Butler, Ricky W.: Fault-Tolerant Clock Synchronization in Distributed Systems. IEEE Computer, October 1990, Vol. 23, No. 10, p. 33-42.

  42. Di Vito, Ben L.; Butler, Ricky W.; and Caldwell, James L.: 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. (PostScript, 68 pages, 461037 bytes)

  43. Caldwell, James L., II; Butler, Ricky W.; and Di Vito, Ben L.: Hierarchical Approach to Specification and Verification of Fault-Tolerant Operating Systems. Presented at the Workshop on Software Tools for Distributed Intelligent Control Systems, Pacifica, CA, July 17-19, 1990, Pacifica, CA. In Proceedings.

  44. Butler, Ricky W.; and Johnson, Sally C.: The Art of Fault-Tolerant System Reliability Modeling. NASA TM-102623, March 1990.

  45. Butler, Ricky W.; and Martensen, Anna L.: The Fault-Tree Compiler (FTC) Program and Mathematics. NASA TP-2915, July 1989. (Program available here.)

  46. Butler, Ricky W.; and Sjogren, Jon A.: Hardware Proofs Using EHDM and the RSRE Verification Methodology. NASA Technical Memorandum 100669, NASA Langley Research Center, Hampton, Virginia, December 1988.

  47. Butler, Ricky W.: Fault-Tolerant Clock Synchronization Techniques for Avionics Systems. Presented at the AIAA/AHS/ASEE Aircraft Design and Operations Meeting, Atlanta, GA, September 7-9, 1988. AIAA Paper No. 88-4408.

  48. Butler, Ricky W.; and White, Allan L.: SURE Reliability Analysis Program and Mathematics. NASA TP-2764, March 1988. (Program available here.)

  49. Butler, Ricky W.; and Stevenson, Phillip H.: The Paws and Stem Reliability Analysis Programs, NASA TM-100572, March 1988. (Program available here.)

  50. Butler, Ricky W.: A Survey of Provably Correct Fault-Tolerant Clock Synchronization Techniques, NASA TM-100553, February 1988.

  51. Johnson, Sally C.; and Butler, Ricky W.: Automated Generation of Reliability Models. Presented at the ASME, ASQC, et al., 1988 Annual Reliability and Maintainability Symposium, Los Angeles, CA, January 26-28, 1988. In Proceedings, p. 17-22.

  52. Butler, Ricky W.; Palumbo, Daniel L.; and Johnson, Sally C.: Fault-Tolerant Clock Synchronization Validation Methodology. Journal of Guidance, Control, and Dynamics, Vol. 10, No. 6, p. 513-522, November-December 1987.

  53. Ellis, Erik L.; and Butler, Ricky W.: Estimating the Distribution of Fault Latency in a Digital Processor. NASA TM-100521, November 1987.

  54. Butler, Ricky W.; and Elks, Carl R.: A Preliminary Transient-Fault Experiment on the SIFT Computer System. NASA TM-89058, February 1987.

  55. Martensen, Anna L.; and Butler, Ricky W.: The Fault-Tree Compiler. NASA TM-89098, January 1987.

  56. Butler, Ricky W.: An Abstract Language for Specification of Markov Reliability Models. IEEE Transactions on Reliability, Vol. R-35, No. 5, p. 595-601, December 1986. (Program available here.)

  57. Butler, Ricky W.: The SURE Reliability Analysis Program. Presented at the AIAA Guidance, Navigation and Control Conference, Williamsburg, VA, August 18-20, 1986. AIAA Paper No. 86-2034-CP. (Program available here.)

  58. Palumbo, Daniel L.; and Butler, Ricky W.: A Performance Evaluation of the Software-Implemented Fault-Tolerance Computer. Journal of Guidance, Control, and Dynamics, Vol. 9, No. 2, p. 175-180, March-April 1986.

  59. Butler, Ricky W.: The SURE Reliability Analysis Program. NASA TM-87593, February 1986.

  60. Krishna, C. M.; Shin, K. G.; and Butler, Ricky W.: Ensuring Fault-Tolerance of Phased-Locked Clocks. IEEE Transactions on Computers, Vol. C-34, p. 752-756, August 1985.

  61. Butler, Ricky W.; Palumbo, Daniel L.; and Johnson, Sally C.: Application of a Clock Synchronization Validation Methodology to the SIFT Computer System. Presented at the IEEE Fifteenth International Symposium on Fault-Tolerant Computing, Ann Arbor, MI, June 19-21, 1985. IEEE Paper No. 64.

  62. Palumbo, Daniel L.; and Butler, Ricky W.: Measurement of SIFT Operating System Overhead. NASA TM-86322, April 1985.

  63. Butler, Ricky W.: An Abstract Specification Language for Markov Reliability Models. NASA TM-86423, April 1985. (Program available here.)

  64. Johnson, Sally C.; and Butler, Ricky W.: Validation of a Fault-Tolerant Clock Synchronization System. Presented at the AIAA/IEEE 6th Digital Avionics Systems Conference, Baltimore, MD, December 3-6. 1984. AIAA Paper No. 84-2648-CP.

  65. Butler, Ricky W.; and Johnson, Sally C.: Validation of a Fault-Tolerant Clock Synchronization System. NASA TP-2346, September 1984.

  66. Butler, Ricky W.: The Semi-Markov Unreliability Range Evaluator (SURE) Program. NASA TM-86261, July 1984.

  67. Krishna, C. M.; Shin, K. G.; and Butler, Ricky W.: Synchronization and Fault-Masking in Redundant Real-Time Systems presented by Butler at the Fourteenth International Conference on Fault-Tolerant Computing, Kissimmee, FL, June 20-22, 1984. In Proceedings, p. 152-157.

  68. Butler, Ricky W.: Critical Issues in Real-Time Operating Systems. Presented at the IEEE 1983 Real-Time Systems Symposium, Arlington, VA, December 7, 1983.

  69. Palumbo, Daniel L.; and Butler, Ricky W.: SIFT - A Preliminary Evaluation. Presented at the IEEE/AIAA 5th Digital Avionics Systems Conference, Seattle, WA, October 31-November 3, 1983. IEEE/AIAA Paper No. 21.4.

  70. Butler, Ricky W.: Fault-Tolerant Operating Systems Research in AIRLAB. Presented at the IEEE Computer Society Workshop on Laboratories for Reliable Systems Research, Hampton, VA, April 27-29, 1983.

  71. Butler, Ricky W.: An Assessment of the Real-Time Application Capabilities of the SIFT Computer System. Presented at the General Electric Company Second Annual Reliable and Fault-Tolerant System Seminar, Charlottesville, VA, April 20, 1983. (Available as NASA TM-84482).

  72. Butler, Ricky W.: An Assessment of the Real-Time Application Capabilities of the SIFT Computer System. NASA TM-84482, April 1982.

 

   
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 20 March 2002 (08:44:49)