A Formal Methods Workbench for Critical Systems
John Rushby · 2000
The research performed in this project enhanced the PVS formal verification system to provide improved support for the development and assurance of fault-tolerant and safety-critical systems. The capabilities developed are freely available in the publicly distributed version of PVS. In addition, new and more systematic methods were developed for verifying certain kinds of critical systems (including self-stabilizing ones), and an exciting new application of formal methods to the problems of automation surprises and mode confusions in advanced cockpits was pioneered. Finally, new fault-tolerant algorithms and architectures were developed, and some significant demonstration applications of formal methods were performed.