Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Theorem Proving <s> We introduce a first-order dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential actions. For handling real arithmetic during proofs, we lift quantifier elimination to dynamic logic. To obtain a modular combination, we use side deductions for verifying interacting dynamics. With this, our logic supports deductive verification of hybrid systems with symbolic parameters and first-order definable flows. Using our calculus, we prove a parametric inductive safety constraint for speed supervision in a train control system. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Theorem Proving <s> This article deals with the problem of dynamic role-playing in Multi-Agent organisations. The approach presented uses a formal specification notation and is based upon a formal framework which defines the concepts of role, interaction and organisation. Within this framework the problem of dynamic role-playing specification is related to the merging of specifications. The formal notation used composes Object-Z and Statecharts. The main features of this approach are: enough expressive power to represent Multi-Agents dynamic aspects, tools for specification analysis and mechanisms allowing the refinement of a high level specification into a low level specification which can be easily implemented. The last part of this paper presents an application with the specification of a reactive and cooperative MAS model named Satisfaction Altruism. An analysis of the specification validates the agents' behaviours. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Theorem Proving <s> Nowadays, robots interact more frequently with a dynamic environment outside limited manufacturing sites and in close proximity with humans. Thus, safety of motion and obstacle avoidance are vital safety features of such robots. We formally study two safety properties of avoiding both stationary and moving obstacles: (i) passive safety, which ensures that no collisions can happen while the robot moves, and (ii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well. We use hybrid system models and theorem proving techniques that describe and formally verify the robot’s discrete control decisions along with its continuous, physical motion. Moreover, we formally prove that safety can still be guaranteed despite location and actuator uncertainty. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Theorem Proving <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> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Theorem Proving <s> State-machine based notations are ubiquitous in the description of component systems, particularly in the robotic domain. To ensure these systems are safe and predictable, formal verification techniques are important, and can be cost-effective if they are both automated and scalable. In this paper, we present a verification approach for a diagrammatic state machine language that utilises theorem proving and a denotational semantics based on Unifying Theories of Programming (UTP). We provide the necessary theory to underpin state machines (including induction theorems for iterative processes), mechanise an action language for states and transitions, and use these to formalise the semantics. We then describe the verification approach, which supports infinite state systems, and exemplify it with a fully automated deadlock-freedom check. The work has been mechanised in our proof tool, Isabelle/UTP, and so also illustrates the use of UTP to build practical verification tools. <s> BIB005
Theorem proving offers the benefit of producing a formal proof of the correctness of a software system. These formal proofs can be used to provide robust evidence for certification of autonomous robotic systems. A notable example here is the use of Isabelle/HOL and temporal logic to formalize a subset of traffic rules for vehicle overtaking in Germany  . More recently, the RoboChart notation and its associated toolset also makes use of Isabelle/HOL to verify robotic systems BIB005 . Other work in this domain includes BIB003 , which uses the hybrid systems logic dL BIB001 to describe the discrete and continuous navigation behavior of a robot rover. They then use the hybrid theorem prover, KeYmaera, to verify that the robot does not collide with stationary or moving obstacles and maintains sufficient distance from obstacles. Mitsch et al. BIB004 update this work, verifying a less safe property that allows for imperfect sensors; adding liveness proofs, to guarantee progress; and automatically synthesizing runtime monitors from the verified models, to mitigate the problems caused by the reality gap. In BIB002 , OZS (a combination of Object-Z and Statecharts  ) is used to capture the dynamic roles that an agent in a multirobot system can play, which define the robot's interaction patterns. OZS has an operational semantics, and the STeP theorem prover is used for verification of safety and liveness properties of their model. Although effective, it is clear from our analysis that these kinds of approaches have not received much attention in the literature. We believe that this is a usability issue with the tools generally more difficult to master than those of other approaches.