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.
Constraint solving requires mathematical models of the inputs to the system (code) to stimulate, in the form of constraint programs or optimization programs to solve @cite_1 . Some heuristics are needed to help the solvers, e.g., orders of variables. Search methods are an alternative to solve constraint programs or optimization problems @cite_16 @cite_24 @cite_20 @cite_29 . Nevertheless, heuristics to guide the search are needed, e.g., cost functions. Hybrid systems approaches require the formulation of the test generation problem into a hybrid model (e.g., hybrid automata) @cite_7 @cite_20 , which means a great deal of abstraction and manual input in practice.
@cite_7 @cite_29 @cite_1 @cite_24 @cite_16 @cite_20
2006705367 2160089068 1990733120 2031397756
This paper presents a bounded model checking tool called @math for hybrid systems. It translates a reachability problem of a nonlinear hybrid system into a predicate logic formula involving arithmetic constraints and checks the satisfiability of the formula based on a satisfiability modulo theories method. We tightly integrate (i) an incremental SAT solver to enumerate the possible sets of constraints and (ii) an interval-based solver for hybrid constraint systems (HCSs) to solve the constraints described in the formulas. The HCS solver verifies the occurrence of a discrete change by using a set of boxes to enclose continuous states that may cause the discrete change. We utilize the existence property of a unique solution in the boxes computed by the HCS solver as (i) a proof of the reachability of a model and (ii) a guide in the over-approximation refinement procedure. Our @math implementation successfully handled several examples including those with nonlinear constraints. With ongoing advances in hardware and software, the bottleneck in linear programming is no longer a model solution, it is the correct formulation of large models in the first place. During initial formulation (or modification), a very large model may prove infeasible, but it is often difficult to determine how to correct it. We present a formulation aid which analyzes infeasible LP s and identifies minimal sets of inconsistent constraints from among the perhaps very large set of constraints defining the problem. This information helps to focus the search for a diagnosis of the problem, speeding the repair of the model. We present a series of filtering routines and a final integrated algorithm which guarantees the identification of at least one minimal set of inconsistent constraints. This guarantee is a significant advantage over previous methods. The algorithms are simple, relatively efficient, and easily incorporated into standard LP solvers. Preliminary computational results are reported. INFORMS Journal on Computing , ISSN 1091-9856, was published as ORSA Journal on Computing from 1989 to 1995 under ISSN 0899-1499. Abstract We investigate solution techniques for numerical constraint-satisfaction problems and validated numerical set integration methods for computing reachable sets of nonlinear hybrid dynamical systems in the presence of uncertainty. To use interval simulation tools with higher-dimensional hybrid systems, while assuming large domains for either initial continuous state or model parameter vectors, we need to solve the problem of flow sets intersection in an effective and reliable way. The main idea developed in this paper is first to derive an analytical expression for the boundaries of continuous flows, using interval Taylor methods and techniques for controlling the wrapping effect. Then, the event detection and localization problems underlying flow sets intersection are expressed as numerical constraint-satisfaction problems, which are solved using global search methods based on branch-and-prune algorithms, interval analysis and consistency techniques. The method is illustrated with hybrid systems with uncertain nonlinear continuous dynamics and nonlinear invariants and guards. This paper examines techniques for finding falsifying trajectories of hybrid systems using an approach that we call trajectory splicing. Many formal verification techniques for hybrid systems, including flowpipe construction, can identify plausible abstract counterexamples for property violations. However, there is often a gap between the reported abstract counterexamples and the concrete system trajectories. Our approach starts with a candidate sequence of disconnected trajectory segments, each segment lying inside a discrete mode. However, such disconnected segments do not form concrete violations due to the gaps that exist between the ending state of one segment and the starting state of the subsequent segment. Therefore, trajectory splicing uses local optimization to minimize the gap between these segments, effectively splicing them together to form a concrete trajectory. We demonstrate the use of our approach for falsifying safety properties of hybrid systems using standard optimization techniques. As such, our approach is not restricted to linear systems. We compare our approach with other falsification approaches including uniform random sampling and a robustness guided falsification approach used in the tool S-Taliro. Our preliminary evaluation clearly shows the potential of our approach to search for candidate trajectory segments and use them to find concrete property violations.