Fig.1

General structure of the proposed method"

Fig.2

Hierarchical control structure of TCAS mission process"

Fig.3

Task schedule of control process elements relative to TCAS mission process"

Table 1

Unsafe control actions in TCAS mission process"

Table 2

Hazard causes for TCAS mission failure related to human factors"

Table 3

Hazard causes for TCAs mission failure related to device factors"

Fig.4

Timed automata model of controller"

Table 4

Control action and corresponding UPPAAL channel based on STAMP/STPA analysis"

Fig.5

Timed automata model of pilot"

Fig.6

Timed automata model of aircraft"

Fig.7

Timed automata model of TCAS"

Fig.8

Timed automata model of ADS-B"

Fig.9

Timed automata model of pilot with hazard causation"

Fig.10

Timed automata model of aircraft with hazard causation"

Fig.11

Timed automata model of ADS-B system with hazard causation"

Fig.12

Timed automata model of TCAS with hazard causation"

Fig.13

Timed automata model of controller with hazard causation"

Table 5

Syntax meaning of BNF and its equivalent properties"

Table 6

Descriptions of activity validation statement, statement function of model and validation results"

Fig.14

Activity validation results of model based on UPPAAL"

Fig.15

State transition in TCAS mission process due to specific hazard causation"

Table 7

Descriptions of validation statement statement function for accessibility of hazard causes and validation results"

Fig.16

Validation results for accessibility of hazard causes and adequacy of safe constraints based on UPPAAL"

Table 8

Description of validation statement statement function for adequacy of safe constraints and validation results"