Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Formalisms for Robotic Systems <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> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Formalisms for Robotic Systems <s> Self-adaptive systems have the capability to autonomously modify their behaviour at run-time in response to changes in their environment. Self-adaptation is particularly necessary for applications that must run continuously, even under adverse conditions and changing requirements; sample domains include automotive systems, telecommunications, and environmental monitoring systems. While a few techniques have been developed to support the monitoring and analysis of requirements for adaptive systems, limited attention has been paid to the actual creation and specification of requirements of self-adaptive systems. As a result, self-adaptivity is often constructed in an ad-hoc manner. In this paper, we argue that a more rigorous treatment of requirements explicitly relating to self-adaptivity is needed and that, in particular, requirements languages for self-adaptive systems should include explicit constructs for specifying and dealing with the uncertainty inherent in self-adaptive systems. We present RELAX, a new requirements language for self-adaptive systems and illustrate it using examples from the smart home domain. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Formalisms for Robotic Systems <s> We present a computational framework for automatic synthesis of control and communication strategies for a robotic team from task specifications given as regular expressions about servicing requests in an environment. Our approach is based on two main ideas. First, we extend recent results from formal synthesis of distributed systems to check for the distributability of the task specification and to generate local specifications, while accounting for the service and communication capabilities of the robots. Second, by using a technique inspired from LTL model checking, we generate individual control and communication strategies. We illustrate the method with experimental results in our Robotic Urban-Like Environment. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Formalisms for Robotic Systems <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> BIB004
This section describes the formalisms currently used in the literature for specifying the behavior of robotic systems. Table 2 summarizes the formalisms found, according to the methodology described in Section 1.1, in use to specify the system and properties to be checked. There were more studies found that specify the system (56) than specify the properties BIB003 . Some systems' specifications are checked for deadlock or reachability, for example,  , whereas some are just used for specification, such as  . Conversely, some of the studies only specify properties and monitor a running system BIB004 BIB001 or describe a framework for dealing with property specification BIB002 . Also, the ontologies found in our literature search are all used to specify systems. State-transition systems are the most numerous for specifying systems and temporal logics the most numerous for specifying properties. This popularity may be explained by the popularity and usability of model checkers for these formalisms; state-transition systems are often used to 