Informatics had a significant interest in formal specification techniques in both the software engineering and computer graphics areas. A flavour of some of these projects is given below.
Tony Cox worked on the Alvey (VLSI/CAD) funded research project The Transformation and Verification of Occam Programs, which is a collaboration between Inmos Ltd and Oxford University; at Oxford the project consisted of Dr Bill Roscoe, supervising, and two research officers, in addition to Tony.
Occam, a language for concurrent systems, was derived from the language Communicating Sequential Processes, and inherits its clear semantics; in Roscoe, A Denotational Semantics For Occam, a model is given which accounts for both the purely parallel and the internal and store-based aspects of the language. This semantics readily gives rise to a set of laws between Occam programs (Roscoe and Hoare Laws of Occam programming) which can be used as the basis of an automated transformation system. A semantics preserving transformation system offers various possibilities: deciding the equivalence of programs (through transforming to a normal form); improving efficiency; transforming to restricted syntax for VLSI implementation.
A prototype system was written in Edinburgh Standard ML which was able to parse Occam Programs, apply any of the transformation laws and converted a program to normal form, including infinitary programs to a specified number of communication steps. Tony Cox did almost all the programming on the project, while other members contributed ideas on concurrency theory and the user-interface.
The prototype transformation system was used in earnest in the development of the floating point transputer and proved to be of real value in the development of a very complex system.
Mario Martins (MM) from the University of Minho, Portugal was a Visiting Scientist from March to December 1987.
Text editors are are the most widely used software components of any interactive computing system and a new generation of editors has emerged based on sophisticated interactive techniques. Spy, developed at RAL, was a prime example of such an editor. Formal specification of text editors has received very little attention, given the number of text editors in use.
Mario developed a formal specification of Spy in Oxford's Z specification notation. To increase the modularity and readability of the specification the editor was divided into four subsystems, the Editing System, the File System Interface, the Display Control System and the Window System. The schema notation in Z allowed complex specifications to be presented in manageable chunks and this facility was used to great advantage in this specification. The editor specification was developed in easy stages, corresponding to increasing richness of functionality. The specification started to get difficult when the UNDO facility was introduced. A report describing the specification was produced.
Jim Woodcock with He Jifeng (PRG, Oxford) worked on the combination of the Z notation with CSP, the basic idea being to use Z to describe states, and CSP to describe concurrency and interaction. Jifeng fixed the theoretical underpinnings and produced a complete set of rules for data refinement. Jim produced a case study which used the new techniques. Part of the work was presented at a Z users meeting in Oxford, and at a series of lectures at IBM's Hursley Park.
Working with material from the CICS formalisation project at IBM, Jim developed some case studies in specification and refinement. Later, he worked with IBM on large-scale proofs of parts of the CICS transaction processing system.
Working with Jim Davies, a specification and implementation of the Ethernet protocol in Timed CSP was produced. This was the first major use of the theory, and it threw up many research topics. It is not possible to complete the proof that the implementation satisfies the specification without a probabilistic model for CSP.
This was a three year project funded by the IEATP. The consortium consists of Royal Holloway and Bedford New College (RHBNC), the University of Glasgow and Informatics and was uncled by British Telecom (BT).
LOTOS is based on the concept of specifying a system in terms of observable behaviour. In LOTOS events are used to denote the occurrence of something which the specification makes assertions about. LOTOS can express ordering constraints on events and through their structure the communication and change of information within a system. The ordering and structure of events are captured in two separate components of the LOTOS language. The first of these, the process calculus, is based on process algebraic methods (Milner) and the semantics are based on Milner's CCS (system of inference rules and labelled transitions of processes) and Hoare's CSP (operators for process composition). The second component, based on the data typing language ACT ONE, uses equational specification with initial algebra semantics.
The industrial use of LOTOS has focused on developing formal descriptions of OSI standards. Complete formal descriptions of several OSI standards now exist and are being progressed within ISO as technical reports. It is ISO policy that these texts will become definitive standards. The project uncle, British Telecom, is heavily involved in this work, and Glasgow University is already involved in LOTOS work involving the translation of ASN.1 into LOTOS.
If full benefit is to be obtained from the use of this formal specification language it is essential to be able to reason about such specifications and the implementations derived from them, in order to determine that the specification has the required properties, or verification requirements.
BT was already working on the verification of LOTOS specifications, using existing theorem provers. However, while research had been done on verification for different parts of the language, it had not yet been incorporated into an integrated whole. Term rewriting and equational reasoning were clear candidates for this work, as they were already widely accepted as a verification technology for the major constituents of the language, algebraic specifications and process algebras.
The equational reasoning system ERIL was used to for experimentation with a wide variety of strategies.
Brian Matthews designed and implemented a basic set of general tools for use with equational reasoning in Standard ML and a Knuth-Bendix Completion algorithm was produced. This was developed further with the use of the ML module system to produce an initial basis for a set of tools for equational reasoning. In addition an ERIL-like interface was placed on top of the tools to give a clean presentation of the tools to the user.
ZIP was a three year project involving Jim Woodcock that was aimed at:
David Duce worked for many years, in collaboration with other members of RAL staff and external contacts, formally specify parts of the emerging ISO/IEC graphics standards (in particular GKS, the revised version GKS-94, PHIGS and the Computer Graphics Reference Model). Some examples of this work are:
David A. Duce, E. V. C. Fielding, Lynn S. Marshall: Formal specification of a small example based on GKS. ACM Trans. Graph. 7(3): 180-197 (1988)
David A. Duce, Ljiljana B. Damnjanovic: Formal Specification in the Revision of GKS: An Illustrative Example. Comput. Graph. Forum 11(1): 17-30 (1992)
Ljiljana B. Damnjanovic, David A. Duce, S. K. Robinson: GKS-9x: Some Implementation Considerations. Comput. Graph. Forum 12(3): 295-313 (1993)
David A. Duce, Fabio Paterno: A Formal Specification of a Graphics System in the Framework of the Computer Graphics Reference Model. Comput. Graph. Forum 12(1): 3-20 (1993)
Philippe Nehlig, David A. Duce: GKS-9x: The Design Output Primitive, an Approach to a Specification. Comput. Graph. Forum 13(3): 381-392 (1994)
