Growing use of computers in safety-critical systems increases the need for Human Computer Interfaces (HCIs) to be both smarter-to detect human errors-and better designed-to reduce likelihood of errors. We are developing methods for determining the likelihood of operator errors which combine current theory on the psychological causes of human errors with formal methods for modelling human-computer interaction. We present the models of the HCI and operator in an air-traffic control (ATC) system simulation, and discuss the role of these in the prediction of human error rates.