摘要

User-centered design (UCD) is an approach for creating human-machine interfaces that are usable and support the human operator's tasks. UCD can be challenging because designers can fail to account for human-machine interactions that occur due to the concurrency between the human and the other system elements. Formal methods are tools that enable analysts to consider all of the possible system interactions using a combination of formal modeling, specification, and proof-based verification. However, creating formal interface design models can be extremely difficult. This work describes a method that supports UCD by automatically generating formal designs of human-machine interface behavior from task-analytic models. The resulting interface design will always support the behavior captured in the task model. This paper describes the method and demonstrates its capabilities with three case studies: a light switch, a vending machine, and a patient-controlled analgesia pump. The produced designs are validated with formal verifications to prove that they support their associated tasks. Results and future research are discussed.

  • 出版日期2017-12