SPLICE (Specification using LOTOS for an Interactive Customer Environment)

Introduction

This eighteen-month project was funded by EPSRC under grant H/80811 from August 1992 to March 1994. The main activities were to develop a method with computer support for turning functional requirements into formal specifications written in LOTOS, and to explore how to explain formal specifications to different levels of users. The project was undertaken by Paul Gibson and Ashley McClenaghan under the supervision of Ken Turner. See the separate final report for more details of the results.

Objectives

The principal aim of the project was to bridge the gap between the customer, the specifier and the designer in specifying requirements. The objectives of SPLICE were:

to develop a method for using the internationally-standardised formal specification language LOTOS (Language Of Temporal Ordering Specification, ISO 8807) to capture software requirements in a specification
to design prototype software tools for turning functional requirements into formal specifications written in LOTOS
to investigate a method and prototype tools for explaining formal specifications to different levels of users, using animation of specifications and graphical interfaces to communicate the essence of specifications.

Initial Surveys

Investigations were made of a number of areas in which requirements capture and animation could be undertaken. The problem domains studied were layered communications systems, digital logic design, neural networks and reactive systems. Relevant concepts for requirements capture in these areas were studied, leading to a strategy for tackling them from an architectural point of view.

Existing LOTOS tools were also studied. The two toolsets available to the investigators were those produced by the ESPRIT SEDOS project and the ESPRIT LOTOSPHERE project. Although the LOTOSPHERE toolset, called LITE, was more recent and more advanced, it was still being developed during the lifetime of SPLICE and was somewhat unstable. The decision was therefore taken to use the SEDOS tools, using hippo as a `LOTOS calculator' within the SPLICE tools.

Requirements Capture Method

A language SAGE (Service Attribute Generator) was defined to allow compact formulation of service requirements from a customer point of view. SAGE provides the building blocks (facilities) needed to define services in a modular and natural way. In addition, SAGE provides a range of combinators for building higher-level services from lower-level services and facilities. A specification component library was developed for SAGE, and also a translation tool that turns a SAGE specification into a LOTOS specification. The resulting LOTOS specification can be simulated in order to demonstrate its behaviour to the customer requiring the new service.

A language DILL (Digital Logic In LOTOS) was defined to allow requirements for digital logic to be specified and animated in a component-based fashion. The DILL approach parallels the SAGE approach in having a specification component library, a tool to translate DILL specifications into LOTOS, and simulation of the resulting specifications. The composition and synchronisation features of LOTOS allow specification components to be `wired up' very easily.

The specification of neural networks and their design from requirements are active areas of research, and a new application for LOTOS. Library components were developed to support specification of aspects such as neurons, layers of neurons, fan-out units, etc. Learning functions, connectivity functions, neural states, etc. were modelled using the abstract data type facilities of LOTOS.

Reactive systems were chosen as the final area for study from the point of view of requirements definition. A language SOLVE (Specification using an Object-oriented, LOTOS-based, Visual language) was defined in order to allow requirements for reactive systems to be formulated. A rather basic library of specification components was developed, and used to model requirements for systems such as a VCR (Video Cassette Recorder) on-screen clock controller. SOLVE specifications are translated automatically into LOTOS and are then animated graphically. A set of tools supports this animation in a visual, user-oriented fashion.

Object-Oriented Requirements Capture and Analysis

The most promising means of easing requirements capture and specification was felt to lie in formal object-oriented approaches. Apart from the work on SOLVE (which was more animation-oriented), effort was invested in developing a LOTOS-based method for requirements capture and analysis using object-oriented principles. This is the method called ORCA (Object-oriented Requirements Construction and Analysis) that supports various kinds of static analysis (based on diagrammatic representations) and dynamic analysis (through animation). Requirements capture and analysis methods tend to be analyst-oriented, allowing only limited customer involvement. The ORCA method was designed to be customer-oriented, allowing full involvement of customers at all stages. Apart from customer orientation, ORCA is object-oriented, formal, visual and constructive.

Customer orientation allows a flexible approach to analysis; a rigid framework was felt to discourage customers from communicating their needs effectively. ORCA also avoids the traditional emphasis on documentation as a basis for determining requirements, which can lead to isolation of the customer and the analyst. Instead, ORCA allows direct customer involvement in requirements definition. In particular, ORCA allows customers to alter the way in which requirements are presented so that they can be interpreted more readily in problem domain terms.

Object orientation allows requirements to be modelled in a natural way, i.e. natural to the customer. Although object-oriented and object-based techniques are widely used, there is a surprising variability in the way that even fundamental concepts are treated. Part of the project work was to develop a consistent framework of object-oriented concepts and to give these a precise basis. ORCA is also formal. The method is underpinned by LOTOS, such that the end result of requirements analysis is a requirements specification in LOTOS. This offers the expected benefits of precision, analysability, and a foundation for tool support. Other work on the project concerned with animating requirements specifications in LOTOS complements ORCA.

ORCA is supported by various forms of visualisation. Graphical notations in requirements analysis are normal, but ORCA adds the extra ingredient of a formal basis for its graphical representations. A number of graphical views can be presented of requirements. These include navigation around large graphs, browsing and selection of classes, and choosing different views of the same structure (dynamic/static, hierarchical/flat). The same information can be presented with differing graphical emphasis, the intention being to allow the customer to see the requirements in the most appropriate form. This is done by defining mappings between the formal definitions of classes and how they might appear graphically. The range of mappings is provided by the analyst for selection by the customer.

Communication of Specifications

The project carried out pilot studies to address these problems. The SOLVE approach uses graphical presentation and manipulation to convey the meaning of a specification. Unlike other approaches, SOLVE's primary concern is to deal with formal specifications. As well as use with reactive systems, SOLVE was also developed to allow requirements for digital logic circuits to be specified and animated; in this form the approach is known as XDILL (X-based Digital Logic In LOTOS).

SOLVE is designed to be used by people who are not familiar with formal languages (in particular LOTOS). It allows formal requirements specifications to be written using a simple object-oriented language, and to be explored using interactive animation. SOLVE is suitable for requirements capture in problem domains where systems are interactive (producing feedback in response to user input) and can be represented by visual animation. SOLVE has been tried out on a number of simple systems such as a VCR controller.

SOLVE allows the analyst to write a requirements specification in an intuitive, object-oriented language that is then automatically translated into LOTOS. The LOTOS translation is graphically animated, allowing the customer, analyst or designer to explore the requirements specification by interacting with it directly (e.g. by clicking or dragging object icons).

A key feature of SOLVE is visualisation. Each object is visualised as an icon. An object is responsible for displaying and modifying its own icon. An object icon can change to represent an abstraction of the state of an object or some part of the total system. The object icons visually inform the SOLVE user of what is happening in the system. Each simple SOLVE object is created with all the characteristics of a basic prototypical object. Once an object has been created it may be customised. In fact the specifier may build up a kit of predefined simple and composite objects.

Tool Design

Both SAGE (for layered communications systems) and DILL (for digital logic) are supported by specification component libraries. There is a tool for each language that translates it into LOTOS so that specifications can be animated. The specification libraries are actually complex macro packages written in the {\it m4} language and translated into LOTOS by the {\it m4} macro processor. The approach is simple but surprisingly powerful. Compact requirements declarations in SAGE or DILL are translated into LOTOS specifications that are 20 to 40 times larger. This gives some idea of the productivity gains possible in producing formal requirements specifications. The tool libraries also support specification component re-use, and allow the user to work at a more architectural level during requirements definition.

Publications

Article J. Paul Gibson. Formal object-based design in LOTOS. Technical Report CSM-113, University of Stirling, Department of Computing Science and Mathematics, April 1993.

Article J. Paul Gibson. A LOTOS-based approach to neural network specification. Technical Report CSM-112, University of Stirling, Department of Computing Science and Mathematics, May 1993.

Article J. Paul Gibson. Formal object-oriented development of software systems using LOTOS. Technical Report CSM-114, University of Stirling, Department of Computing Science and Mathematics, September 1993.

Article Ashley McClenaghan. Distributed systems: Architecture-driven specification using extended LOTOS. Technical Report CSM-120, University of Stirling, Department of Computing Science and Mathematics, December 1993.

Article Ashley McClenaghan. SOLVE: specification using an object-oriented, LOTOS based, visual language. Technical Report CSM-115, University of Stirling, Department of Computing Science and Mathematics, January 1994.

Article Ashley McClenaghan. XDILL: An X-based simulator tool for DILL. Technical Report CSM-119, University of Stirling, Department of Computing Science and Mathematics, April 1994.

Article Richard O. Sinnott. The formally specifying in LOTOS of electronic components, M.Sc. thesis, University of Stirling, Scotland, March 1993.

Article Magdalene S. P. Teo. Component-oriented specification and analysis of communications services, M.Sc. thesis, University of Stirling, Scotland, September 1993.

Article Kenneth J. Turner. An engineering approach to formal methods. In Andre A. S. Danthine, Guy Leduc, and Pierre Wolper, editors, Proc. Protocol Specification, Testing and Verification XIII, pages 357-380. North-Holland, Amsterdam, Netherlands, June 1993. Invited paper.

Article Kenneth J. Turner and Richard O. Sinnott. DILL: Specifying digital logic in LOTOS. In Richard L. Tenney, Paul D. Amer, and M. Umit Uyar, editors, Proc. Formal Description Techniques VI, pages 71-86. North-Holland, Amsterdam, Netherlands, 1994.

Article Kenneth J. Turner and Ashley McClenaghan. Visual animation of LOTOS using SOLVE (extended version). In Dieter Hogrefe and Stefan Leue, editors, Formal Description Techniques VII, Amsterdam, October 1994. North-Holland.

Up one level to Ken Turner - Research Projects

Last Update: 15th July 2006
URL: https://www.cs.stir.ac.uk/~kjt/research/splice.html