Run-time verification of regularly expressed behavioral properties in robotic systems with logic-labeled finite state machines

Abstract

More and more, pre-runtime testing or verification of software in robotic systems is not feasible. For example, autonomous robots using learning behaviors to handle new environments. What sort of software architecture would then enable runtime-verification? We propose that logic-labeled finite-state machines (LLFSMs), jointly with regular expressions are a potent tool to describe acceptable and unacceptable system behaviors. Our architecture has the advantage of expressive power, since sometimes regular expressions are more succinct and comprehensible, while other times, the visual display of the LLFSM would be more accessible to requirements engineers. Moreover, LLFSMs have a prescribed schedule that enables their comprehensive testing and formal verification, and in similar ways, allows monitoring at run-time. The architecture facilitates verification of monitor LLFSMs and higher safety than alternatives such as ROSRV. Moreover, for a subset of LTL (co-safe LTV), LLFSMs can be synthesised from LTL constraints.