On the run-time verification of autonomy software

The mission-critical and dependability aspects of autonomous systems demand formal level of assurance in ascertaining their mission-survivability capabilities. The complete understanding of system autonomy and its verification and validation (V&V) continue to pose technical challenges. In recent years, formal methods have shown considerable promise in the area of V&V of autonomous systems. In this paper, we further explore the applicability of model checking techniques in run-time verification of autonomy software such as automated planning and scheduling algorithms. We illustrate our proposed approach for run-time verification through a case study of FireSat satellite. We also discuss our experiences and ongoing research activities in this direction.