Differences

This shows you the differences between two versions of the page.

--- verification [2007/11/01 14:06] – franck
+++ verification [2007/11/01 14:13] (current) – franck
@@ Line 125: / Line 125: @@
 Techniques that are lacking, notes Price, include the use of formal methodologies for designing and writing software."
-==== Ambulance Dispatch System failure ====
+==== Ambulance dispatch system failure ====
 In November 1992, the computerized dispatch system for the London (England) Ambulance Service, broke down suddenly and “locked up altogether”, leaving calls for assistance which had already been stored in the system unavailable, and forcing a taxing and cumbersome return to a manual, paper-based dispatch system. Luckily, the breakdown occurred in early morning hours, so that there were no severe consequences for patients.
@@ Line 134: / Line 135: @@
 gradually used up all available memory thus causing the system to crash. This programming error should not have occurred and was caused by carelessness and lack of quality assurance
 of program code changes. Given the nature of the fault it is unlikely that it would have been detected through conventional programmer or user testing."
 ==== Software that kills ====
@@ Line 149: / Line 151: @@
 Levenson and Turner warn against simply blaming tragedies such as the Therac-25 accidents on software errors alone—they argue for a deeper analysis of “organizational, managerial, technical” and even “political, or sociological factors” on the grounds that, as we have already observed, there will always be another bug; so focusing only on eliminating individual software errors may blind us to considering the larger environment which tolerates and unintentionally furthers the occurrence of such errors with their drastic consequences.
+True enough, but one of the underlying causes of unsafe software may be the general reluctance to apply formal methods and verification techniques, usually on the grounds that they are too difficult to automate and hence cannot be applied to “real code”. One purpose of this text is to argue by example against the validity of this excuse—to show that through the use of appropriate tools, portions of code can be verified automatically
+or semi-automatically, or can be generated automatically from logical specifications. Just as we would expect any author who uses a word-processor to use a spelling checker
+to check for at least those spelling errors which the dictionary can catch, so we should — in the future, if not today — expect programmers to routinely check or generate their code with software verification tools to catch and eliminate at least those errors which the tools can prevent. Even then programmers will not succeed in stamping out that vexatious and stubborn “last bug”, but at least its available hiding places will grow smaller, and both money and lives may be saved.