Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Runtime Monitoring <s> Techniques for efficiently evaluating future time Linear Temporal Logic (abbreviated LTL) formulae on finite execution traces are presented. While the standard models of LTL are infinite traces, finite traces appear naturally when testing and/or monitoring real applications that only run for limited time periods. A finite trace variant of LTL is formally defined, together with an immediate executable semantics which turns out to be quite inefficient if used directly, via rewriting, as a monitoring procedure. Then three algorithms are investigated. First, a simple synthesis algorithm for monitors based on dynamic programming is presented; despite the efficiency of the generated monitors, they unfortunately need to analyze the trace backwards, thus making them unusable in most practical situations. To circumvent this problem, two rewriting-based practical algorithms are further investigated, one using rewriting directly as a means for online monitoring, and the other using rewriting to generate automata-like monitors, called binary transition tree finite state machines (and abbreviated BTT-FSMs). Both rewriting algorithms are implemented in Maude, an executable specification language based on a very efficient implementation of term rewriting. The first rewriting algorithm essentially consists of a set of equations establishing an executable semantics of LTL, using a simple formula transforming approach. This algorithm is further improved to build automata on-the-fly via caching and reuse of rewrites (called memoization), resulting in a very efficient and small Maude program that can be used to monitor program executions. The second rewriting algorithm builds on the first one and synthesizes provably minimal BTT-FSMs from LTL formulae, which can then be used to analyze execution traces online without the need for a rewriting system. The presented work is part of an ambitious runtime verification and monitoring project at NASA Ames, called PathExplorer, and demonstrates that rewriting can be a tractable and attractive means for experimenting and implementing logics for program monitoring. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Runtime Monitoring <s> This paper presents a formal specification-based software monitoring approach that can dynamically and continuously monitor the behaviors of a target system and explicitly recognize undesirable behaviors in the implementation with respect to its formal specification. The key idea of our approach is in building a monitoring module that connects a specification animator with a program debugger. The requirements information about expected dynamic behaviors of the target system are gathered from the formal specification animator, while the actual behaviors of concrete implementations of the target system are obtained through the program debugger. Based on the information obtained from both sides, the judgement on the conformance of the concrete implementation with respect to the formal specification is made timely while the target system is running. Furthermore, the proposed formal specification-based software monitoring technique does not embed any instrumentation codes to the target system nor does it annotate the target system with any formal specifications. It can detect implementation errors in a real-time manner, and help the developers and users of the system to react to the problems before critical failure occurs. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Runtime Monitoring <s> Correct functioning of cyber-physical systems is of critical importance. This is more so in the case of safety critical systems such as in medical, automotive and many other applications. Since verification of correctness, in general, is infeasible and testing is not exhaustive, it is of critical importance to monitor such system during their operation and detect erroneous behaviors to be acted on. A distinguishing property of cyber-physical systems is that they are described by a mixture of integer-valued and real-valued variables. As a result, approaches that assume countable number of states are not applicable for runtime monitoring of such systems. This paper proposes a formalism, called Extended Hidden Markov systems, for specifying behavior of systems with such hybrid state. Using measure theory, it exactly characterizes when such systems are monitorable with respect to a given property. It also presents monitoring algorithms and experimental results showing their effectiveness. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Runtime Monitoring <s> Verification of component-based systems still suffers from limitations such as state space explosion since a large number of different components may interact in an heterogeneous environment. Those limitations entail the need for complementary verification methods such as runtime verification based on dynamic analysis and prone to scalability. In this paper, we integrate runtime verification into the BIP (Behavior, Interaction, and Priority) framework. BIP is a powerful component-based framework for the construction of heterogeneous systems. Our method augments BIP systems with monitors checking a user-provided specification. This method has been implemented in RV-BIP, a prototype tool that we used to validate the whole approach on a robotic application. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Runtime Monitoring <s> We present ROSRV, a runtime verification framework for robotic applications on top of the Robot Operating System (ROS [8]), a widely used open-source framework for robot software development. ROSRV aims to address the safety and security issues of robots by providing a transparent monitoring infrastructure that intercepts and monitors the commands and messages passing through the system. Safety and security properties can be defined in a formal specification language, and are ensured by automatically generated monitors. ROSRV integrates seamlessly with ROS—no change in ROS nor the application code is needed. ROSRV has been applied and evaluated on a commercial robot. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Runtime Monitoring <s> Runtime monitoring is a versatile technique for detecting property violations in safety-critical (SC) systems. Although instrumentation of the system under monitoring is a common approach for obtaining the events relevant for checking the desired properties, the current trend of using black-box commercial-off-the-shelf components in SC system development makes these systems unamenable to instrumentation. In this paper we develop an online runtime monitoring approach targeting an autonomous research vehicle (ARV) system and recount our experience with it. To avoid instrumentation we passively monitor the target system by generating atomic propositions from the observed network state. We then develop an efficient runtime monitoring algorithm, EgMon, that eagerly checks for violations of desired properties written in future-bounded, propositional metric temporal logic. We show the efficacy of EgMon by implementing and empirically evaluating it against logs obtained from the testing of an ARV system. EgMon was able to detect violations of several safety requirements. <s> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Runtime Monitoring <s> There is an increasing necessity to deploy autonomous systems in highly heterogeneous, dynamic environments, e.g. service robots in hospitals or autonomous cars on highways. Due to the uncertainty in these environments, the verification results obtained with respect to the system and environment models at design-time might not be transferable to the system behavior at run time. For autonomous systems operating in dynamic environments, safety of motion and collision avoidance are critical requirements. With regard to these requirements, Macek et al. [6] define the passive safety property, which requires that no collision can occur while the autonomous system is moving. To verify this property, we adopt a two phase process which combines static verification methods, used at design time, with dynamic ones, used at run time. In the design phase, we exploit UPPAAL to formalize the autonomous system and its environment as timed automata and the safety property as TCTL formula and to verify the correctness of these models with respect to this property. For the runtime phase, we build a monitor to check whether the assumptions made at design time are also correct at run time. If the current system observations of the environment do not correspond to the initial system assumptions, the monitor sends feedback to the system and the system enters a passive safe state. <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Runtime Monitoring <s> This article answers fundamental safety questions for ground robot navigation: under which circumstances does which control decision make a ground robot safely avoid obstacles? Unsurprisingly, the answer depends on the exact formulation of the safety objective, as well as the physical capabilities and limitations of the robot and the obstacles. Because uncertainties about the exact future behavior of a robot’s environment make this a challenging problem, we formally verify corresponding controllers and provide rigorous safety proofs justifying why the robots can never collide with the obstacle in the respective physical model. To account for ground robots in which different physical phenomena are important, we analyze a series of increasingly strong properties of controllers for increasingly rich dynamics and identify the impact that the additional model parameters have on the required safety margins. We analyze and formally verify: (i) static safety, which ensures that no collisions can happen with stationary obstacles; (ii) passive safety, which ensures that no collisions can happen with stationary or moving obstacles while the robot moves; (iii) the stronger passive-friendly safety, in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well; and (iv) passive orientation safety, which allows for imperfect sensor coverage of the robot, i.e., the robot is aware that not everything in its environment will be visible. We formally prove that safety can be guaranteed despite sensor uncertainty and actuator perturbation. We complement these provably correct safety properties with liveness properties: we prove that provably safe motion is flexible enough to let the robot navigate waypoints and pass intersections. To account for the mixed influence of discrete control decisions and the continuous physical motion of the ground robot, we develop corresponding hybrid system models and use differential dynamic logic theorem-proving techniques to formally verify their correctness. Since these models identify a broad range of conditions under which control decisions are provably safe, our results apply to any control algorithm for ground robots with the same dynamics. As a demonstration, we also synthesize provably correct runtime monitor conditions that check the compliance of any control algorithm with the verified control decisions. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Runtime Monitoring <s> When applying formal verification to a system that interacts with the real world we must use a model of the environment. This model represents an abstraction of the actual environment, but is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well-behaved. A solution to this problem consists in exploiting the model of the environment for statically verifying the system's behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The paper reports on a demonstration of the feasibility of this approach using the Agent Java PathFinder model checker. Trace expressions are used to model the environment for both static formal verification and runtime verification. <s> BIB009
Runtime monitors can be used to sidestep the problem of verifying a (needfully) complex model of a robotic system. Instead of specifying and verifying the entire system, the properties that the system has to exhibit are extracted and specified as a monitor of the system. Because the monitor is simpler than the system, it is often easier to verify. Another advantage is that runtime monitors can mitigate the problem of the reality gap (between a model and the real world) especially when used to complement offline verification. Given that a robotic system is naturally cyber-physical, and therefore malfunctions can have safety consequences, monitoring the system's behavior at runtime can be key to ensuring safe operation BIB003 . A monitor consumes events from a system and compares them to the expected behavior. If the system's events differ from the expectation, then it can invoke mitigating activities, including logging, flagging this to the user, or triggering behavior to remedy the situation. Runtime monitoring cannot guarantee all system behaviors beforehand. It has received attention in the literature on runtime verification, which brings together model-checking and stream-processing technologies BIB001 . Examples include BIB004 BIB005  , and the International Conference on Runtime Verification has been running since 2006. Aniculaesei et al. BIB007 use runtime monitors to complement design-time formal methods. The runtime monitors are built to check that design-time assumptions hold during the execution of the program. For additional confidence at design time, they also specify the system and its physical environment using TA with safety properties in TCTL. Ferrando et al. BIB009 develop runtime verification to recognize anomalous environmental interactions and so highlight when the previous formal verification that has been carried out on an autonomous robotic system (with some environmental assumptions) becomes invalid. Kane et al. BIB006 present runtime monitors for an autonomous research vehicle. These monitors are written in the αVSL safety specification language, whose semantics is given over timestamped traces using future-bounded, propositional Metric Temporal Logic (MTL). Their algorithm, EgMon, uses the MAUDE rewriting engine to reduce the input formulae. They extend EgMon with a hybrid monitoring algorithm, HMon, which first performs conservative checks and then as many eager checks as the remaining time permits. Often, robotic systems are distributed, either because of the software architecture (such as Robot Operating System (ROS)) or because it is a multirobot system (such as a robot swarm). For such systems, Bauer and Falcone [21] describe a method of distributing an LTL specification of a system's macro-level behavior to a collection of micro-level behavioral monitors. Their approach does not assume any central information collection and ensures that the communication between monitors is minimal, but sufficient to allow the monitors to work. Robotic systems are intrinsically cyber-physical, combining discrete and continuous parts. The implications of this on runtime monitoring are addressed in BIB003 , which describes an approach for modeling the hybrid nature of cyber-physical systems without discretizing them. They use Probabilistic Hybrid Automata (PHA) to capture both the discrete and continuous elements of a system. They illustrate their approach using an electronically controlled train braking system. A similar hybrid-logic approach is taken by BIB008 , who specify the safety properties of a robot rover using dL and then automatically synthesize runtime monitors from these verified models. ROSRV is a runtime verification framework for robotics systems deployed on ROS BIB005 that uses a novel formal specification language for writing safety properties. Using a new configuration file, ROSRV then automatically generates C++ ROS nodes to monitor the system for the specified properties. Because their approach uses normal ROS nodes and a custom configuration file, it doesn't require any changes to be made to either ROS or the application. They make the interesting observation that their approach cannot currently be verified because that "would require a model of ROS itself" to be able to prove that the monitors and other generated code respect the model. Similarly, Falcone et al. BIB004 describe RV-BIP, a tool that produces runtime monitors for robots in the BIP framework, which will be discussed in Section 6.5. They provide a formal description of the BIP component-based framework and monitors. Each monitor consumes events from the BIP system and assesses the sequence of events, producing a verdict of either true, false, or currently true or false. RV-BIP takes an XML description of an LTS, describing the monitor, and produces a BIP monitor for a given BIP system. Falcone et al. provide an example where they use this tool to produce a BIP system with execution order and data freshness monitors. Liang et al. BIB002 describe a runtime monitoring approach that does not require any alterations or additions to the monitored system. They specify the system in Z and compare the traces from a specification animator with information from a Java debugger to check if the running program is correct with respect to the Z specification. This has the added advantage of decoupling the monitor from the monitored program.