From Livingstone to SMV

To ful ll the needs of its deep space exploration program, NASAis actively supporting research and development in autonomy software. However, the reliable and cost-e ective development and validation of autonomy systems poses a tough challenge. Traditional scenario-based testing methods fall short because of the combinatorial explosion of possible situations to be analyzed, and formal veri cation techniques typically require a tedious, manual modelling by formal method experts. This paper presents the application of formal veri cation techniques in the development of autonomous controllers based on Livingstone, a model-based health-monitoring system that can detect and diagnose anomalies and suggest possible recovery actions. We present a translator that converts the models used by Livingstone into speci cations that can be veri ed with the SMV model checker. The translation frees the Livingstone developer from the tedious conversion of his design to SMV, and isolates him from the tech...

• Type: Conference
• Year: 2000
• Where: FAABS
• Authors: Charles Pecheur, Reid G. Simmons
• Keywords: FAABS 2000, Formal Veri Cation, Intelligent Agents, SMV Model Checker, Veri Cation Techniques