SPIDER Publications

SPIDER Prototype and DO-254

• Wilfredo Torres-Pomales, Mahyar R. Malekpour, Paul S. Miner, and Sandra V. Koppen: "Plan for the Characterization of HIRF Effects on a Fault-Tolerant Computer Communication System", NASA Technical Memorandum TM-2008-215306, May 2008, pp. 43.
• Wilfredo Torres-Pomales, Mahyar R. Malekpour, and Paul S. Miner. Design of the Protocol Processor for the ROBUS-2 Communication System. NASA Technical Memorandum TM-2005-213934, Nov 2005.
• 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. pdf
• Paul S. Miner.  SPIDER Research and DO-254 Experiences.  FAA National Software Conference, 2003. pdf
• *Wilfredo Torres. ROBUS2. Assessment Technology Branch Talk, NASA Langley Research Center, August, 2004. pdf
• *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. pdf 
• Paul S. Miner, Victor A. Carreņo, Mahyar Malekpour, and Wilfredo Torres. A Case-Study Application of RTCA DO-254: Design Assurance Guidance for Airborne Electronic Hardware, 19th Digital Avionics Systems Conference, October 2000.
• Paul Miner. Analysis of the SPIDER Fault-Tolerance Protocols.  5th NASA Langley Formal Methods Workshop, 2000.  powerpoint
  

Fault-tolerant Formalizations

• Lee Pike, "Modeling Time-Triggered Protocols and Verifying Their Real-Time Schedules", Formal Methods in Computer Aided Design (FMCAD), 2007. (Winner of FMCAD best paper award) also here
• Lee Pike. Formal Verification of Time-Triggered Systems. PhD Dissertation. Indiana University, May 2006. More Info
• Lee Pike. A note on inconsistent axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms". IEEE Transactions of Software Engineering. Volume 32, Issue 5, pp 347-348, May 2006.
• Lee Pike and Steven D. Johnson. The formal verification of a reintegration protocol. Accepted at the ACM Conference on Embedded Software (EMSOFT), 2005. pdf. Proof files available here
• Lee Pike. Real-time system verification by k-induction. NASA Technical Memorandum TM-2005-213751, 2005. pdf. Proof files available here
• Lee Pike, Paul Miner, Wilfredo Torres. Model Checking Failed Conjectures in Theorem Proving: A Case Study. NASA Technical Memorandum NASA/TM-2004-213278, 2004. pdf. Proof files are available here.
• *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. pdf. Proof files are available here.
• 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.  pdf Proof files are available here.
• Lee Pike. The Formal Verification of the SPIDER Interactive Consistency Protocol.  Internal presentation of work completed while an intern with the Formal Methods Group, August, 2003. power point, open office
• Alfons Geser.  A Fault-Tolerant Diagnosis Protocol.  Talk at NASA Langley ATB, 2003.
• Alfons Geser.  SPIDER--An Ultra-Reliable Communication Architecture.  Informal Presentation at NIA, 2003.
• *Alfons Geser and Paul Miner.  A New On-line Diagnosis Protocol for the SPIDER Family of Byzantine Fault Tolerant Architectures.  NASA TM-212432, December 2004. pdf
• Alfons Geser, Paul Miner.  A Formal Correctness Proof of the SPIDER Diagnosis Protocol.. Theorem-Proving in Higher-Order Logics (TPHOLs), track B, 2002.
• Alfons Geser.  Dependability in the Presence of Diagnosed Faults.  NASA Langley ATB, March 2002.
• Alfons Geser.  Dependable Distributed Defect Diagnosis or Formal Verification of a Fault-Tolerant Diagnosis Protocol.  NASA Langley ATB, May 2002.
• Alfons Geser.  A Formal Correctness Proof of the SPIDER Diagnosis Protocol.  TPHOLs, track B, 2002.
• Alfons Geser.  Formal Verification of the SPIDER Diagnosis Protocol in PVS.  NASA Langley ATB Internal Formal Methods Workshop, 2001.
• Alfons Geser.  SPIDER -- Formally Verified Fault Tolerance.  ICASE Science Council Meeting, 2001.
• Paul S. Miner. Verification of Fault-Tolerant Clock Synchronization Systems. NASA TP-3349, November, 1993.

Self-Stabilization

• Mahyar R. Malekpour, "A Byzantine-Fault Tolerant Self-Stabilizing Protocol for Distributed Clock Synchronization Systems", NASA/TM-2006-214322, August 2006.
• Mahyar R. Malekpour, Radu Siminiceanu. Comments on the Byzantine Self-Stabilizing Pulse Synchronization Protocol: Counterexamples. NASA Technical Memorandum NASA/TM-2006-213951, February 2006.

Other Topics

• Beth Latronico.  Reliability Validation of Group Membership Services for X-by-Wire Protocols. Ph.D dissertation, Carnegie Mellon University, Department of Electrical and Computer Engineering, 2005.  pdf
• Elizabeth Latronico, Paul Miner, and Philip Koopman. Quantifying the Reliability of Proven SPIDER Group Membership Service Guarantees.  Dependable Systems and Networks (DSN), 2004.  pdf
• Elwin C. Ong.  From Anonymity to Ubiquity:  A Study of Our Increasing Reliance on Fault Tolerant Computing.  2003. pdf
• Jeffrey M. Maddalon, Paul S. Miner. An Architectural Concept for Intrusion Tolerance in Air Traffic Networks.  Integrated Communication Navigation and Surveilence (ICNS), Annapolis, Maryland, 2003.  pdf talk pdf
• K. Driscoll, B. Hall, H. Sivencrona, P. Zumsteg.  Byzantine Fault Tolerance, From Theory to Reality.  Proc. 22nd International Conference on Computer Safety, Reliability and Security (SAFECOMP03), pp.235-248, Edinburgh, Scotland, UK, October 2003. pdf
• *John Rushby.  Bus Architectures For Safety-Critical Embedded Systems.  In Edited by Tom Henzinger and Christoph Kirsch: EMSOFT 2001: Proceedings of the First Workshop on Embedded Software, pp. 306--323. Springer-Verlag.  pdf

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