Formal Reasoning for Requirements Engineering

FRERE

Introduction

This REAIMS module is used for adapting and defining processes for using formal methods for software production early in the process lifecycle. It is aimed at producing formal and formalisable software requirements specifications. It describes techniques for validating formal requirements against domain knowledge and the system specification.

The general aim is to define a process for translating informal requirements into formal specifications, guarding against errors and misunderstandings in this translation.

Summary description

The FRERE guide contains:

A model process based on the Adelard and GEC Alsthom experience of the industrial use of formal methods.
Technical guidance on the phases of the model process.
Metrics suitable for the model process.
Guidance on process adaptation for integrating formal methods with existing processes.

Benefits and application areas

There is increasing realisation of the importance of process in software development. A defined process is now essential in the production of safety-critical software, an aspect that has previously had little attention in the application of formal methods. This REAIMS module provides a process tailored to the use of formal methods.

The REAIMS process is specifically aimed at requirements engineering using formal methods, by firstly analysing the informal requirements, maintaining traceability between these and a formal model, and verifying the formal model. Application areas are: mission critical or commercially critical systems, e.g. complex microprocessor design, fault-tolerant architectures, complex real-time systems; and any where regulatory or other requirements mandate or recommend use of formal methods, e.g. safety critical systems, protection systems, safety related systems.

Industrial areas where this is the case include defence, nuclear, transport, telecommunications and aerospace.

How to apply

The FRERE process can be applied directly if there is no existing process for development of high-integrity software. Otherwise the process can be adapted to fit with existing procedures. Guidance on how this adaptation can be carried out is included in the module.

More information available from:

Robin Bloomfield
Adelard
3, Coborn Road
London E3 2DA
United Kingdom Phone: +44-181 983 0217
FAX: +44-181 983 1845
email: reb@adelard.co.uk

François Bustany
Steria-Digilog 5
21, Rue Frederic Joliot
F-13791 Aix en Provence
France Phone: +33-4216 8600
FAX: +33-4216 8686

Herbert Schippers
TÜV Informationstechnik GmbH
Im Teelbruch 122
D - 45219 Essen
Germany Phone: +49 201 825 5120
FAX: +49 201 825 5131
email: H.Schippers@tuvit.cubis.de

Stephen Shirlaw
Project Coordinator
GEC Alsthom
Phone: +44-181-236-9254
FAX: +44-181-207-6694
email: s.shirlaw@gasl.co.uk

Page last updated Thu, 18 December 1997. Please report problems to reaims-request@comp.lancs.ac.uk