The best available modern system for formal verification is the Extended Static Checking system for Java developed at DEC SRL. This was developed at DEC before HP shut down that research operation.
The problem with such a tool is its limitation to static checking. Many of the most pernicious errors are dynamic. Consider race conditions, timing skew, and deadlocks. SPARK is more than a set of tools. It is also a specification of a subset of Ada. That subset was carefully chosen to avoid many of those dynamic errors.
While Java is statically verifiable and widely used, it is also not dynamically verifiable. The performance of a Java program on a given hardware platform is highly dependent upon the particular JVM the program runs in. More than that, Java synchronization is not temporally deterministic. It is relialble on the average. Being reliable on the average is simply not good enough for many safety critical real time systems.
_Safeware_ by Nancy Leveson looked at several software-related disasters. Only one disaster, the Therac radiation machine that fried several patients, was the result of actual bugs (and those bugs were race conditions).
The Leveson book is informative but not exhaustive. There have been several software safety incidents not covered by the book. It is not advisable to assume _Safeware_ describes all software failure modes.
Race conditions are only one of many dangerous failures in safety critical systems. Others (also not an exhaustive list) include deadlocks, timing skew, unhandled exhaustion of resources (memory, file space, fuel, power), buffer overflows, numeric underflows or overflows, and unexpected values from implicit conversions.
Remember the Mars rover last year. It had a nearly total failure of control software due to a full file system. The problematic behavior was not a case of properly executing the requirements. It was a violation of requirements not caught during testing because the duration of testing was significantly shorter than the duration of the actual mission.
The SPARK approach does flush out a lot of what-if questions. While going through the exercise of trying to formally prove compliance with requirements, the developer exposes ambiguous, poorly expressed, and contradictory requirements.
Nancy Leveson also promotes a rather formal analysis of system requirements. That analysis is necessary both in builing a correct system and in identifying the safety hazards inherent in the requirements.
Actually, yes. These people have successfully used SPARK on many projects. They also provide the tools making the SPARK approach feasible.
The SPARK approach causes discomfort for many software developers because its approach diverges from that of the various agile development processes.
If you read the book you will discover that the author's claims are supported by real data from real projects.
The SPARK approach is extremely formal. It has frequently been used on the safety critical portions of larger systems.
Remember that SPARK is intended for use primarily on real time safety critical systems. Such systems control energy sources. Failure of such systems carries a high probability of injury or death to people.
Slashdot Mirror
The problem with such a tool is its limitation to static checking. Many of the most pernicious errors are dynamic. Consider race conditions, timing skew, and deadlocks. SPARK is more than a set of tools. It is also a specification of a subset of Ada. That subset was carefully chosen to avoid many of those dynamic errors.
While Java is statically verifiable and widely used, it is also not dynamically verifiable. The performance of a Java program on a given hardware platform is highly dependent upon the particular JVM the program runs in. More than that, Java synchronization is not temporally deterministic. It is relialble on the average. Being reliable on the average is simply not good enough for many safety critical real time systems.
The Leveson book is informative but not exhaustive. There have been several software safety incidents not covered by the book. It is not advisable to assume _Safeware_ describes all software failure modes.
Race conditions are only one of many dangerous failures in safety critical systems. Others (also not an exhaustive list) include deadlocks, timing skew, unhandled exhaustion of resources (memory, file space, fuel, power), buffer overflows, numeric underflows or overflows, and unexpected values from implicit conversions.
Remember the Mars rover last year. It had a nearly total failure of control software due to a full file system. The problematic behavior was not a case of properly executing the requirements. It was a violation of requirements not caught during testing because the duration of testing was significantly shorter than the duration of the actual mission.
The SPARK approach does flush out a lot of what-if questions. While going through the exercise of trying to formally prove compliance with requirements, the developer exposes ambiguous, poorly expressed, and contradictory requirements. Nancy Leveson also promotes a rather formal analysis of system requirements. That analysis is necessary both in builing a correct system and in identifying the safety hazards inherent in the requirements.
Actually, yes.
These people have successfully used SPARK on many projects. They also provide the tools making the SPARK approach feasible.
The SPARK approach causes discomfort for many software developers because its approach diverges from that of the various agile development processes.
If you read the book you will discover that the author's claims are supported by real data from real projects.
The SPARK approach is extremely formal. It has frequently been used on the safety critical portions of larger systems.
Remember that SPARK is intended for use primarily on real time safety critical systems. Such systems control energy sources. Failure of such systems carries a high probability of injury or death to people.