Verification of Intelligent Control Software
Charles Pecheur, Ste Barbe · 2006
Autonomous embedded controllers are seen as a critical technology to enable new mission objectives and scale down operating costs for space applications. However, the validation of intelligent controls software poses a huge challenge, where traditional testing approaches fall short of providing the required level of confidence for such safety-critical applications. This is an overview of recent research in applying modern, analytical verification technologies and tools to the validation of autonomy software, in the context of space applications, at NASA Ames Research Center in California, with a particular focus on model-based approaches to autonomous control, and more specifically fault diagnosis systems. We have developed and experimented with two lines of tools, both related to model checking techniques. Verifying diagnosis systems and models has led to considering the issue of diagnosability, in the sense of checking whether a system provides sufficient observations to determine and track its internal state with sufficient accuracy. We discuss how this kind of question can be reduced to a modified model checking problem. Diagnosability analysis also expands to the domain of epistemic (i.e. knowledge) models and logics. 1