Testing Effectiveness:TCAS

### Program Information

Name: Testing Effectiveness:TCAS
Domain: Algorithm
Functionality: TCAS is an implementation of onboard aircraft conflict detection and resolution system.
Input: It accepts twelve input parameters, judges whether there will be a conflict between the current aircraft and the intruder aircraft based on the inputs. Source and follow-up test cases are denoted by $T_s$ and $T_f$ , respectively
Output: Outputs are a kind of manoeuvre the current aircraft should take. TCAS has three types of outputs: 0 represents UNRESOLVED that indicates no manoeuvre, while 1 and 2 represent UPWARD or DOWNWARD manoeuvres, respectively. The test outputs of $T_s$ and $T_f$ are denoted by $O_s$ and $O_f$ , respectively.

#### Reference

 On Testing Effectiveness of Metamorphic Relations: A Case Study https://doi.org/10.1109/SSIRI.2011.21

### MR Information

The next eight relations (MR4-MR11) have an additional prerequisite that includes the following conditions. (1)The TCAS system on the controlled aircraft has a high confidence, and (2)The vertical converging speed is not larger than 600, and (3)The current vertical separation between the two aircrafts at the closest point will be larger than 600 if the controlled aircraft maintains its trajectory, and (4)(i)The intruder aircraft does not have the TCAS system, or (ii.a)the intruder aircraft does not have any intention, and (ii.b)the report describing the presence of any intruder is valid.

#### MR1------

Description:
Property: Given that the intruder aircraft does not have the TCAS system, if $T_s$ and $T_f$ only differ in whether the intruder aircraft has an intention or not, we should have the relation $O_f = O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR2------

Description:
Property: Given that the intruder aircraft does not have the TCAS system, if $T_s$ and $T_f$ only differ in whether the report describing the presence of any intruder is valid or not, we should have the relation $O_f = O_s$ .
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR3------

Description:
Property: Given that the intruder aircraft does not have any intention, and the report describing the presence of any intruder is valid, if $T_s$ and $T_f$ only differ in whether the intruder aircraft has the TCAS system or not, we should have the relation $O_f = O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR4------

Description:
Property: Given that the current altitude of the controlled aircraft is smaller than that of the intruder aircraft, and the vertical separation between two aircrafts will be smaller than the threshold value if the controlled aircraft initiates a downward maneuver, if $T_s$ and $T_f$ differ in the relation between the calculated inhibit biased climb and the vertical separation between two aircrafts where the controlled aircraft initiates a downward maneuver, we should have the relation $O_f \neq O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR5------

Description:
Property: Given that the current altitude of the controlled aircraft is not smaller than that of the intruder aircraft, and the vertical separation between two aircrafts will not be smaller than the threshold value if the controlled aircraft initiates an upward maneuver, if $T_s$ and $T_f$ differ in the relation between the calculated inhibit biased climb and the vertical separation between two aircrafts where the controlled aircraft initiates a downward maneuver, we should have the relation $O_f \neq O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR6------

Description:
Property:  Given that the vertical separation between two aircrafts will be no larger than the calculated inhibit biased climb and smaller than the threshold value if the controlled aircraft initiates an downward maneuver, if $T_s$ and $T_f$ differ in the relation between the current altitudes of the two aircrafts, we should have the relation $O_f \neq O_s$ .
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR7------

Description:
Property:  Given that the vertical separation between two aircrafts will not be smaller than the calculated inhibit biased climb if the controlled aircraft initiates a downward maneuver and not larger than the threshold value if the controlled aircraft initiates an upward maneuver, if $T_s$ and $T_f$ differ in the relation between the current altitudes of the two aircrafts, we should have the relation $O_f \neq O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR8------

Description:
Property: Given that the vertical separation between two aircrafts will be smaller than the threshold value if the controlled aircraft initiates a downward maneuver, if $T_s$ and $T_f$ differ in the relation between the calculated inhibit biased climb and the vertical separation between two aircrafts where the controlled aircraft initiates a downward maneuver, we should have the relation: if $O_s = 0, O_f \in \{0, 1, 2\}$; otherwise, $O_f \neq O_s$ .
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR9------

Description:
Property:  Given that the vertical separation between two aircrafts will not be smaller than the threshold value if the controlled aircraft initiates an upward maneuver, if $T_s$ and $T_f$ differ in the relation between the calculated inhibit biased climb and the vertical separation between two aircrafts where the controlled aircraft initiates a downward maneuver, we should have the relation: if $O_s = 0, O_f \in \{0, 1, 2\}$; otherwise, $O_f \neq O_s$ .
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR10------

Description:
Property: Given that the vertical separation between two aircrafts will be smaller than the threshold value if the controlled aircraft initiates a downward maneuver, if $T_s$ and $T_f$ differ in the relation between the current altitudes of the two aircrafts, we should have the relation: if $O_s = 0, O_f \in \{0, 1, 2\}$; otherwise, $O_f \neq O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR11------

Description:
Property: Given that the vertical separation between two aircrafts will not be smaller than the threshold value if the controlled aircraft initiates an upward maneuver, if $T_s$ and $T_f$ differ in the relation between the current altitudes of the two aircrafts, we should have the relation: if $O_s = 0, O_f \in \{0, 1, 2\}$; otherwise, $O_f \neq O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR12------

Description:
Property: Given that other parameters can be randomly changed, if $T_s$ and $T_f$ differ in whether the TCAS system on the controlled aircraft has a high confidence or not, we should have the relation: if $O_s = 0, O_f \in \{0, 1, 2\}$; otherwise, $O_f \neq O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR13------

Description:
Property: Given that other parameters can be randomly changed, if $T_s$ and $T_f$ differ in whether the vertical converging speed is larger than 600 or not, we should have the relation: if $O_s = 0, O_f \in \{0, 1, 2\}$; otherwise, $O_f \neq O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

#### MR14------

Description:
Property: Given that other parameters can be randomly changed, if $T_s$ and $T_f$ differ in whether the current vertical separation between the two aircrafts at the closest point will be larger than 600 or not where the controlled aircraft maintains its trajectory, we should have the relation: if $O_s = 0, O_f \in \{0, 1, 2\}$; otherwise, $O_f \neq O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:
Insert title here