Formal methods

Chapter 10

The term formal methods is used to refer to any activities that rely on mathematical representations of software including formal system specification, specification analysis and proof, transformational development, and program verification. In the 1980s many software engineering researchers proposed that using formal development methods was the best way to improve software quality. They also predicted that by 21st century a large proportion of software would be developed using formal methods. However, this prediction has not come true.

Critical systems development usually involves a plan-based software process that is based on the waterfall model of development. Both the system requirements and the system design are expressed in detail and carefully analysed and checked before implementation begins. The involvement of the client decreases and the involvement of the contractor increases as more detail is added to the system specification. In the early stages of the process the specification should be ‘customer-oriented’.

Stages of software specification and its interface with the design process are (in order): User Requirements Definitions → System requirements specification → Architectural design → Formal specification → High-level design. Depending on the process used, specification problems discovered during formal analysis might influence changes to the requirements specification if this has not already been agreed.

Two fundamental approaches to formal specification have been used to write detailed specifications for industrial software systems:

1. An algebraic approach where the system is described in terms of operations and their relationships.
2. A model-based approach where a model of the system is built using mathematical constructs such as sets and sequences, and the system operations are defined by how they modify the system state.

Large systems are usually decomposed into sub-systems that are developed independently. Sub-systems make use of other sub-systems, so an essential part of the specification process is to define sub-system interfaces.

The algebraic approach was originally designed for the definition of abstract data type interfaces. In an abstract data type, the type is defined by specifying the type operations rather than the type representation, so it is similar to an object class.

The process of developing a formal specification of a sub-system interface includes the following activities:

1. Specification structuring. Organise the informal interface specification into a set of abstract data types or object classes.
2. Specification naming. Establish a name for each abstract type specification.
3. Operation selection. Choose a set of operations for each specification based on the identified interface functionality.
4. Informal operation specification. Write an informal specification of each operation.
5. Syntax definition. Define the syntax of the operations and the parameters to each.
6. Axiom definition. Define the semantics of the operations by describing what conditions are always true for different operation combinations.

The simple algebraic techniques can be used to describe interfaces where the object operations are independent of the object state. Therefore, the result of applying an operation should not depend on the results of previous operations. As structure increases in size, algebraic descriptions become increasingly difficult to understand.

Model-based specification is an approach to formal specification where the system specification is expressed as a system state model. System operations are defined by how they affect the state of the system model.

While developing a model-based specification, state variables and predicates should be defined.

My thoughts

Maybe I just don’t have any good experience, but for me a model-based approach seems like too complicated case, and algebraic approach sound more natural.