FM Program: SPIDER

Why is NASA designing SPIDER? The SPIDER project is a research project being conducted for multiple purposes.  SPIDER is providing a testing grounds for the use of Formal Methods in FAA certification. Furthermore, the ROBUS is one of the most advanced communication buses being developed.  It has the capacity to withstand many simultaneous faults. The ROBUS has reintegration services to allow for the reintegration of hardware that is transiently faulty. We hope to show that services such as reintegration are both practical and feasible.

Can I buy a ROBUS system for my x-by-wire application? Although we are prototyping the ROBUS in conjunction with Derivation Systems®, Inc., we are not commercially designing SPIDER systems.

PVS? What's that? The Prototype Verification System (PVS) (free down-load and documentation available at this site) is a theorem-proving system developed by SRI, International. It employs a strongly-typed higher-order predicate logic for the specification language, and a sequent-calculus reasoning system for the proving environment. It is one of the more widely-used theorem provers available. It is used in both research and industry.  Be sure to also download the NASA Langley libraries and strategies.

Are the design specifications for SPIDER available so that I can build one? The design specifications are available!  Please consult the Publications page.

I have a fault-tolerant architecture I'd like to formally verify. Can I look at the SPIDER formal specifications to see how you did it? We have formal specifications and proofs completed in PVS as well as other tools. Consult the Publications page or contact the SPIDER Team.

Is anyone outside of NASA working on SPIDER or SPIDER-related things? Yes. Please see our SPIDER People page to see some of the people who have interests in SPIDER. As well, our Publications page refers to some publications on or mentioning SPIDER written by independent researchers.

I do research related to SPIDER. How can I get involved? The formal and engineering specifications of SPIDER are all freely available. If you would like to learn more about SPIDER, please visit our Publications page. If you have additional questions, please contact the SPIDER Team directly.

I'm an undergraduate/graduate student working in formal methods and/or reliability analysis and/or distributed systems and/or hardware. Do you have internships available?  Sometimes.  Please contact Paul Miner about your interest.

I'd like to work at NASA on SPIDER. How do I do that? Our group, the Formal Methods Group, hires civil servants. The conditions of employment and job postings can be found here. As well, the Formal Methods Group does business with many contractors who sometimes directly or indirectly work with the SPIDER Team.

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