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.