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.
