Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficiently Obtaining Reachset Conformance for the Formal Analysis of Robotic Contact Tasks

Chencheng Tang, Matthias Althoff

TL;DR

This work injects non-determinism into the continuous dynamics and the discrete transitions, and optimally identify all model parameters together with the non-determinism required to capture the recorded behaviors.

Abstract

Formal verification of robotic tasks requires a simple yet conformant model of the used robot. We present the first work on generating reachset conformant models for robotic contact tasks considering hybrid (mixed continuous and discrete) dynamics. Reachset conformance requires that the set of reachable outputs of the abstract model encloses all previous measurements to transfer safety properties. Aiming for industrial applications, we describe the system using a simple hybrid automaton with linear dynamics. We inject non-determinism into the continuous dynamics and the discrete transitions, and we optimally identify all model parameters together with the non-determinism required to capture the recorded behaviors. Using two 3-DOF robots, we show that our approach can effectively generate models to capture uncertainties in system behavior and substantially reduce the required testing effort in industrial applications.

Efficiently Obtaining Reachset Conformance for the Formal Analysis of Robotic Contact Tasks

TL;DR

This work injects non-determinism into the continuous dynamics and the discrete transitions, and optimally identify all model parameters together with the non-determinism required to capture the recorded behaviors.

Abstract

Formal verification of robotic tasks requires a simple yet conformant model of the used robot. We present the first work on generating reachset conformant models for robotic contact tasks considering hybrid (mixed continuous and discrete) dynamics. Reachset conformance requires that the set of reachable outputs of the abstract model encloses all previous measurements to transfer safety properties. Aiming for industrial applications, we describe the system using a simple hybrid automaton with linear dynamics. We inject non-determinism into the continuous dynamics and the discrete transitions, and we optimally identify all model parameters together with the non-determinism required to capture the recorded behaviors. Using two 3-DOF robots, we show that our approach can effectively generate models to capture uncertainties in system behavior and substantially reduce the required testing effort in industrial applications.

Paper Structure

This paper contains 14 sections, 18 equations, 7 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries and Problem Statement
  3. Preliminaries
  4. Problem Statement
  5. System Modeling
  6. Synthesizing Reachset Conformant Models
  7. Test Case Processing for Hybrid Systems
  8. Decoupling Discrete States in Conformance Synthesis
  9. Reachset Conformance as Linear Constraints
  10. Evaluating the Costs of Reachable Sets
  11. Experimental Results
  12. Modeling the Normal Working Condition of Robot A
  13. Enclosing Exception Cases and Other Robots with Little Testing Effort
  14. Conclusions

Figures (7)

  • Figure 1: State evolution in a hybrid automaton.
  • Figure 2: The hybrid automaton of the representative scenario. The end effector (blue) is shaped like a sphere whose center locates the tool center point. A force sensor (yellow) measures the external force. A location is represented by a box with the flow function above the dotted line and the invariant below. Guards and reset functions are presented next to the transition arrows.
  • Figure 3: Separating a test case $\mathtt{C}$ by locations into sections. We assume $\bm{y} = \bm{x}$ to simplify the visualization, and we denote the elements of the $s$-th section $\mathtt{S}_{s}$ using the superscript $(s)$.
  • Figure 4: Concept for synthesizing reachset conformant models for robotic contact tasks.
  • Figure 5: Two 3-DOF robots hitting a wood board. The collision force tilts the robot mounting (yellow line) with respect to the board (red line).
  • ...and 2 more figures

Theorems & Definitions (5)

  • Definition 1: Zonotope
  • Definition 2: Hybrid Automaton
  • Definition 3: Reachable Set
  • Definition 4: Test Case
  • Definition 5: Test Case Section