Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Multirobot Systems <s> We present a novel formal verification approach for collective robotic systems that is based on the use of the formal language Klaim and related analysis tools. While existing approaches focus on either micro- or macroscopic views of a system, we model aspects of both the robot hardware and behaviour, as well as relevant aspects of the environment. We illustrate our approach through a robotics scenario, in which three robots cooperate in a decentralized fashion to transport an object to a goal area. We first model the scenario in Klaim. Subsequently, we introduce random aspects to the model by stochastically specifying actions execution time. Unlike other approaches, the specification thus obtained enables quantitative analysis of crucial properties of the system. We validate our approach by comparing the results with those obtained through physics-based simulations. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Multirobot Systems <s> The formal development of multi-agent systems MAS may involve consideration of system functionality at three distinct levels of abstraction. The macro level focusses on the system's overall, global behaviour, independently of how the agents of the system operate and interact. The meso level focusses on agent interactions, and the micro level on the operation of individual agents. While Object-Z with its high-level support for component-based specifications is well suited to modelling MAS at the macro and meso levels, it can become cumbersome at the micro level where the low-level mechanisms required for dealing with asynchronous communication between agents and timing constraints need to be explicitly defined. In this paper we introduce MAZE, an extension of Object-Z supporting i action refinement to facilitate the development process from the macro to micro level, and ii a number of syntactic conventions to facilitate micro-level specification. The syntactic conventions are shorthands for existing Object-Z notation and so require no redefinition of Object-Z's semantics. <s> BIB002
Robotic systems composed of several robots present challenges that must be tackled in addition to those faced when developing single-robot systems. Two broad categories of multirobot systems exist: swarms, where all of the robots exhibit the same behavior, and teams, where the robots may each behave distinctly. In both cases, the behavioral requirements of the system must be considered at both the microscopic level (individual robots) and the macroscopic level (whole system). Multirobot systems can present difficulties for ensuring safety and liveness properties due to the number of concurrent, interacting agents and the changeability of the system's environment  . The work in BIB001 presents a methodology for verifying cooperative robots with distributed control. They use the formal language Klaim, which was designed for distributed systems; its stochastic extension, StoKlaim; and its related tool set. They formalize a specification of the robot's behavior and physical environment, in Klaim, and then add stochastic execution times for actions, in StoKlaim. They validate their modeling approach by comparing their results to those obtained from physics-based simulations of the same system. The case study contains three homogeneous robots, cooperating under distributed control, to transport objects. In this system, the robots have homogeneous behavior but are too few in number to be considered a swarm. One approach to easing multirobot system development formally relates the languages used at the macro-and micro-levels of abstraction. To this end, Smith and Li BIB002 present MAZE, an extension of Object-Z for multiagent systems, which includes Back's action refinement. They describe a top-down refinement-based development process and several shorthand notations to improve robot specification at the micro-level. Next, we discuss the specific challenges faced when developing homogeneous robot systems, specifically swarms (in Section 4.2.1), and heterogeneous robot systems, specifically teams (in Section 4.2.2).