Title: 	Formal verification of the NASA SPIDER start-up protocol: 
	an automata theoretic approach

Speaker: 	Shinya Umeno

Place: 	32-G531
Time: 	1-2:30pm
Date: 	Friday, October 19, 2007

Abstract: We present a case study of an automata theoretic
formal verification approach for the NASA SPIDER
fault-tolerant architecture. The verification target
is a sub-protocol of the SPIDER, called the start-up
protocol. This sub-protocol is used to establish an
initial time-synchronization between the processes
in the SPIDER.
   We use the Calendar Automata framework to model
the protocol, and then verify properties of the model
as invariants. By using the SAL model-checker, all
inductive properties are verified automatically.
We discuss pros and cons of the automata theoretic
approach used in this case study, and compare the
approach with another verification approach that has
been used for the same case study by the NASA Langley
formal method team.
  This project was conducted during a speaker's summer
internship at NASA Langley research center and National
Institute of Aerospace.