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.
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.
You can find the AADL model on the following github repository: https://github.com/osate/examples/tree/master/robot
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.
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.).
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
The system has the following input ports:
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