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

人机交互（HCI）的并发性可能导致设计者没有预料到的情况。可用性可能并不总是得到适当的维护，或者人工操作员可能无法完成系统设计支持的任务目标。这可能导致系统的不良采用，其使用的生产率降低，或不安全的操作条件。被称为“形式化方法”的数学工具和技术存在，用于对人机交互的不同元素进行建模和基于证据的评估，包括人机界面、人类操作员的任务分析行为和可用性。不幸的是，这些方法需要创建接口设计的正式模型，这是一种非标准的实践，容易出现建模错误。该项目将表明，形式化方法可以用于自动生成形式化人机界面设计，这些设计保证遵循可用性属性并支持人工操作任务。具体来说，将创建一个使用L*机器学习算法的系统，该系统将使用任务分析行为模型和可用性属性的正式表示生成正式的界面设计。研究人员将实现一个接口生成系统，用一组基准示例测试其性能，并评估其为实际应用生成接口的能力。为了实现生成器，研究人员将首先构建一个oracle系统，该系统能够根据分析师指定的任务模型和可用性属性接受或拒绝接口状态转换序列。该oracle系统将连接到L*算法的实现，该算法将通过观察生成的接口状态转换序列如何被oracle接受或拒绝来逐步学习正式的接口模型。利用系统的不同特性的人工测试用例将用于生成界面设计，并且将使用正式的验证来检查设计是否显示了预期的属性。该系统将用于生成人机界面，为患者控制的镇痛泵编程，这是一种自动向患者静脉注射止痛药的医疗设备。然后将生成的接口与这些设备现有的正式接口设计标准进行比较。从任务分析模型和可用性属性自动生成人机界面设计构成了一种以用户为中心的设计新方法。通过在接口的创建中使用这种方法，将保证设计总是显示某些属性。这将潜在地有助于确保设计将被用户接受，提高相关系统的效率，并促进更安全的操作。由该方法的实现产生的用户界面的形式化表示也将允许HCI设计者追求其他界面属性的形式化分析和验证，并且将促进用于可用性验证和认证目的的测试用例的自动生成。更广泛的影响：拟议的研究有可能显著改变人机界面的设计方式。通过保证生成的界面始终可用，本研究可以提高跨领域用户界面的可用性和安全性。生成的设计的性能保证可以减少开发和测试时间，从而降低开发和软件成本。这项工作也将提高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.