Using B to Design and Verify Controllers for

Chemical Processing

<_author_search_(k. lano)>K. Lano, <_author_search_(j. bicarregui?)>J. Bicarregui?, <_author_search_(a. sanchez??)>A. Sanchez??

Abstract. This paper is concerned with bridging the gap between approaches for the synthesis of controllers in the process industries and formal methods of specifying, designing and verifying reactive and realtime systems.

We present a method which integrates techniques for the synthesis of procedural controllers [24] with specification and verification techniques for B [1]. The combined method enables a systematic approach to be taken to the creation of formalised designs for process controllers and proof obligations for the correctness of these designs against specifications to be generated.

The techniques have been applied to a part of an industrial plant [20]. In this paper we present the approach using the well-known gas burner example [22]. We also propose extensions to B which would allow more abstract and expressive specification of the requirements and designs of such systems.

1 Introduction

The chemical process industries are some of the world's most successful

and significant industries, with world-wide sales in 1993 of 1250 billion US

dollars [7]. Process control is a key element in improving the efficiency

of these industries and enabling more advanced and flexible plants to

be developed [3]. As in other domains, the progress of the theory and

practice of process control for chemical plants involves a collaboration

between application engineers, control engineers and software engineers.

This is particularly marked when aspects such as safety of the resulting

plants is considered: analysing the hazards that may arise from a process,

and how these may be minimised, inevitably involves consideration of the

interactions between elements of each of these domains.

A formal process of software specification and design for process con-

trollers introduces the possibility of verifying some safety requirements

on the basis of a well-defined mathematical theory. In the case of the B

? Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ ?? Centre for Process Systems Engineering, Dept. of Chemical Engineering, Imperial College