Using a Graphical Design Tool for Formal Specification

Colin Snook and Michael Butler.
Department of Electronics and Computer Science
University of Southampton
Highfield, Southampton, SO17 1BJ, United Kingdom.

Keywords: POP-II.B. formal specification, POP-III.D. visualisation, POP-V.A. mental models

Formal languages enable the behaviour of a system to be precisely specified and verified. However, even experienced users admit that creating useful models is difficult and this is a barrier to more widespread use. One reason for this is the lack of tools to assist in the modelling process. The process of formal specification is, in many ways, similar to that of programming where design notations and tools have evolved over many years. In this paper we suggest the adaptation of a graphical design notation (UML) for formal specification and support this with a prototype tool to perform automatic translation into a B specification.