Dejanira Araiza-Illan

Dejanira Araiza-Illan, Kerstin Eder

This paper examines the verification of stability, a control requirement, over discrete control systems represented as Simulink diagrams, using different model checking approaches and tools. Model checking comprises the (exhaustive) exploration of a model of a system, to determine if a requirement is satisfied. If that is not the case, examples of the requirement's violation within the system's model are provided, as witnesses. These examples are potentially complementary to previous work on automatic theorem proving, when a system is not proven to be stable, but no proof of instability can be provided. We experimentally evaluated the suitability of four model checking approaches to verify stability on a set of benchmarks including linear and nonlinear, controlled and uncontrolled, discrete systems, via Lyapunov's second method or Lyapunov's direct method. Our study included symbolic, bounded, statistical and hybrid model checking, through the open-source tools NuSMV, UCLID, S-TaLiRo and SpaceEx, respectively. Our experiments and results provide an insight on the strengths and limitations of these model checking approaches for the verification of control requirements for discrete systems at Simulink level. We found that statistical model checking with S-TaLiRo is the most suitable option to complement our previous work on automatic theorem proving.

Satragni Sarkar, Dejanira Araiza-Illan, Kerstin Eder

To design trustworthy robots, we need to understand the impact factors of trust: people's attitudes, experience, and characteristics; the robot's physical design, reliability, and performance; a task's specification and the circumstances under which it is to be performed, e.g. at leisure or under time pressure. As robots are used for a wide variety of tasks and applications, robot designers ought to be provided with evidence and guidance, to inform their decisions to achieve safe, trustworthy and efficient human-robot interactions. In this work, the impact factors of trust in a collaborative manufacturing scenario are studied by conducting an experiment with a real robot and participants where a physical object was assembled and then disassembled. Objective and subjective measures were employed to evaluate the development of trust, under faulty and non-faulty robot conditions, and the effect of previous experience with robots, and personality traits. Our findings highlight differences when compared to other, more social, scenarios with robotic assistants (such as a home care assistant), in that the condition (faulty or not) does not have a significant impact on the human's perception of the robot in terms of human-likeliness, likeability, trustworthiness, and even competence. However, personality and previous experience do have an effect on how the robot is perceived by participants, even though that is relatively small.

Dejanira Araiza-Illan, Anthony G. Pipe, Kerstin Eder

Robotic code needs to be verified to ensure its safety and functional correctness, especially when the robot is interacting with people. Testing real code in simulation is a viable option. However, generating tests that cover rare scenarios, as well as exercising most of the code, is a challenge amplified by the complexity of the interactions between the environment and the software. Model-based test generation methods can automate otherwise manual processes and facilitate reaching rare scenarios during testing. In this paper, we compare using Belief-Desire-Intention (BDI) agents as models for test generation with more conventional automata-based techniques that exploit model checking, in terms of practicality, performance, transferability to different scenarios, and exploration (`coverage'), through two case studies: a cooperative manufacturing task, and a home care scenario. The results highlight the advantages of using BDI agents for test generation. BDI agents naturally emulate the agency present in Human-Robot Interactions (HRIs), and are thus more expressive than automata. The performance of the BDI-based test generation is at least as high, and the achieved coverage is higher or equivalent, compared to test generation based on model checking automata.

Jeremy Morse, Dejanira Araiza-Illan, Jonathan Lawry et al.

The widespread adoption of autonomous systems depends on providing guarantees of safety and functional correctness, at both design time and runtime. Information about the extent to which functional requirements can be met in combination with non-functional requirements (NFRs) -- i.e. requirements that can be partially complied with -- , under dynamic and uncertain environments, provides opportunities to enhance the safety and functional correctness of systems at design time. We present a technique to formally define system attributes that can change or be changed to deal with dynamic and uncertain environments (denominated weakened specifications) as a partially ordered lattice, and to automatically explore the system under different specifications, using probabilistic model checking, to find the likelihood of satisfying a requirement. The resulting probabilities form boundaries of "optimal specifications", analogous to Pareto frontiers in multi-objective optimization, informing the designer about the system's capabilities, such as resilience or robustness, when changing its attributes to deal with dynamic and uncertain environments. We illustrate the proposed technique through a domestic robotic assistant example.

Dejanira Araiza-Illan, Tony Pipe, Kerstin Eder

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.

Dejanira Araiza-Illan, David Western, Anthony Pipe et al.

Collaborative robots could transform several industries, such as manufacturing and healthcare, but they present a significant challenge to verification. The complex nature of their working environment necessitates testing in realistic detail under a broad range of circumstances. We propose the use of Coverage-Driven Verification (CDV) to meet this challenge. By automating the simulation-based testing process as far as possible, CDV provides an efficient route to coverage closure. We discuss the need, practical considerations, and potential benefits of transferring this approach from microelectronic design verification to the field of human-robot interaction. We demonstrate the validity and feasibility of the proposed approach by constructing a custom CDV testbench and applying it to the verification of an object handover task.

Dejanira Araiza-Illan, Kerstin Eder, Arthur Richards

This paper presents the verification of control systems implemented in Simulink. The goal is to ensure that high-level requirements on control performance, like stability, are satisfied by the Simulink diagram. A two stage process is proposed. First, the high-level requirements are decomposed into specific parametrized sub-requirements and implemented as assertions in Simulink. Second, the verification takes place. On one hand, the sub-requirements are verified through assertion checks in simulation. On the other hand, according to their scope, some of the sub-requirements are verified through assertion checks in simulation, and others via automatic theorem proving over an ideal mathematical model of the diagram. We compare performing only assertion checks against the use of theorem proving, to highlight the advantages of the latter. Theorem proving performs verification by computing a mathematical proof symbolically, covering the entire state space of the variables. An automatic translation tool from Simulink to the language of the theorem proving tool Why3 is also presented. The paper demonstrates our approach by verifying the stability of a simple discrete linear system.

Laura Antuña, Dejanira Araiza-Illan, Sérgio Campos et al.

The emergent global behaviours of robotic swarms are important to achieve their navigation task goals. These emergent behaviours can be verified to assess their correctness, through techniques like model checking. Model checking exhaustively explores all possible behaviours, based on a discrete model of the system, such as a swarm in a grid. A common problem in model checking is the state-space explosion that arises when the states of the model are numerous. We propose a novel implementation of symmetry reduction, in the form of encoding navigation algorithms relatively with respect to a reference, based on the symmetrical properties of swarms in grids. We applied the relative encoding to a swarm navigation algorithm, Alpha, modelled for the NuSMV model checker. A comparison of the state-space and verification results with an absolute (or global) and a relative encoding of the Alpha algorithm highlights the advantages of our approach, allowing model checking larger grid sizes and number of robots, and consequently, verifying more complex emergent behaviours. For example, a property was verified for a grid with 3 robots and a maximum allowed size of 8x8 cells in a global encoding, whereas this size was increased to 16x16 using a relative encoding. Also, the time to verify a property for a swarm of 3 robots in a 6x6 grid was reduced from almost 10 hours to only 7 minutes. Our approach is transferable to other swarm navigation algorithms.