|
|
home >
team >
civil servants >
rwb >
publications
Ricky W. Butler's Publications
-
George E. Hagen, Nelson M. Guerreiro, Jeffrey M. Maddalon, Ricky W. Butler.
An effcient Universal Trajectory Language, NASA/TM-2017-219669, Sept 2017.
-
Guerreiro, Nelson M.; Jones, Denise R.; Barmore, Bryan E.; Butler, Ricky W.; Hagen, George E.; Maddalon, Jeffrey M.; Ahmad, Nash'at N.;
Rogers, Laura J.; Underwood, Matthew C.; Johnson, Sally C.
An Advanced Trajectory-Based Operations
Prototype Tool and Focus Group Evaluation
NASA/TM-2017-219670 Sept 2017.
- Guerreiro, Nelson M., Jones, Denise R., Barmore, Bryan E., Butler, Ricky W., Hagen, George E., Maddalon, Jeffrey M., Ahmad, Nash'at N.
Prototype Tool and Focus Group Evaluation for an Advanced Trajectory-Based Operations Concept,
17th AIAA Aviation Technology, Integration, and Operations Conference, AIAA AVIATION Forum, (AIAA 2017-4096)
-
Hagen, George E., Butler, Ricky W., Maddalon, Jeffrey M.
The Stratway Program for Strategic Conflict Resolution: User's Guide ,
NASA/TM-2016-219196, May 2016.
- Nelson M. Guerreiro, Ricky W. Butler, George E. Hagen, Jeffrey M. Maddalon, and Timothy A. Lewis
Parametric Analysis of Surveillance Quality and Level and
Quality of Intent Information and their Impact on Conflict Detection
Performance, NASA/TM-2016-219177, March 2016.
- Nelson M. Guerreiro, Ricky W. Butler , Jeffrey M. Maddalon , George E. Hagen , and Timothy
A. Lewis, Conflict Detection Performance Analysis For Function Allocation
Using Time-Shifted Recorded Traffic Data, June 22-26, 2015 in Dallas, Texas.
- Aaron Dutle, César Muñoz, Anthony Narkawicz, and
Ricky Butler,
Software Validation via Model Animation, Proceedings of the 9th International Conference on Tests and Proofs (TAP 2015),
Lecture Notes in Computer Science, Vol. 9154, pp. 92-108, 2015
. BibTeX Reference.
-
George E. Hagen and Ricky W. Butler,
Towards a Formal Semantics of Flight Plans
and Trajectories, NASA/TM-2014-218662, Dec 2014.
- Wilfredo Torres-Pomales, Michael M. Madden, Ricky W. Butler, and
Raleigh B. Perry,
Analysis and Simulation of the Simplified
Aircraft-Based Paired Approach Concept With
the ALAS Alerting Algorithm in Conjunction
With Echelon and Offset Strategies
NASA/TM–2014-218151, Jan 2014.
- Ricky W. Butler and Timothy A. Lewis,
A Turn-Projected State-Based Conflict Resolution Algorithm,
Technical Memorandum NASA/TM–2013-218055, November, 2013
- Raleigh B. Perry, Michael M. Madden, Wilfredo Torres-Pomales, Ricky W. Butler.
The Simplified Aircraft-Based Paired Approach With the ALAS Alerting Algorithm,
Technical Memorandum NASA/TM-2013-217804, February, 2013
- Ricky W. Butler, George Hagen, and Jeffrey M. Maddalon,
The Chorus Conflict and Loss of Separation Resolution Algorithms,
Technical Memorandum NASA/TM-2013-218030, August 2013.
- Ricky Butler, George Hagen, Jeffrey Maddalon, César
Muñoz, and Anthony Narkawicz, The search for
effective algorithms for recovery from loss of separation,
Proceedings of the 31st Digital Avionics Systems Conference (DASC 2012),
Williamsburg, Virginia, 2012. BibTeX Reference.
- Hagen, G. E.; Butler, R. W.; and Maddalon, J. M.: Stratway: A
Modular Approach to Strategic Conflict Resolution. Presented at
11th AIAA Aviation Technology, Integration, and Operations (ATIO)
Conference, September 20-22, 2011, Virginia Beach, Virginia.
- César Muñoz, Ricky Butler, Anthony Narkawicz, Jeffrey Maddalon, and George Hagen,
A Criteria Standard for Conflict Resolution: A Vision for Guaranteeing the Safety of Self-Separation in
NextGen,
Technical Memorandum, NASA/TM-2010-216862,
October 2010. BibTeX Reference.
- Ricky W. Butler; George Hagen; Jeffrey M. Maddalon; Cesar A. Munoz; Anthony Narkawicz;
How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project,
Second NASA Formal Methods Symposium
(NFM 2010), Washington D.C., April 13-15, 2010.
- Jeffrey Maddalon, Ricky Butler, Cesar Munoz, Gilles Dowek. A Mathematical Analysis of Conflict Prevention Information. Presented at the 9th Aviation Technology, Integration, and Operations Conference (ATIO), AIAA-2009-6907. Sept 21st, 2009, Hilton Head, SC.
PDF
- Jeffrey Maddalon, Ricky Butler, César Muñoz, and Gilles Dowek, Mathematical Basis for the Safety Analysis of Conflict Prevention
Algorithms, Technical Memorandum, NASA TM-2009-215768, June 2009. BibTex Reference.
- Butler, Ricky W.; Munoz, Cesar A.
Formally Verified Practical Algorithms For Recovery From Loss of Separation ,
NASA TM-2009-215726, June 2009.
- Ricky Butler,
Formalization of the Integral Calculus in the PVS Theorem Prover ,
Journal of Formalized Reasoning, Vol 2, No 1., 2009.
- Butler, Ricky W.; Munoz, Cesar A.
A Formal Framework for the Analysis of Algorithms That Recover From Loss of Separation ,
NASA TM-2008/215356, Oct 2008.
-
Radu Siminiceanu, Ricky W. Butler, César Muñoz.
Experimental Evaluation of a Planning Language Suitable for
Formal Verification",
Model Checking and Artificial Intelligence
5th International Workshop, MoChArt 2008, Patras, Greece, July 21, 2008;
Lecture Notes in Computer Science, Springer Berlin, Volume 5348/2009.
-
Ricky W. Butler, César Muñoz.
NASA Langley's Formal Methods Research in Support of the
Next Generation Air Transportation System
Proceedings of The Sixth NASA Langley Formal Methods Workshop,
June 2008, p.3-5.
- Ricky W. Butler,
A Primer on Architectural Level Fault Tolerance,
NASA TM-2008-215108,
Feb 2008.
- Ricky Butler, Radu Siminiceanu and César Muñoz,
The ANMLite Language and Logic for Specifying Planning Problems,
NASA/TM-2007-215088, Nov 2007.
- 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.
- Ricky Butler and César Muñoz,
An Abstract Plan Preparation Language,
NASA/TM-2006-214518, Nov 2006.
- Ricky Butler,
Formalization of the Integral Calculus in the PVS Theorem Prover
, NASA TM-2004-213279,Oct-2004.
- 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.
- 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.
- 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.
- 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.
- Johnson, Sally C.; and Butler, Ricky W.;: Formal Methods, Chapter 21
in The Avionics Handbook, edited by Cary R. Spitzer, CRC Press, 2001
- 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.
- Butler, Ricky W.,
WinSURE: A New Windows Interface to the SURE
Program , 19th Digital Avionics Systems Conference; Oct 7-13, 2000
Philadelphia, PA.
- 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.
- Ricky W. Butler, Kelly J. Hayhurst and Sally C. Johnson,
A Note About HARP's State Trimming Methods, NASA/TM-1998-208427, May 1998.
- 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)
- 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.
- 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)
- Holloway, C. Michael; Butler, Ricky W.: Impediments to
Industrial Use of Formal Methods, in IEEE Computer, April 1996, pp. 25-26.
- 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. ( 112 pages, 1115955 bytes)
- 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)
- 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)
- 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) 12 pages)
- Butler, Ricky W.; and Johnson, Sally C.:
Formal Methods For Life-Critical Software . In Computing in Aerospace 9
Conference , pages 319-329, San Diego, California, October 1993.
- 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. (
- 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)
- 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)
- 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)
- 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)
- 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)
- 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.
- 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.
- 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.)
- 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)
- 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)
- 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)
- Butler, Ricky W. and Sjogren, Jon A.: Formal Design Verification of
Digital Circuitry. Reliability Engineering and System Safety, Vol. 32, p.
67-93, 1991.
- 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.
- 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.
- 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)
- Butler, Ricky W. (Ed.).
NASA Formal Methods Workshop 1990 . NASA CP-10052,
November 1990.
- 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.
- 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)
- 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.
- Butler, Ricky W.; and Johnson, Sally C.: The Art of Fault-Tolerant System
Reliability Modeling. NASA TM-102623, March 1990.
- Butler, Ricky W.; and Martensen, Anna L.: The Fault-Tree Compiler (FTC)
Program and Mathematics. NASA TP-2915, July 1989. (Program available
here.)
- 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.
- 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.
- Butler, Ricky W.; and White, Allan L.:
SURE Reliability Analysis Program and Mathematics. NASA TP-2764, March 1988. (Program
available here.)
- Butler, Ricky W.; and Stevenson, Phillip H.: The Paws and Stem Reliability
Analysis Programs, NASA TM-100572, March 1988. (Program
available here.)
- Butler, Ricky W.:
A Survey of Provably Correct Fault-Tolerant Clock
Synchronization Techniques, NASA TM-100553, February 1988.
- 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.
- 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.
- Ellis, Erik L.; and Butler, Ricky W.:
Estimating the Distribution of Fault Latency in a Digital Processor. NASA TM-100521, November 1987.
- Butler, Ricky W.; and Elks, Carl R.:
A Preliminary Transient-Fault Experiment on the SIFT Computer System. NASA TM-89058, February 1987.
- Martensen, Anna L.; and Butler, Ricky W.:
The Fault-Tree Compiler. NASA
TM-89098, January 1987.
- 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.)
- 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.)
- 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.
- Butler, Ricky W.: The SURE Reliability Analysis Program. NASA TM-87593,
February 1986.
- 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.
- 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.
- Palumbo, Daniel L.; and Butler, Ricky W.: Measurement of SIFT Operating
System Overhead. NASA TM-86322, April 1985.
- Butler, Ricky W.: An Abstract Specification Language for Markov
Reliability Models. NASA TM-86423, April 1985. (Program
available here.)
- 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.
- Butler, Ricky W.; and Johnson, Sally C.: Validation of a Fault-Tolerant
Clock Synchronization System. NASA TP-2346, September 1984.
- Butler, Ricky W.: The Semi-Markov Unreliability Range Evaluator (SURE)
Program. NASA TM-86261, July 1984.
- 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.
- Butler, Ricky W.: Critical Issues in Real-Time Operating Systems.
Presented at the IEEE 1983 Real-Time Systems Symposium, Arlington, VA,
December 7, 1983.
- 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.
- 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.
- 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).
- Butler, Ricky W.: An Assessment of the Real-Time Application Capabilities
of the SIFT Computer System. NASA TM-84482, April 1982.
|