SHF: CSR: Small: Integrated Design and Verification of High-Confidence Interactive Systems

高可信度计算机系统是指那些需要高水平保证正确操作的系统。许多此类系统是交互式的--它们与人类交互--人类操作员的角色是系统操作的核心。这种系统的例子包括电传操纵飞机控制系统（与飞行员交互）、电传操纵汽车系统（与驾驶员交互）、医疗设备（与医生交互）和电子投票机（与投票人交互）。在所有这些系统中，不正确操作的成本可能非常严重。必须开发技术，确保这些系统的正确运行。然而，这是非常具有挑战性的，部分原因是正式指定的交互式system.This项目的所有部分的困难正在开发一种方法的原则性设计的高置信度的交互式系统的正确性是通过正式的验证和测试相结合的人类认证。该方法有三个组成部分。首先，系统是根据一组易于验证和测试的指导原则设计的，包括确定性、独立性和明确性。第二，新的算法技术正在开发中，以执行正式验证上述确定性，独立性，和系统设计上的明确属性。最后，利用上述设计原则和形式化验证来测试人机界面，并进行了大量的测试。该方法适用于一系列高置信度交互系统，包括航空电子设备，医疗设备和电子投票system.Human/operator错误是高置信度系统的主要故障源之一，本项目旨在通过原则性设计，形式验证和系统测试的紧密结合来减少此类故障的发生。这种方法正在被整合到加州大学伯克利分校的本科和研究生课程的课程和项目中。

High-confidence computer systems are those that require a high level of assurance of correct operation.Many of these systems are interactive - they interact with a human being - and the human operator's role is central to the operation of the system. Examples of such systems include fly-by-wire aircraft control systems (interacting with a pilot), drive-by-wire automobile systems (interacting with a driver), medical devices (interacting with a doctor), and electronic voting machines (interacting with a voter). The costs of incorrect operation in all such systems can be very severe. It is essential to develop techniques to ensure correct operation of such systems. However, this is very challenging due in part to the difficulty of formally specifying all parts of an interactive system.This project is developing an approach for the principled design of high-confidence interactive systems where correctness is certified through a combination of formal verification and testing by humans. The approach has three components. First, systems are designed according to a set of guiding principles that ease verification and testing, including determinism, independence, and unambiguity. Second, new algorithmic techniques are being developed to perform formal verification of the above determinism, independence, and unambiguity properties on system designs. Finally, the above design principles and formal verification are leveraged to test the human-computer interface with a tractable number of tests. The approach is applicable to a range of high-confidence interactive systems, including avionics, medical devices, and electronic voting systems.Human/operator error is one of the major sources of failures in high-confidence systems, and this project seeks to reduce the occurrence of such failures through a tight integration of principled design, formal verification, and systematic testing. The approach is being integrated into the curriculum and projects in undergraduate and graduate courses at UC Berkeley.