SAFECOMP 2003 Keynote Talks

Abstract. The greatest problem facing the developer of a software based safety-related system is the challenge of showing that the system will provide the required service and will not cause or allow an accident to occur. It is very difficult to provide such evidence before the system is put to use, yet that is exactly what is required by society and regulators, and rightly so. Conventional wisdom recommends that systems are classified into safety integrity levels (SILs) based on some combination of the allowable rate or probability of unsafe failure and the probable consequences of such a failure; then, depending on the SIL, development methods are chosen that will (it is hoped) deliver the necessary system quality and the evidence on which to base a confident assessment that the system is, indeed, safe enough. Such conventional wisdom is founded on a number of unstated axioms, but computing is a young discipline and progress has thrown doubt on these assumptions. It is time for a new approach to safety assurance.

Abstract. Recently, researchers have developed a number of power- ful, formally based software tools, such as modelcheckers and theorem provers. To date, these tools have largely been used to analyze hardware designs. In the future, they should have signi cant value for analyzing the requirements and designs of software systems, especially high as- surance software systems, where compelling evidence is needed that the system satis es critical properties, such as safety and security properties. This paper brie y describes the di erent roles that formally based soft- ware tools can play in debugging, verifying, and testing software systems and software system artifacts. It also describes one important activity in software development notinvolving tools that is often neglected and that merits greater care and attention.