In this paper we present an approach to safety verification of
Air-Traffic Control Systems (ATC) using probabilistic real-time
model-checking.  Namely we use ATC as a case study for the formal
analysis of real time systems whose performance depends on uncertain
or probabilistic behaviors. We construct a probabilistic timed
automata model for ATC by extending the Operator Choice Model (OCM), a
model of operators' behaviors in ATC system, with timed and
probabilistic assumptions. Some properties of this system are then
expressed in probabilistic real time computation tree logic
(PCTL). The verification results produced by using the tool PRISM
illustrate the uses of this approach to better understand the human
errors in real time systems.