Skip past navigation NASA Langley Formal Methods



quick page







home > research > SPIDER > publications

SPIDER Publications






Note: If the title of a publication is a link, then the file is served from an outside
website.  Otherwise, the file is provided after the bibilographic information.

Publications marked with a "*" provide an introductory overview of SPIDER.

SPIDER Prototype and DO-254

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 hereexternal link
  • Lee Pike. Formal Verification of Time-Triggered Systems. PhD Dissertation. Indiana University, May 2006. More Info
  • Lee Pike. external link 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.


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 link to external site tag identifies links that are outside of the NASA domain.

  Skip past navigation  
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Lee Pike
larc privacy statement
last modified: 17 May 2004