Using software verification techniques in non-safety critical embedded software designs
The aerospace and automotive industries are well known for the
rigorous software quality standards to which they must adhere, but
developers of non-safety critical systems can also benefit from the
type of standards employed within these industries. In addition to
producing reliable software, development costs can be contained and
requirements met more easily by observing a software quality process.
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.