Using software verification techniques in non-safety critical embedded software designs

Software development often proves far more expensive than expected; bugs discovered late in the development cycle send costs soaring and risk the integrity and safety of a system, especially if the software has been deployed. Obviously, careful planning, organization and a team with the correct skills all help. However, it is verification and validation (V&V) that identify when and how the development process drifted from what was intended or required by the user.

What's the difference between verification and validation? Validation focuses on producing the right software system while verification ensures the software is built the right way. V&V should be evident at each stage of development and conducted with reference to the outputs from previous stages.

Verification is at the hub of a quality process, evaluating whether or not a product, service, or system complies with a regulation, specification, or conditions imposed at the start of a development phase.

Since its inception in the early 1970s, the sequential waterfall model serves as a framework for modern alternatives (Figure 1 below). Typically, earlier phases need to be revisited as developers work iteratively and requirements come together, as users test prototype versions of the system.

Because of this iterative approach, it is even more important to apply suitable V&V techniques at each stage and within each iteration of the cycle.

Figure 1: The familiar waterfall process for a typical software development life-cycle.

Evidence indicates that the earlier a defect is discovered in development the less impact it has on both the timescales and cost. There is much to gain by ensuring that requirements are captured in full, they are well understood, and they are specified completely and unambiguously.

Formal methods of tracking requirements are based on a mathematical approach to specification, development and verification of software and hardware systems. Formal methods can vary from using commonly accepted notation to the full formality of theorem proving or automated deduction " a method of proving mathematical theorems by a computer program " which is currently the most developed subfield of automated reasoning (AR).

Although the cost of using formal methods often limits them to applications where a high level of software integrity is required, some degree of formal specification reaps benefits at later stages in the process for any software application. It is at this point that test data is constructed so that the system may be later validated against requirements.

Traditionally, the design of large systems follows a top-down, functional decomposition approach. The system is broken down into subsystems, which pass data and control across defined interfaces.

Subsystems normally comprise a number of program modules or units and each module has a number of routines which perform distinct tasks. Coupling and cohesion are two important quality metrics considered during the design of a software system. A high degree of coupling implies an over-dependency between modules and indicates poor structure. Modules with low cohesion are typically difficult to maintain, test, reuse, and even difficult to understand.

Object-oriented (OO) methodologies add a further dimension, with data and functionality encapsulated by the concept of an object which interacts with other objects. An OO design is driven by the choice of object types, or classes, and their representation.