Systems Engineering Division (SED) was created in July 1988. The main function of SED is the development of software and knowledge engineering techniques of interest to the programme of the Engineering Board of the Science and Engineering Research Council (SERC).
The major objectives of SED are:
The SED has its origins in 1977 when SERC launched its first national information technology programme, the Distributed Computing Systems (DCS) Programme. The DCS Programme was co-ordinated by the Rutherford Appleton Laboratory (RAL) and received both management and technical support from it.
The success of RAL's involvement led to it coordinating the next national programme, the Software Technology Initiative, launched in 1981.
This background explains RAL's subsequent major role in designing and directing the Alvey Software Engineering and Intelligent Knowledge Based Systems (IKBS) Programme.
The technical support work for these Programmes established the basis for the SED collaborative research activities, forming a blend of management, support, research and technology transfer activities.
With the closure of the Alvey Programme, the SED has run down its management and support of national programmes, though it does continue to provide Monitoring Officers for projects funded by national programmes and has built up its research and technology transfer roles. In particular, its research provides a technology input to the Engineering Applications Support Environment (EASE) programme.
The SED is thus currently organised around two main research themes of Software and Knowledge Engineering, with a third strand of evaluating Integrated Project Support Environments (IPSE), methods and tools candidates for the EASE programme.
SED consists of two groups, Knowledge Engineering and Software Engineering.
The concern of knowledge engineering is to "write down descriptions of the world in such a way that an intelligent machine can come to new conclusions about its environment by formally manipulating these descriptions" (Brachman and Levesque). A machine which communicates effectively with a variety of humans will have to use information about what people can be expected to know in various circumstances. Progress towards these goals has led to increased interest in knowledge engineering techniques in recent years for all manner of application domains, from science and engineering to finance. The particular interests of KEG are in the development of methods, tools and techniques in:
These interests are being pursued through a variety of collaborative projects, ranging from international interdepartmental work, through inter-laboratory technology transfer, to formal collaborative projects with UK and European academics and industrialists. The major projects in which the group is involved are described in separate sheets in this series.
SEG is concerned with the development of techniques and methodologies for the specification, construction and maintenance of software systems. Systems engineering is mainly about achieving quality and the overall theme of the Group is "Quality Certification of Software Products". SERC's Engineering Board has a practical requirement for better systems engineering in many of its Programmes.
The main interests of the group are in:
Education and awareness activities, in the area of software engineering methods, tools and environments are undertaken for the Engineering Board's research community and the Group is contributing to the specification and development of the EASE environment.
The interests of the group are also pursued through a range of collaborative projects, which are described in other sheets in this series.
This is a three year project funded by the IEATP. The consortium consists of Royal Holloway and Bedford New College (RHBNC), the University of Glasgow and the Rutherford Appleton Laboratory (RAL) and is 'uncled' by British Telecom (BT).
Formal Methods of specification and verification are a technology which must become more widely used by UK companies if they wish to remain competitive in the long term in areas where such methods are becoming the industry standard. One such area is the formal specification of standards for open distributed systems, and in particular those related to Open Systems Interconnection (OSI) computer network architecture, for which the formal description technique LOTOS (Language Of Temporal Ordering Specification) was adopted as an international standard in 1988. 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.
The underlying goal of this project is to determine the verification requirements for LOTOS specifications and to investigate techniques for discharging those requirements, particularly those based on term rewriting and equational reasoning.
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 focussed 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.
BT is already working on the verification of LOTOS specifications, using existing theorem provers. However, while research has been done on verification for different parts of the language, it has not yet been incorporated into an integrated whole. Term rewriting and equational reasoning are clear candidates for this work, as they are already widely accepted as a verification technology for the major constituents of the language, algebraic specifications and process algebras.
The equational reasoning system ERIL has been developed at RAL, with significant technical research input from RHBNC, and is particularly suited for experimental use as it is easily user configurable to allow experimentation with a wide variety of strategies. While it is felt that, as it stands, ERIL could be of significant use in discharging the verification requirements of LOTOS, the collaborators also believe that a long term research project such as this will allow significant further technical developments.
Therefore, the objectives of the project are
The work in (2), undertaken by RHBNC, will also indicate directions in which the ERIL tool has to be enhanced to serve as a test-bed for these ideas. The development of the ERIL system in the light of this falls to RAL. The developed system will be assessed using examples arising from the case studies in the final year of the project.
The result of the project will be
ZIP is a three year project employing research and development effort from the membership of British Aerospace (Military Aircraft) Ltd. (Lead), BP International Ltd., IBM UK Laboratories Ltd., Logica Cambridge Ltd., Praxis Systems Pic, Rutherford Appleton Laboratory (RAL) and Oxford University Programming Research Group (pRG). Work began on the project on the 1st of February 1990.
The work programme schedules activities for:
The major products of these research and development activities will serve to promote the unification initiative and enhance the state-of-the-art.
The Paralfex project was set up to run in parallel with Alfex, an Alvey community club in financial expert systems. The Alfex Club had two expen systems produced, one for advice on corporate financing (the Source of Finance Adviser) and one as a 'market assessor,' using conventional expert systems technology. The interest of the Paralfex project was in more advanced forms of knowledge representation suitable for explanation of reasoning and conclusions, and to explore this interest the project team had access to the knowledge elicitation transcripts of the Alfex knowledge engineers. The financial domain is significantly different from the medical domain in which much work on architectures for knowledge based systems (KBS) has hitherto been carried out, and it was intended that representations particularly suited to the domain should be developed.
The first goal of the project was to reconstruct the Source of Finance Adviser with a graphical user interface. It is felt that graphics has a great potential in KBS interfaces, though previously it has - in common with many explanation facilities - been aimed mainly at the system implementer and knowledge engineer. Graphics offers a realistic alternative to natural language and 'canned text' interfaces, avoiding many of their problems. A good graphical interface can make it obvious to the user what information is available, so that an explicit request for explanation never has to be formulated: one might say that the explanations are emergent from the structure. Related to this ideal is another, that the system's intelligence as perceived by the user through the interface should closely match its actual intelligence. Both were taken into account when designing the interface for the Source of Finance Adviser.
It is generally acknowledged that adequate explanation of a knowledge-based system's reasoning and conclusions requires that its knowledge be made explicit, and in particular that the distinction between different kinds of knowledge be represented and used appropriately. This recognition was used as the basis for the design of the graphical interface, in that different kinds of knowledge were assigned different and appropriate forms of presentation. The interface form is a modular one, in that within the principles set out there is scope for flexibility to suit different domains. The nodes representing knowledge base entities need not have the form they had for the Source of Finance Adviser; they could be domain-specific icons such as dials or meters, though of course the representation of uncertain conditions is likely to be useful in many domains. The displays of fixed domain relationships have no restriction on their form.
The Source of Finance Adviser and its graphical interface were implemented using the toolkit Inference ART on a Symbolics 3670, taking advantage of the multiple windowing facility, high-resolution graphics and mouse input. In trials with a number of financial experts drawn from the membership of the Alfex Club, the interface was favourably received. In fact, it was considered that this demonstrator, together with the comparative implementations mentioned in Section 4, were the most satisfactory deliverables to the Alfex Club.
It is recognised that knowledge should, as far as possible, be explicit rather than 'compiled out'. There are many examples of the epistemology of knowledge in financial expert systems, eg a Company Health Adviser:
The graphical interface can and does employ different forms of presentation for different types of knowledge. This gives scope for reusability of interfaces. Furthermore. by making knowledge explicit. knowledge reuse becomes possible within .a domain and across domains (structural knowledge IS the ontology within the domain. and high-level control knowledge is available for a general classification problem solver).
MMI2 is a five year research project drawing on 60 man years of effort that started in January 1989 with funding from the CEC under the Esprit initiative. The consortium undertaking the project consists of 2 software companies, 2 universities and 3 research laboratories; that is BIM (Belgium) as lead partner, with Intelligent Software Solutions (Spain), University of Leeds (UK), Ecole des Mines de Saint Etienne (France), SERC/RAL (UK), ADR/CRISS (France), INRIA (France).
The objective of the project is to develop a highly interactive multi-modal interface for human-machine interaction with knowledge based systems. More specifically, the project aims to build a human-machine interface which will:
The interface will provide simultaneous interactive use of modes suitable to support the developed skills of professional users, and natural communication modes well suited for naive users. These modes include:
The natural languages to be used are English, French and Spanish. The English natural language system is that developed in the Esprit I project LOKI by BIM, while the French and Spanish systems will be based on existing developments by ADR/CRISS and ISS respectively.
The Gesture Mode will allow users experienced in character-like domain notations to use mouse gestures rather than either conventional direct manipulation sequences or typed commands. . This mode will also allow users experienced with direct manipulation to use gestures as compound macro operators.
The main research advances are expected be made in the interactive use of the different modes, their integration and intelligent co-operative dialogue management. Integration across four pairs of modes will be researched: between NL and graphics, NL and commands, commands and graphics, graphics and gesture. The core of the interface will consist of modules for:
The interface will initially be developed to accommodate a Prolog based knowledge based system for local and wide area computer network design, which provides the requirement for intelligent dialogue, different classes of users, and the integration of multiple modes of representation and communication. The interface will be designed to be portable across a range of potential applications of knowledge based systems. Tools for the rapid adaptation of the interface will be developed in the later stages of the project.
Within the project the Science and Research Council/Rutherford Appleton Laboratory will be involved in the development of the:
and address problems involving:
The Knowledge Engineering Group of the Informatics Department at the Rutherford Appleton Laboratory (RAL) has begun work on a project for a consortium of Water Companies under the coordination of the Water Research Centre, Swindon. The aim is to develop a pilot knowledge based system for assisting in the operations of water supply and distribution. The project plan calls for a definition phase to identify and clarify a suitable problem, taking into account the needs of all the members of the consortium, followed by a phase of prototyping and the building of a pilot system for one particular site. The pilot will be such that it will then be possible to create a 'platform' a site-independent but domain-specific knowledge base on which further site-specific applications may be built. In this way the usefulness of the system to all members of the consortium will be assured.
Not only will the results of the work be useful to the consortium members, but they are likely to involve some challenging research issues such as representation of network knowledge and its integration with heuristic knowledge, time-constrained reasoning, truth maintenance and user modelling.
At the time of writing, the definition phase has been completed and the scope of the system defined. There are three classes of problem, frequently encountered in water supply and distribution, which the system will be able to assist with: dealing with non-routine abnormal conditions; risk assessment; and resource management. The commonality which exists between aspects of these problems means that a single system will be useful for all of them. The prototyping phase has begun with knowledge acquisition at the selected pilot site, Southern Water at Otterbourne.
In order to make research more effective and to facilitate technology transfer from research programmes, the Science and Engineering Research Council (SERC) strongly encourages the use of standards, wherever appropriate. Computer graphics is widely used in scientific and engineering research as a tool for presenting data and synthetic objects. Graphics standards are therefore important in SERC's support of research programmes and Rutherford Appleton Laboratory (RAL) has been involved in the development of international standards for computer graphics since work commenced in the International Organization for Standardization (ISO) in 1978.
This project is investigating the use of formal specification techniques to describe computer graphics standards.
Work commenced in 1985 with investigations into the applicability of formal specification techniques to the first ISO standard for computer graphics programming, the Graphical Kernel System (GKS). Various techniques were explored including VDM, Z and OBJ. These techniques were applied to subsets of GKS carefully chosen to capture the key concepts and ideas in G KS.
Result,> have been reported in the literature. A paper by Duce and Fielding showed how the graphical output primitives could be described in VDM or Z and a paper by Duce in conjunction with Arnold and Reynolds at the University of East Anglia, presented a framework within which GKS and (by extension) GKS-3D could be described.
The relationship between the GKS standard and the Programmer's Hierarchical Graphics System (PHIGS0 - to be published by ISO/IEC in 1989) has recently been explored and presented as a layered specification in OBJ.
The results of the project continue to be fed into the standards-making process. The work to date has influenced Reference Model activities within ISO/IEC and the presentation of PHIGS. Insights from the project are now forming the basis for some of the UK input to the first 5-year review of GKS.
In joint work with ten Hagen and van Liere at Centrum voor Wiskunde en Informatica (CWI), Amsterdam, a specification of the input model of GKS was given in Hoare's CSP notation. This work formed the basis of a submission to the ISO Study Group on graphical input models and is being extended to show how hierarchically structured input devices can be described.
Duce D A, 'Formal Specification of Graphics Software', in Theoretical Computer Graphics and CAD, Ed. Earnshaw R A, Springer-Verlag, 1987. (This paper contains an overview of the project and references to 1987.)
Duce D A, van Liere, R and ten Hagen P J W 'Components, Frameworks and GKS Input', Proceedings of Eurographics '89, Ed. Hopgood F R A and Strasser, W, North-Holland (1989).
Integrated Project Support Environment (IPSE) 2.5 is the largest project in the Alvey Software Engineering Programme with a total budget of around £1OM, of which the Rutherford Appleton Laboratory (RAL) component is £400K. The RAL component of the project terminated on 31 March 1990. The IPSE 2.5 consortium consists of the following organisations:
The project aims to demonstrate that computer based technology in the form of an IPSE can provide significant assistance towards addressing some of the major issues in system development The project is about IPSEs which integrate the management and control of the development process with the development activities themselves and particularly with development activities based on form fill methods.
The name of the project derives from the fact that the IPSE being constructed lies somewhere between a second generation IPSE (using database technology) and a third generation IPSE (using knowledge base technology).
Rather than providing support for a particular method, IPSE 2.5 aims to provide a generic IPSE which can be instantiated to provide support for particular methods or collections of methods. This is done by describing the development process associated with the method in a process modelling language, PML, and providing appropriate tooling.
The work at RAL is undertaken jointly with the University of Manchester (MU), under the direction of Professor C.B. Jones.
Formal methods of software development are methods which use mathematical specifications to capture the requirements of a design, and verification of design steps to yield implementations that are correct with respect to this specification. A development may involve several layers of specification and the construction of formal proofs of various properties of them and of the relationships between the specifications is a vital part of the method. Each design decision a choice of a particular representation of some abstract datatype or an implementation of an implicit function or operation - gives rise to certain proof obligations to justify the decision in terms of the original specification.
The main aim of the MU/RAL work is to provide an IPSE to support formal reasoning (µral). It is centred around a proof assistant. rather than a fully automated theorem proving tool because the former allows the intuition of the human user, who has an insight into the problem and a feeling why the result is true, to guide the proof process along the right lines.
MU constructed an experimental formal reasoning tool called Muffin as an experiment in user-interface design. The tool was formally specified in VDM and was constructed in the Smalltalk-80 programming system. The user interface in the µral draws extensively on the results of this experiment.
Different formal methods are based on different formal logics. µral provides a logical framework (called FSIP) upon which may be defined the notation, axioms and deduction rules of particular logics.
RAL undertook the design of the theory store for µral. Because an axiom which can be used for reasoning about some particular objects in one context may not be applicable in other contexts, the 'database' of results has to be organized in such a way that those results dealing with the same symbol under the same interpretation are available together. Such a collection of results is called a theory. The theory store allows results to be safely reused.
RAL is also responsible for the construction of a prototype YDM support environment in which YDM specifications can be entered and operation and data refinement steps can be described. The system generates proof obligations corresponding to refinement steps which can then be discharged using the proof assistant
Bicarregui, J C, and Ritchie, B 'Providing Support for the Formal Development of Software', Proceedings of the International Conference on System Development Environments and Factories, Berlin, May 1988.
µral snapshot showing two specifications of an insertion operation (where INSERT1 is 'more concrete' than INSERTO), and the µral generated 'implementabilty' proof obligation for INSERT1.
The project aims to meet the need for better defined and more standard measures for evaluating the Knowledge Based System (KBS) elements of system performance; for standard and systematic guidelines for assessing the suitability of a knowledge-based approach and quantifying its feasibility; and for sound comparative evidence from evaluation to support the case for KBS in preference to some other approach. There are three areas in which evaluation is appropriate and which are to be addressed by the project: system performance (software and hardware considerations), usability (interfaces, maintainability, user motivation, etc.) and organizational effectiveness (relation of the KBS to the milieu in which it operates).
Specifically, the objectives are as follows:
The project will draw on evaluative measures for conventional systems where appropriate and modify them for application to KBS. It will also develop measures for KBS-specific aspects. Software tools will not be developed from scratch but will be employed and evaluated where possible and minor adaptations will be made where appropriate. It is intended that comparative evaluation will lead to some absolute measures, thereby enhancing the predictive power of the methods, which is an important goal because of the need for prediction in the early stages of a system lifecycle when it is necessary to assess the potential for KBS involvement and to present evidence for its effectiveness.
The approach taken will address three aspects of KBS:
There are many aspects of each of the three distinguished facets of KBS performance which could be open to evaluation. The evaluation of some of these will be similar to the evaluation of conventional systems. Other aspects require evaluation measures which will be novel for KBS. The feasibility and usefulness of evaluating these will be investigated in the study phase and those which appear useful will be developed and assessed during the remainder of the project.
The project will consist of six phases:
