FORMAL TECHNIQUES IN THE DEVELOPMENT OF BLACKBOARD SYSTEMS

In a recent book, the author presented a mathematical specification of a blackboard system shell. The exercise suggested a method for developing blackboard systems with the aid of formal methods. This paper describes a formal method for the development of blackboard systems. The method is based, in part, on an informal one. Apart from the difference in emphasis (formal rather than informal), the new approach rests upon a formal definition of the architecture. The essential idea is that the mapping between the formal model of the problem domain (which is intended to be similar to the formal models proposed by, for example, Hayes) and the blackboard shell should be supported by formal proofs of correctness in a way identical to formal software engineering. We present an informal method for constructing blackboard systems. The informal method forms the basis of the formal method whose initial stages are then described. We outline the formal treatment of control and suggest the use of temporal logic as a tool for reasoning about control. The paper ends with a review of the method.