Title :
Verification of Plans and Procedures
Author :
Brat, G. ; Gheorghiu, M. ; Giannakopoulou, D. ; Pasareanu, C.
Author_Institution :
USRA/RIACS, NASA Ames Res. Center, Moffett Field, CA
Abstract :
Procedures and plans are used across NASA missions. For example, astronaut activities on the International Space Station are regulated by procedures which are uploaded from the ground. It is critical that these procedures are verified and validated before being executed by astronauts. This paper describes how we are applying advanced formal verification techniques, such as model checking, to plans and procedures expressed in semantically well-defined languages such as PRL and PLEXIL.
Keywords :
aerospace computing; formal verification; NASA missions; PLEXIL; PRL; astronaut activities; formal verification techniques; Automata; Control systems; Government; Humans; International Space Station; NASA; Power system modeling; Safety; Space shuttles; Space technology;
Conference_Titel :
Aerospace Conference, 2008 IEEE
Conference_Location :
Big Sky, MT
Print_ISBN :
978-1-4244-1487-1
Electronic_ISBN :
1095-323X
DOI :
10.1109/AERO.2008.4526574
