Page 351 -

334 Chapter 12 Dependability and security specification

Formal specification techniques

Formal system specifications may be expressed using two fundamental approaches, either as models of the
system interfaces (algebraic specifications) or as models of the system state. You can download an extra web
chapter on this topic, where I show examples of both of these approaches. The chapter includes a formal
specification of part of the insulin pump system.
http://www.SoftwareEngineering-9.com/Web/ExtraChaps/FormalSpec.pdf

The starting point for all formal development processes is a formal system model,
which serves as a system specification. To create this model, you translate the sys-
tem’s user requirements, which are expressed in natural language, diagrams, and
tables, into a mathematical language which has formally defined semantics. The for-
mal specification is an unambiguous description of what the system should do.
Using manual or tool-supported methods, you can check that a program’s behavior is
consistent with the specification.
Formal specifications are not just essential for a verification of the design and
implementation of software. They are the most precise way of specifying systems,
and so reduce the scope for misunderstanding. Furthermore, constructing a formal
specification forces a detailed analysis of the requirements and this is an effective
way of discovering requirements problems. In a natural language specification,
errors can be concealed by the imprecision of the language. This is not the case if the
system is formally specified.
Formal specifications are usually developed as part of a plan-based software
process, where the system is completely specified before development. The system
requirements and design are defined in detail and are carefully analyzed and checked
before implementation begins. If a formal specification of the software is developed,
this usually comes after the system requirements have been specified but before the
detailed system design. There is a tight feedback loop between the detailed require-
ments specification and the formal specification.
Figure 12.12 shows the stages of software specification and its interface with soft-
ware design in a plan-based software process. As it is expensive to develop formal
specifications, you may decide to limit the use of this approach to those components
that are critical to the system’s operation. You identify these in the architectural
design of the system.
Over the past few years, automated support for analyzing a formal specification has
been developed. Model checkers (Clarke et al., 2000) are software tools that take a
state-based formal specification (a system model) as an input, along with the specifica-
tion of some formally expressed desirable property, such as ‘there are no unreachable
states.’ The model checking program exhaustively analyzes the specification and either
reports that the system property is satisfied by the model or presents an example
that shows it is not satisfied. Model checking is closely related to the notion of static
analysis and I discuss these general approaches to system verification in Chapter 15.