Fundamentals of Dependable Computing for Software Engineers

CHAPTER 9        Software Fault Avoidance in Implementation

Learning objectives of this chapter are to understand:

•  How faults can be avoided in software implementation using correctness by construction.

•  The role of programming languages in software implementation.

•  The difficulties that arise with languages like C.

•  The advantages of languages designed for dependability such as Ada.

•  The role of programming standards.

•  The SPARK approach to correctness by construction using low-level specification and mechanical verification.

•  How formal verification can be applied easily by practicing engineers.

9.1 Implementing Software

Once we have a specification of what software is to do, we have to develop an implementation that can eventually ...