NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner


John image John Rushby
SRI
The Challenge of High-Assurance Software

It is difficult to build complex systems that (almost) never go (badly) wrong, yet this is what we expect of airplanes and pacemakers and the phone system. In essence, we have to anticipate everything that could fail or go wrong, develop countermeasures, and then provide compelling evidence that we have done all this correctly. I outline some of the intellectual challenges in construction of suitable evidence, particularly as applied to software. I introduce the idea of "possibly perfect" software and its associated "probability of perfection" and describe how this relates to correctness and reliability. I sketch some approaches to estimating a probability of perfection and touch on alternative proposals such as those based on "eliminative induction." I then describe epistemic and logic uncertainties in high-assurance software and speculate on the relation between these and the notion of resilience. Much of this material is based on joint work with Bev Littlewood and others at City University UK, some of which is described a recent paper [1].

1. Littlewood, B., Rushby, J.: Reasoning about the reliability of diverse two-channel systems in which one channel is "possibly perfect". IEEE Transactions on Software Engineering 38 (2012) 1178-1194

First Gov logo
NASA Logo - nasa.gov