Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> 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> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> FORMALISMS FOR ROBOTIC SYSTEMS <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> BIB002
This section discusses the formalisms found in the literature, following the methodology from Section 1.1, that have been used to specify or verify robotic systems. Table 2 summarizes the categories of formalisms being used to specify both the system and the properties being checked. 2 We explicitly display the formalisms used to specify both the system and the properties because it illustrates the (well-known) links between types of formalism (e.g., state-transition systems and temporal logics); it also highlights potential gaps in the literature or areas to focus on when producing tools. We found that systems were normally specified as state-transition systems and the properties using a logic-typically, a temporal logic. The "Other" category contains those which do not fit in the other categories but are not numerous enough to warrant their own. Examples include the relax BIB001 requirements language and the Quartz language used with the Averest framework  . Table 3 summarizes the wide variety of formal analysis tools that were found using our methodology. Several studies use tools that specify properties in temporal logic (e.g., Uppaal BIB002 , PRISM  , etc.). The number of tools in use for temporal logic is commensurate with their prevalence as illustrated in Table 2 . In this section, we describe the formalisms used to specify and verify robotic systems. Section 5.1 discusses set-based formalisms. Section 5.2 describes approaches using automata. Section 5.3 describes approaches using logics (temporal, dynamic, and others). Section 5.4 discusses process algebras. Section 5.5 outlines ontologies that have been used, and Section 5.6 describes other existing formalisms. Finally, Section 5.7 summarizes.