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

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