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

人机交互(HCI)的并发性质可能会导致设计者意想不到的情况。可用性可能并不总是得到适当的维护，或者操作员可能无法完成系统设计支持的任务目标。这可能会导致系统的不良采用、使用时的生产率降低或不安全的操作条件。数学工具和技术称为“形式方法”，用于对人机交互的不同元素进行建模和基于证据的评估，这些元素包括人机界面、人类操作员的任务分析行为和可用性。不幸的是，这些方法需要创建接口设计的正式模型，这是非标准的做法，容易出现建模错误。该项目将展示正式方法方法可用于自动生成正式的人机界面设计，以保证遵守可用性属性并支持人工操作员的任务。具体地说，将创建一个使用L*机器学习算法的系统，该系统将使用任务分析行为模型和可用性属性的形式化表示来生成正式的界面设计。研究人员将实现一个界面生成系统，通过一组基准测试示例测试其性能，并评估其为现实应用程序生成界面的能力。为了实现生成器，研究人员将首先构建一个Oracle系统，该系统能够根据分析师指定的任务模型和可用性属性接受或拒绝界面状态转换序列。该甲骨文系统将连接到L*算法的实现，该算法将通过观察甲骨文如何接受或拒绝生成的界面状态转换序列来逐步学习正式的界面模型。利用系统不同功能的人工测试用例将用于生成界面设计，并将使用正式验证来检查设计是否显示了预期的属性。该系统将用于生成人机界面，用于对患者控制的止痛泵进行编程，这是一种自动向患者静脉输送止痛药的医疗设备。然后将生成的界面与这些设备现有的正式界面设计标准进行比较。根据任务分析模型和可用性属性自动生成人机界面设计构成了一种以用户为中心的设计新方法。通过在创建界面时使用此方法，将确保设计始终显示某些属性。这可能有助于确保设计将被用户接受，提高相关系统的效率，并促进更安全的操作。这种方法的实施所产生的用户界面的形式化表示还将允许人机交互设计者对其他界面属性进行形式化分析和验证，并将促进用于可用性验证和认证目的的测试用例的自动生成。广泛影响：拟议的研究有可能显著改变人机界面的设计方式。通过保证生成的界面始终可用，这项研究可以提高许多领域用户界面的可用性和安全性。生成的设计的性能保证可以减少开发和测试时间，从而降低开发和软件成本。这项工作还将加强UIC不同工科学生群体的教育和研究经验。为这项工作获得的计算资源将提供给学生进行研究项目，研究结果将被纳入PI的研究生和本科生课程。项目成果将由学生研究人员在会议上发表，并在高质量的期刊上以开放获取的方式发表。将使用一个专门的网站来迅速传播在这项工作中产生的成果和工具。

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.