Runtime Verification of Prediction

Speaker: Stefano Tonetta, Fondazione Bruno Kessler, Italy

Abstract

Runtime verification of predictions is crucial for ensuring the reliability of complex systems, especially in domains like space exploration, where failures can have significant consequences. These systems exhibit typically partial observability especially of the surrounding environment, and this poses significant challenges to the evaluation of properties at runtime. This vision paper proposes a novel methodology for the runtime verification of the precision of predictive functions that are used for planning and control. The problem is motivated by an ongoing project, ExploDTwin, where digital twins are employed for monitoring and planning the activities of space exploration applications, and use simulation and/or AI models to predict related resource consumption. During runtime, only a subset of system variables is observable so that the precision of the prediction cannot be directly checked on the system execution. To address this challenge, we envision a methodology exploiting assumption-based runtime verification and belief state exploration to enumerate variable assignments compatible with the observations, enabling verification of whether the predictions are aligned.