The software of robotic assistants needs to be verified, to ensure its safety and functional correctness. Testing in simulation allows a high degree of realism in the verification. However, generating tests that cover both interesting foreseen and unforeseen scenarios in human-robot interaction (HRI) tasks, while executing most of the code, remains a challenge. We propose the use of belief-desire-intention (BDI) agents in the test environment, to increase the level of realism and human-like stimulation of simulated robots. Artificial intelligence, such as agent theory, can be exploited for more intelligent test generation. An automated testbench was implemented for a simulation in Robot Operating System (ROS) and Gazebo, of a cooperative table assembly task between a humanoid robot and a person. Requirements were verified for this task, and some unexpected design issues were discovered, leading to possible code improvements. Our results highlight the practicality of BDI agents to automatically generate valid and human-like tests to get high code coverage, compared to hand-written directed tests, pseudorandom generation, and other variants of model-based test generation. Also, BDI agents allow the coverage of combined behaviours of the HRI system with more ease than writing temporal logic properties for model checking.
Other model-based approaches seek to test models at the same level of abstraction as the model-based test generation @cite_5 , or they focus on testing high-level functionality @cite_23 @cite_28 @cite_13 . Thus, test generation is much easier to implement than for our testing problem, which targets the real robotics code in HRI realistic scenarios. Our model-based test generation approach is based on divide-and-conquer, simplifying the constraint solving or search problem. This abstract-concrete process has been proposed for the synthesis of hybrid controllers that satisfy properties @cite_17 @cite_27 .
@cite_28 @cite_27 @cite_23 @cite_5 @cite_13 @cite_17
2112398472 1594775721 2107360681 2134312936
This paper proposes a method for automatic generation of time-optimal robot motion trajectories for the task of collecting and moving a finite number of objects to particular spots in space, while maintaining predefined temporal logic constraints. The continuous robot dynamics change upon an object pick-up or drop-off. The temporal constraints are expressed as syntactically co-safe Linear Temporal Logic (scLTL) formulas over the set of object and drop-off sites. We propose an approach based on constructing a discrete abstraction of the hybrid system modeling the robot in the form of a finite weighted transition system. Then, by employing tools from automata-based model checking, we obtain an automaton containing only paths that satisfy the specification. The shortest path in this automaton is found by graph search and corresponds directly to the time-optimal hybrid trajectory. The method is applied to a case study with a mobile ground robot and a case study involving a quadrotor moving in an environment with obstacles, thus reflecting its computational advantage over a direct optimization approach. The use of autonomous systems, including cooperating agents, is indispensable in certain fields of application. Nevertheless, the verification of autonomous systems still represents a challenge due to lack of suitable modelling languages and verification techniques. To address these difficulties, different modelling languages allowing concurrency are compared. Coloured Petri Nets (CPNs) are further analysed and illustrated by means of an example modelling autonomous systems. Finally, some existing structural coverage concepts for Petri Nets are presented and extended by further criteria tailored to the characteristics of CPNs. This chapter presents principles and techniques for modelbased black-box conformance testing of real-time systems using the Uppaal model-checking tool-suite. The basis for testing is given as a network of concurrent timed automata specified by the test engineer. Relativized input output conformance serves as the notion of implementation correctness, essentially timed trace inclusion taking environment assumptions into account. Test cases can be generated offline and later executed, or they can be generated and executed online. For both approaches this chapter discusses how to specify test objectives, derive test sequences, apply these to the system under test, and assign a verdict. Robot motion planning algorithms have focused on low-level reachability goals taking into account robot kinematics, or on high level task planning while ignoring low-level dynamics. In this paper, we present an integrated approach to the design of closed–loop hybrid controllers that guarantee by construction that the resulting continuous robot trajectories satisfy sophisticated specifications expressed in the so–called Linear Temporal Logic. In addition, our framework ensures that the temporal logic specification is satisfied even in the presence of an adversary that may instantaneously reposition the robot within the environment a finite number of times. This is achieved by obtaining a Buchi automaton realization of the temporal logic specification, which supervises a finite family of continuous feedback controllers, ensuring consistency between the discrete plan and the continuous execution.