Using Lightweight Formal Methods in Support of System Design

Dave Robertson
Dept. of Artificial Intelligence, Univ. of Edinburgh.

Abstract:

Everyone recognises that the early stages of system design tend to be "woolly": it is difficult to get a grip on the requirements and to see how these can be fitted to architectural and system specifications. This problem is often used to justify the exclusion of formal methods from these areas of design. I shall describe some counter-examples which suggest that formal methods can provide useful support to early stages of design, concentrating on recent work on codes of practice in the design of safety shutdown systems for oil production platforms. I will argue that the key issues in making these sort of methods work are:

• Narrowing the focus of application, either to a stage of design; or to a specific group of designers; or to a well-established domain.
• Applying the methods in a "lightweight" manner, in which a series of modest and carefully selected niches are found for formality.
• Attempting to adapt to, rather than revolutionise, existing work practices.