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 ...

Get Fundamentals of Dependable Computing for Software Engineers now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.