2. A brief overview of software reliability methods

There are numerous methods (and associated tools) for improving software reliability. These methods are based on a sometimes complex formalism which allows a more or less relevant level of verification. They can be applied to a particular phase of the development cycle or to all phases, to certain properties (static or dynamic) or to all software properties. The level of effort depends, of course, on the scope of the methods. Type checking (as done in most programming languages) is less effective than static analysis, which in turn is less effective than model checking or automated abstraction. Maximum confidence is achieved with software developed in a language that can be used directly to prove theorems.

To avoid errors in the software, there are several possible solutions for each design phase. We have seen that errors arise from successive transformations of...