EAGER: Automatically Generating Formal Human-Computer Interface Designs From Task Analytic Models

点击翻译按钮获取中文摘要

The concurrent nature of human-computer interaction (HCI) can result in situations unanticipated by designers. Usability may not always be properly maintained or human operators may not be able to complete the task goals that a system was designed to support. This can result in poor adoption of the system, decreased productivity with its use, or unsafe operating conditions. Mathematical tools and techniques called "formal methods" exist for modeling and providing proof-based evaluations of different elements of HCI including the human-computer interface, the human operator's task analytic behavior, and usability. Unfortunately, these approaches require the creation of formal models of interface designs, something that is non-standard practice and prone to modeling error. This project will show that a formal-methods approach can be used to automatically generate formal human-computer interface designs that are guaranteed to adhere to usability properties and to support human operator tasks. Specifically, a system that uses the L* machine learning algorithm will be created that will generate formal interface designs using task analytic behavior models and formal representations of usability properties.The researchers will implement an interface generation system, test its performance with a suite of benchmark examples, and evaluate its ability to generate an interface for a realistic application. To implement the generator, the researchers will first construct an oracle system capable of accepting or rejecting interface state transition sequences based on analyst-specified task models and usability properties. This oracle system will be connected to an implementation of the L* algorithm that will progressively learn a formal interface model by observing how generated sequences of interface state transitions are accepted or rejected by the oracle. Artificial test cases that exploit the different features of the system will be used to generate interface designs, and formal verification will be used to check that the designs exhibit the intended properties. The system will be used to generate the human-computer interface for programming a patient controlled analgesia pump, a medical device that automatically delivers pain medication to patients intravenously. The generated interface will then be compared against the formal interface design standard that exists for these devices.The automatic generation of human-computer interface designs from task analytic models and usability properties constitutes a novel approach to user-centered design. By using this method in the creation of interfaces, designs will be guaranteed to always exhibit certain properties. This will potentially help ensure that designs will be accepted by users, improve the associated system's efficiency, and facilitate safer operation. The formal representation of user interfaces that result from the implementation of this method will also permit HCI designers to pursue formal analysis and verification of other interface properties, and will facilitate the automated generation of test cases for usability verification and certification purposes.Broader Impacts: The proposed research has the potential to significantly change the way human-computer interfaces are designed. By guaranteeing that generated interfaces are always usable, this research could improve the usability and safety of user interfaces across many domains. The performance guarantees of the generated designs could allow development and testing times to be reduced, thus decreasing development and software costs. This work will also enhance the education and research experience of UIC's diverse engineering student body. The computational resources acquired for this work will be made available to student for research projects and study results will be incorporated into the curriculum of the PI's graduate and undergraduate courses. Project results will be presented at conferences by student researchers and published with open access in high quality journals. A dedicated website will be used to rapidly disseminate results and tools produced during this effort.