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

高可信度的计算机系统是那些需要高度保证正确操作的系统。这些系统中有许多是交互式的——它们与人类互动——而人类操作员的角色是系统操作的核心。此类系统的示例包括电传飞机控制系统（与飞行员交互）、电传汽车系统（与驾驶员交互）、医疗设备（与医生交互）和电子投票机（与选民交互）。在所有这些系统中，错误操作的代价可能非常严重。开发技术以确保这些系统的正确运行是至关重要的。然而，这是非常具有挑战性的，部分原因是难以正式指定交互系统的所有部分。该项目正在开发一种方法，用于高可信度交互系统的原则设计，其中通过正式验证和人类测试的组合来认证正确性。该方法有三个组成部分。首先，系统是根据一组简化验证和测试的指导原则设计的，包括决定论、独立性和无歧义性。其次，正在开发新的算法技术，以对上述系统设计的决定论、独立性和无歧义性进行形式化验证。最后，利用上述设计原则和形式化验证，通过可处理的测试数量来测试人机界面。该方法适用于一系列高置信度交互系统，包括航空电子设备、医疗设备和电子投票系统。在高置信度系统中，人为/操作人员的错误是故障的主要来源之一，该项目旨在通过原则设计、正式验证和系统测试的紧密集成来减少此类故障的发生。这种方法被整合到加州大学伯克利分校的本科和研究生课程和项目中。

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.