Contact us Heritage collections Image license terms
HOME ACL ACD C&A INF SE ENG Alvey Transputers Literature
Further reading □ OverviewSupportTheorem ProvingERILIPSE 2.5MURALFormal Specification
CCD CISD Harwell Archives Contact us Heritage archives Image license terms

Search

   
InformaticsSystems EngineeringSoftware
InformaticsSystems EngineeringSoftware
ACL ACD C&A INF CCD CISD Archives
Further reading

Overview
Support
Theorem Proving
ERIL
IPSE 2.5
MURAL
Formal Specification

Integrated Project Support Environment: IPSE 2.5

IPSE 2.5 was a major Alvey project which ran from 1985 to 1990. It was a consortium of Informatics, the University of Manchester and five UK companies under the leadership of STC Technology Ltd. An IPSE, an Integrated Project Support Environment, provides support for the management and control of the processes involved in a complex project such as software development. A distinguishing characteristic of IPSE 2.5 was that it provided a generic IPSE which could be instantiated to provide support for a particular method or methods. This was achieved by describing the development process associated with the method in a process modelling language, PML, and providing appropriate tooling.

The project thus consisted of two main tasks:

  1. to specify and implement a generic prototype on which specific supports environments could be constructed;
  2. to construct some such specific support environments for demonstrations that stress formal reasoning and the integration of the practice of design with the organisation of design.

Chris Wadsworth jointly authored the initial study of requirements and concepts in the area of formal reasoning. He also represented Informatics in the regular project meetings and contributed to the technical reviews.

The Manchester and Informatics part of the project was concerned with formal methods of software development. Formal methods use mathematical specification to capture the user's requirements, and mathematical techniques to verify the correctness of an implementation with respect to the specification. Tools are essential to the development of software by such methods to support the mathematical reasoning and for the management of complex specifications, refinements and proofs.

The Manchester University and Informatics developed a tool to support formal reasoning. The system provided a prototype support environment for the Vienna Development Method (VDM) and a sophisticated proof assistant. The aim was not to provide a fully automatic system but one that provided an assistant to the human responsible for carrying out proof steps who should, through his understanding of the problem, be able to guide the proof process along the right lines. User interface issues were important in such a system and considerable effort was devoted to this in the project. The proof assistant was sufficiently general that it could support any formal method. Juan Bicarregui and Brian Ritchie were the main people from Informatics involved. Brian wrote a review of his Interactive Proof Editor (developed at Edinburgh) for inclusion in the IPSE 2.5 Theorem Proving Review paper.

Both commented on the specification of Muffin, a prototype interactive theorem proving system built at Manchester as a test bed for ideas. Brian used SML to build a rapid prototype of a part of the Muffin prototype formal reasoning tool. Tests on this revealed a flaw in the initial Muffin specification. Later a complete implementation of Muffin was produced in Smalltalk-80 at Manchester.

Informatics concentrated on the design and development of the prototype VDM support environment in the system. Development steps in VDM revolve around finding more concrete representations for the datatypes of the specifications and redefinition of the functions and operations to correspond to these new datatypes. Each step gives rise to proof obligations, theorems which have to be proved to verify that the step is correct.

In 1987, they concentrated on the design of the theory store for the formal reasoning IPSE (FRIPSE). FRIPSE is split into a left hand side, providing specification language support, and the right hand side, providing theorem power support. Initially it was intended that the left hand side and right hand side would communicate through the theory store, but this was eventually felt to be too complex an interface and a simpler interface was designed, and the theory store was accommodated in the right hand side.

Following a reorganisation early in 1988, Informatics was k charged with the design and implementation of a minimal left hand side to use while the fuller version was being implemented.

Design and presentation of a preliminary formal specification of this was completed by mid-1988. A VDM data model was developed to encapsulate the construction of completed design developments of specifications of varying degrees of abstraction linked by reification information (how one specification can be formally viewed as an implementation of another, both through reification of data models and through redesign of operations and functions upon them). This model went through numerous iterations. FRIPSE eventually changed its name to MURAL.

The project aroused considerable interest in the academic and commercial worlds and pointed the way towards tools which would be usable by practising software engineers as well as highly trained mathematicians.

⇑ Top of page
© Chilton Computing and UKRI Science and Technology Facilities Council webmaster@chilton-computing.org.uk
Our thanks to UKRI Science and Technology Facilities Council for hosting this site