DIET: Developing Implementation and Extending Theory A Symbolic Approach to Reasoning about LOTOS

Extract from the Case for Support

Contents:

• Background
• Programme in Detail

Our experience over a range of applications [KT95] has shown that LOTOS is most appropriate for constructing systems, i.e. describing concrete properties and how the system performs its tasks. We have also identified a need for a more abstract expression of what the system should do. A better formalism for this purpose is a modal or temporal logic. The logic can be combined with a proof system which validates formulae with respect to process algebra descriptions, thus we maintain LOTOS for the concrete and adopt a logic for the abstract. Each language is used in its most appropriate way.

Given the close relation of the process algebra part of LOTOS and CCS, it is relatively straightforward to adapt applications of logic with CCS to the LOTOS setting. Our previous work [Kir:95] reports on this.

When Full LOTOS is considered several problems arise. Consider the process B = g?x:S; B', meaning accept a value x of sort S at gate g, then behave as B'. In order to simplify the synchromisation model the standard semantics of LOTOS gives meaning only to processes with ground data; the semantics is in terms of structured labelled transition systems. This means that query events do not correspond to a single transition, but rather a set of transitions, one for each possible ground instance of the query variable(s). So in our example there is a transition B - g v -> B' for each value v of sort S (i.e. each for each equivalence class in the associated initial algebra). The implication of this semantics is that a query event offer is equivalent (with respect to strong bisimulation) to an infinite choice over all values of the data type, e.g. in?x:Nat;P is equivalent to in!0;P [] in!1;P [] in!2;P [] ...

While the advantage of this semantics is that it easily accomodates multi-way synchronisation between any number of processes (CCS only allows two-way synchronisation), it can result in infinite transition systems (both in depth and breadth) which are difficult to reason about. Moreover, by embedding the data values in the actions, we lose two desirable features: clear indication of uniformities in the actions of the processes, and the ability to describe and reason about partial specifications, i.e. open behaviour expressions.

To overcome this problem with the concrete nature of the semantics, we have defined a symbolic semantics for LOTOS in terms of symbolic transition systems [ST97]. To facilitate reasoning about these systems we also defined a related modal logic. The symbolic approach allows reasoning about data to be separated from reasoning about processes (the latter is our primary interest); we assume the existence of some oracle which will report the validity of predicates on the data. In reality this oracle will be implemented by some other proof system.

This separation of concerns allows us to reason about open processes (where the process or action parameters are uninstantiated). Parameterised processes are desirable because code only has to be written once at an abstract level, rather than several times at a more concrete level, thus allowing less opportunity for errors. We also only have to carry out any analyses once.

To this point the main thrust of the work has been theoretical, although we have carried out a small telecommunications-based case study. The uptake of a particular description technique or proof method is crucially dependent on the availability of tools to automate the specification and analysis process, and on the quality of those tools. There are several tools which can aid the specifier in writing a LOTOS specification, for example syntax and semantics checkers, pretty printers, simulation tools, and testing tools. There are also tools to check the validity of formulae of various forms of logic with respect to a model described using LOTOS. For example, the CADP tools in which Full LOTOS specifications (with some syntactic restrictions) are translated into labelled transition systems, instantiating free variables by all possible data values, and the validity of alternation-free modal µ-calculus formulae is checked with respect to that labelled transition system. No symbolic values are permitted in the logical formulae.

Clearly, although a desirable and powerful logic is used here, the specifications do not retain their symbolic nature. This problem is overcome, to some extent, in Eludo.

Here, the validity of CTL formulae is checked with respect to Full LOTOS specifications. The variables in the LOTOS remain symbolic; predicates about the variables are built up as the model is explored and narrowing is used to obtain concrete values where possible. The (non-standard) semantics of LOTOS used here has not yet been formalised (other than by the Prolog rules of the implementation) nor compared with the standard semantics. This approach does allow us to use unmatched query variables over infinite types; however, CTL cannot describe the cyclical properties we ultimately desire. (Although only finite properties are considered in [ST97], the current proposal seeks to extend the expressivity of the logic.)

Since no current tools satisfactorily approach the problem of reasoning about symbolic LOTOS specifications, we propose to develop a tool of our own. It is possible, and indeed desirable, that our tool will be based on one of the tools mentioned above, or on a more general tool, VPAM, which is designed for symbolic algebraic manipulation of value passing processes, but does not implement model checking. Reuse of existing tools is good software engineering practice, and will also allow us to use the other facilities provided by those tools (such as automatic syntax and semantics checking). In addition, our experience with applications of LOTOS have also shown that it is useful to have a variety of verification, validation and testing methodologies at our disposal. For example, simulation is useful to gain early confidence in the correctness of a description.

Lastly, although LOTOS is useful at certain levels of abstraction for describing systems, sometimes other features are needed to make it more applicable in a particular field. E-LOTOS (Enhanced LOTOS) offers important new features which will improve its usability in many areas; in particular, a new data type description language, more modularity, the addition of timed operations, and a more expressive synchronisation mechanism. These features reflect extensive industrial trials and applications.

Since E-LOTOS is a proposed international standard, and the modifications to LOTOS are so significant, it is important to extend the theory developed in [ST97] and the implementation of the symbolic model checker to include features of E-LOTOS. There are no such tools to support system development with E-LOTOS at present.

Programme and Methodology

1. Implementation of a symbolic model checker for LOTOS and logic of [ST97].
2. Extensions:
   1. Extension of theory of logic to operators from the µ-calculus. Extension of symbolic semantics of LOTOS to include features of E-LOTOS.
   2. Corresponding extension of implementation of symbolic model checker.
Case Studies:
1. Case Study 1 (existing theory only)
2. Case Study 2 (exploiting use of E-LOTOS features)
3. Case Study 3 (exploiting use of µ-calculus operators)
4. Case Study 4 (no special remit)
3. Final evaluation of theory and of implementation.

See the workplan for a schematic representation of the tasks and deliverables involved in the proposal.

The student will be responsible for the implementation work and for three of the case studies. These activities will be guided by the experience of Drs Shankland and Thomas. The theoretical extension to the logic will be carried out by Drs Shankland and Thomas, and the extension to E-LOTOS will be carried out by all participants. Drs Shankland and Thomas will carry out one case study. Smaller case studies may also be carried out by any of the participants during the lifetime of the project.

Task 1: will be to develop an implementation of a symbolic model checker based on the theory in [ST97]. Initially the student will be expected to carry out a more detailed study of the existing LOTOS tools described in the previous section, in order to evaluate the possibility of using one of these as the framework for this implementation. A small case study will also be carried out at this point in order to familiarise the student with LOTOS and with the symbolic logic.

Task 2a: While the implementation is being carried out, Drs Shankland and Thomas will collaborate on the theoretical extensions to the logic and symbolic semantics (to bring in fixed point operators of the modal µ-calculus, and features of E-LOTOS). The student will input experience gained through implementation to these this task.

Task 3a: After successful implementation of the tool the student will carry out a small case study to evaluate the practicalities of applying the method to real problems, and to evaluate the usability and usefulness of the model checker. The case study will be drawn from one of several sources (see below).

Task 2b Before embarking on larger, more detailed case studies the student will collaborate on Task 2 (theory extensions), followed by implementation extensions to reflect the theoretical extensions.

Tasks 3b, 3c \& 3d: Three more case studies will be tackled, two by the student, the remaining one by Drs Shankland and Thomas, drawn from the following fields:

Communications protocols

This is a traditional area of application for process algebra, LOTOS especially. Examples will be selected from new developments such as multimedia, high-speed networks and adaptive protocols. Dr Thomas has strong links with British Telecom through her feature interaction work, and it is possible that this may be a source of case study material.

Distributed systems

Again, a traditional area of application for LOTOS. Examples will be selected from distributed system architectures (ANSA, ODP), distributed objects (CORBA, DOLE), distributed information retrieval and distributed system management. The Persistent Systems group at Stirling has strong links with Iona (a company specialising in distributed systems), a possible source of case study material.

Hardware-software co-design

This is a relatively new area for LOTOS, although process algebras (especially CCS) have been used to describe hardware. These examples will particularly address the integration of hardware and software design. Timing issues will be important here, making the use of E-LOTOS essential.

Existing studies in the literature

It will be important to look at problems which have already been tackled too, in order to evaluate the effectiveness of our approach, and to evaluate the effectiveness of model checking as a proof technique. This will be a form of bench-marking for the project.

The student will be supported in these case studies by the pool of experience at both Stirling and Glasgow in applications of formal methods, particularly LOTOS, and in the implementation of distributed systems. Depending on the nature of the case studies it may be appropriate in the case studies to employ other approaches to verification of LOTOS specifications, or perhaps validation approaches, thus providing an opportunity for direct comparison of the methodology developed in this project and existing methodologies.

Task 4: Finally, the outcomes of the case studies and the project as a whole will be evaluated with respect to other means of verifying/validating/testing LOTOS specifications.

The final evaluation will also include an evaluation of the model checker, and feed back into further development.

The student will be expected to complete his/her PhD thesis during this time.

Research

The Diet Project

Home

Email: ces@cs.stir.ac.uk