Case study: Applying formal methods to the Traffic Alert and Collision Avoidance System (TCAS) II

Author(s):  
J.J. Britt
2013 ◽  
Vol 2013 ◽  
pp. 1-6 ◽  
Author(s):  
Zhanwei Hui ◽  
Song Huang ◽  
Zhengping Ren ◽  
Yi Yao

For mission critical programs, integer overflow is one of the most dangerous faults. Different testing methods provide several effective ways to detect the defect. However, it is hard to validate the testing outputs, because the oracle of testing is not always available or too expensive to get, unless the program throws an exception obviously. In the present study, the authors conduct a case study, where the authors apply a metamorphic testing (MT) method to detect the integer overflow defect and alleviate the oracle problem in testing critical program of Traffic Collision Avoidance System (TCAS). Experimental results show that, in revealing typical integer mutations, compared with traditional safety property testing method, MT with a novel symbolic metamorphic relation is more effective than the traditional method in some cases.


Author(s):  
Joseph B. Lyons ◽  
Nhut T. Ho ◽  
Kolina S. Koltai ◽  
Gina Masequesmay ◽  
Mark Skoog ◽  
...  

This case study analyzes the factors that influence trust and acceptance among users (in this case, test pilots) of the Air Force’s Automatic Ground Collision Avoidance System. Our analyses revealed that test pilots’ trust depended on a number of factors, including the development of a nuisance-free algorithm, designing fly-up evasive maneuvers consistent with a pilot’s preferred behavior, and using training to assess, demonstrate, and verify the system’s reliability. These factors are consistent with the literature on trust in automation and could lead to best practices for automation design, testing, and acceptance.


IEEE Software ◽  
1994 ◽  
Vol 11 (1) ◽  
pp. 35-28 ◽  
Author(s):  
D. Craigen ◽  
S. Gerhart ◽  
T. Ralston

Sign in / Sign up

Export Citation Format

Share Document