Verification of Plans and Procedures
Guillaume P. Brat, Mihaela Gheorghiu, Dimitra Giannakopoulou, Corina S. Păsăreanu · Proceedings - IEEE Aerospace Conference · 2008
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.