Temporal logic runtime verification of dynamic systems

Abstract

Robotic computer systems are increasingly ubiquitous in everyday life and this has led to a need to develop safe and reliable systems. To ensure safety and reliability of these systems, the following three main verification techniques are usually considered: (1) theorem proving, (2) model checking, and (3) testing. However, the behaviour of robotic systems depends heavily on the environment and changes over time, which makes it hard to predict and analyse prior to their execution. Therefore, this paper provides a novel framework that automatically and verifiably monitors these systems at runtime. The main aim of the framework is to assist the operator through witnesses and counterexamples that are generated during the execution of the system. The framework is suitable for manufacturing and mine operations. In addition, the framework can explicitly capture sensor specifications of the environment and react to the changes accordingly to ensure safe and reliable operation during runtime of the system. The framework first constructs a region automaton of the environment and then represents operation rules in a formal specification language called universal computation tree logic (ACTL). This formal specification language allows the expression of complex desired behaviours, such as collision avoidance in the case of haul truck operations