Robot example

From AadlWiki

Jump to: navigation, search

Contents

Overview

This work consists in mapping an existing system that specifies error and behavior-related specifications in the same model into an AADL model that use the error and behavior annexes. This effort would require to separate the behavior and the error logic.


Baseline work

This work is based on the paper and research work published in:

Toward A Quantitative Method for Assuring Coordinated Autonomy, Sagar Chaki, John M. Dolan, Joseph Andrew Giampapa, Proceedings of the AAMAS Workshop on Autonomous Robots and Multirobot Systems (ARMS'13), May 6-10, 2013, to appear.

Model repository

You can find the AADL model on the following github repository: https://github.com/osate/examples/tree/master/robot


System Overview

The system consists in a robot that traverses a grid. On each part of the grid, there might be a bomb. At each step, the robot move try to detect a bomb and if it finds one try to defuse it. The path followed by the robot is illustrated below.

Also, when moving on the board, the robot perform the following actions (illustrated in the following state machine). For more information, please read the article referenced in the Baseline work.



AADL specifications

The architecture of each robot is decomposed into three different sub-systems, each being dedi-cated for representing one aspect of the system:

  • Behavior aspects: represent the functional behavior of the system (defusing a bomb, marking a place, etc.)
  • Error aspect: capture the different states related to errors
  • Environment aspects: exhibits events related to the occurrence of failures in the envi-ronment (such as failure to defuse a bomb, occurrence of failure for not detecting a bomb)

These blocks are then connected each other to transmit errors occurrences between each layer (behavior error propagation into the error layer, etc.).


Behavior

The state automaton contains the following variables:

  • Current_cell: current cell identifier
  • Ncells: number of cells to inspect
  • Time_counter: current time tick
  • Timeout: constant value for a timeout
  • Failures: number of failures (failures to detect a bomb)
  • T_sense: time to sense (constant)
  • T_defuse1: time to defuse in the easy mode (constant)
  • T_defuse2: time to defuse in the medium mode (constant)
  • T_defuse3: time to defuse in the hard mode (constant)
  • T_mark: time required to mark a bomb (constant)

The system has two output signals to trigger the error model and signal a fault from the behavior:

  • Blown: the robot explodes
  • Timeout: when a timeout occurs

The system also have the following input signals:

  • See_mine: probability that a mine is seen.
  • Explode: probability to explode while detecting
  • P_d1: probability to successfully defuse the mine for the easy defuse scenario
  • P_ed1: probability to have the mine explode while trying to defuse it for the easy defuse scenario
  • P_d2 : probability to successfully defuse the mine for the medium defuse scenario
  • P_ed2 ; probability to have the mine explode while trying to defuse it for the medium defuse scenario
  • P_d3 : probability to successfully defuse the mine for the hard defuse scenario
  • P_ed3 : ; probability to have the mine explode while trying to defuse it for the hard de-fuse scenario
  • P_false_neg: probability that the robot does not detect a bomb while there is one

Each signal is mapped into an AADL event port and is true when its associated probability is true.

The transitions are the following:

  • T1: current_cell < ncells – there are more cells to inspect
  • T2: explode signal is not present and no timeout
  • T3, T4, T7, T9, T11: if time_counter >= timeout, we also send the timeout event
  • T4, T7, T9: if the p_dX (X being the defuse identifier) is not present and p_edX is pre-sent, send the blown signal also.
  • T17, T18, T19: is p_dX is not present and p_edX is not present as well
  • T5, T6, T8: p_dX is present
  • T3:explode signal is present, we send the output signal blown
  • T15: current_cell >= ncells
  • T13: p_false_neg not present
  • T14: p_false_neg present, increment the value of the failure variable


Error

The system has the following input ports:

  • Defuse_fail
  • Timeout

There is the detail of the transitions:

  • T1: occurs when an event is received on timeout
  • T2: occurs when an event is received on defuse_fail
Personal tools