header

Program Information

Name: Tcas
Domain: Algorithm
Functionality: A small aircraft conflict avoidance system.
Input: Tcas takes 12 integer parameters, including the altitudes of the controlled aircraft and the intruder aircraft, etc. $Own\_Tracked\_Alt$ and $Other\_Tracked\_Alt$ in the source test case $t_s$ are denoted as $X^1_s$ and $X^2_s$.Define $AVE_s=(X^1_s+X^2_s)/2$. Then, the follow-up test case $t_f$ is constructed by replacing $X^1_s$ and $X^2_s$ in $t_s$ with $X^1_f$ and $X^2_f$ in the following ways, according to the output of $t_s$ (denoted as $O_s$). Suppose Up_Separation and Down_Separation in the source test case $t_s$ are denoted as $Y^1_s$ and $Y^2_s$, respectively. Then, the follow-up test case $t_f$ is constructed by replacing $Y^1_s$ and $Y^2_s$ in $t_s$ with $Y^1_f$ and $Y^2_f$. Let $Z_s$ denote Alt_Layer_Value in $t_s$. Then, the follow-up test case $t_f$ is constructed by replacing $Z_s$ in $t_s$ with $Z_f$.  
Output: It outputs a Resolution Advisory (RA) to advise the pilot to climb (UPWARD), descend (DOWNWARD) or remain the current trajectory (UNRESOLVEDWARD)

Reference

 Metamorphic slice: An application in spectrum-based fault localization https://doi.org/10.1016/j.infsof.2012.08.008;
Generating Source Inputs for Metamorphic Testing Using Dynamic Symbolic Execution https://doi.org/10.1145/2896971.2896980;  

MR Information

MR1------ Modification in Own_Tracked_Altand Other_Tracked_Alt

Description:
Property: (1)If $O_s$ = UPWARD, $X^1_s < X^2_s$, then in $t_f$, set $X^1_f=\textrm{AVE}_s-1$ and $X^2_f=\textrm{AVE}_s+1$, (2)If $O_s$ = DOWNWARD,$X^2_s < X^1_s$, then in $t_f$, set $X^1_f=AVE_s+1$ and $X^2_f=AVE_s-1$, (3)If $O_s$ = UNRESOLVEDWARD,then in $t_f$,set $X^1_f = X^2_f =AVE_s$ Results $\Rightarrow O_s=O_f$  
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

MR2------ Changing TCAS confidence indicator

Description:
Property: For otherwise fixed parameters, let $O_s$ be the output given $TCAS\_has\_high\_confidence = true$ and let $O_f$ be the output given $TCAS\_has\_high\_confidence = false$. Then $O_f = O_s$. 
Source input:  
Source output:  
Follow-up input:  
Follow-up output:  
Input relation:
Output relation:
Pattern:

MR3------ Modification in Alt_Layer_Value

Description:
Property: (1)If $O_s$ = UPWARD, set $Z_f=Z_s+1(0 \leq Z_s < 3)$. (2)If $O_s$ = DOWNWARD, set $Z_f=Z_s - 1(0 < Z_s \leq 3)$ (3)If $O_s$ = UNRESOLVEDWARD,if in $t_s$,Own_Tracked_Alt $\leq$ Other_Tracked_Alt,set $Z_f=Z_s-1(0<Z_s\leq 3)$;otherwise,set $Z_f=Z_s+1(0\leq Z_s <3)$ Results $\Rightarrow O_s=O_f$  
Source input:  
Source output:  
Follow-up input:  
Follow-up output:  
Input relation:
Output relation:
Pattern:

MR4------ Changing parameters randomly

Description:
Property: By randomly changing the parameters values, and $cvs$ = current vertical separation between two aircrafts at the closest point is set to be greater than 600, the following relations should hold: $cvs > 600 \wedge O_s = 0 \Rightarrow O_f \in \{UPWARD,DOWNWARD,UNRESOLVEDWARD\}$ $cvs > 600 \wedge O_s \neq 0 \Rightarrow O_f \neq O_s$
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

MR5------ Changing aircraft's intention

Description:
Property: For otherwise fixed parameters, let $O_s$ be the output given $aircraft\_intent = true$ and let $O_f$ be the output given $aircraft\_intent = false$. Then $O_f = O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

MR6------ Changing the status of reports validity

Description:
Property: For otherwise fixed parameters, let $O_s$ be the output given $reports\_valid = true$ and let $O_f$ be the output given $reports\_valid = false$. Then $O_f = O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:

MR7------ Changing TCAS confidence indicator

Description:
Property: For otherwise fixed parameters, let $O_s$ be the output given $TCAS\_has\_high\_confidence = true$ and let $O_f$ be the output given $TCAS\_has\_high\_confidence = false$. Then $O_f = O_s$.
Source input:
Source output:
Follow-up input:
Follow-up output:
Input relation:
Output relation:
Pattern:
Insert title here