Choosing a Formal Method
Scope
This document is aimed at those who have decided that it would be a good idea for their project or organisation to use a formal method, but are not sure what steps to take next: which formal method or which kind of formal method will be best for their purposes.
In order to result in a successful outcome, choosing a formal method requires the same approach as any other technical decision. First, one needs to be clear about one’s objectives and to know what are the technical, organisational and management constraints. Then one may focus on the characteristics of a formal method which will meet those objectives and constraints. Finally a method can be selected which most closely conforms to, and whose tools, experience and support most closely conforms to those characteristics.
General Approach
This guide is a framework which, we hope, will help you to construct for yourself a decision process tailored to your own application and organisation. The sections which follow consist of possible aims, criteria, characteristics and needs. Considering whether each of these applies should help to focus on and define the objectives, constraints and other criteria particular to an application and organisation which form the context of a choice of formal method, i.e. your application and that part of your organisation which will be using a proposed formal method. The bulleted points, which can be treated as a set of questions for you to ask yourselves, are a guide only; they can be extended or modified according to each individual organisational and technical environment. What is important is to establish and define that environment as clearly as possible before proceeding to make a selection. The purpose of the questions is to help the user organisation to determine appropriate criteria. Accordingly, the questions are grouped into some principal categories in the following sections:
- General reasons for choosing formality
- Characteristics of the application
- Criteria for success ofapplication
- Needs and constraints of the organisation
The answers to these questions form a context in which you can then focus on what are the characteristics of the formal method which is most suitable for your needs. To help you to do that, the “possible characteristics” of a formal method are presented in the last main section:
- Characteristics of a formal method
Having gone through this process you can then match your list of requirements against what is on offer, talking to tool suppliers etc.
General reasons for choosing formality
Software and system quality, consistency and integrity can be improved by formalising different products and processes in the development cycle. Are the reasons you want to apply formal techniques:
- to improve quality and rigour of whole development process?
This would be the case if your organisation wished to adopt a formal approach to software or system development as part of a general improvement of its development process. An improvement of development technology, like adopting formal methods, is a valid aspect of process improvement just as are improvements in documentation, configuration management, measurement etc.
- to improve integrity, reliability or other characteristics of the system?
In some circumstances formal methods may be applied to system development as well as software development. The analysis and design of the system architecture usually precedes the specification of software components. Do you propose to apply formal methods to the development of the larger system as well as the software?
- to reduce specification errors?
Expressing the specification, particularly the functional specification, of software and system components helps greatly to reduce errors in specifications. Is this your principal motivation?
- to improve requirements definition?
Requirements, especially system requirements, are usually expressed in non-formal language. The process of deriving formal expressions of specifications from them nearly always has the effect of improving those requirements definitions. Experience indicates that omissions and inconsistencies in the requirements statements are found more reliably than with other techniques. Is requirements analysis and definition the phase of the life-cycle which you particularly wish to address?
- to improve documentation and understanding of designs?
There is at present a great quantity of legacy software which is undocumented or with very inadequate documentation. Maintaining the software is as a result extremely difficult and confidence in its reliability is low. Good documentation reduces these problems and formal descriptions of the life-cycle products dramatically reduces them. Is this your motivation for using formal methods?
- to provide a firmer foundation for maintenance and enhancement? See above.
- to explore the properties of a design architecture?
In some applications it is not possible to characterise the behaviour of the context of the software; in some telecommunications environments, for example, patterns of traffic may be to an extent unpredictable. A formal model of the design of the software can provide an understanding of its properties and limitations. Do you wish to improve your knowledge of your software’s properties by more accurately modelling the design?
- to provide a more rational basis for choosing test data?
Relatively recently, techniques have been developed for deriving test data from functional specifications of software components. Such test sets may be more closely related to the specifications which the software is designed to fulfil, and the process of test set derivation is more systematic if formal methods are used for functional specification.
- to be as certain as possible that the design and implementation are error-free?
In safety-critical and other critical contexts it can be of utmost importance to ensure that the software is functionally free from errors. Applying formal descriptions to specifications and designs enables proofs of correctness between those successive stages of the development cycle.
- to meet particular customer or standards requirements?
Some contracts mandate the use of formal methods during certain stages of the development cycle, or mandate adherence to standards which do so.