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.
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.
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.
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.
J. Paul Gibson. Formal object-based design in LOTOS. Technical Report CSM-113, University of Stirling, Department of Computing Science and Mathematics, April 1993.
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.
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.
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.
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.
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.
Richard O. Sinnott. The formally specifying in LOTOS of electronic components, M.Sc. thesis, University of Stirling, Scotland, March 1993.
Magdalene S. P. Teo. Component-oriented specification and analysis of communications services, M.Sc. thesis, University of Stirling, Scotland, September 1993.
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.
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.
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 ProjectsLast Update: 15th July 2006