After introducing the LOTOS language and related formalisms, the thesis continues with a survey of approaches to verification of concurrent systems with a view to identifying those approaches suitable for use in verification of properties of systems specified using LOTOS. Both general methodology and specific implementation techniques are considered. As a result of this survey, two useful approaches are identified. Both are based on the technique of expressing the correctness of a LOTOS specification by comparison with another, typically more abstract, specification. The second approach, covered later in the thesis, uses logic for the more abstract specification. The main part of the thesis is concerned with the first approach, in which both specifications are described in LOTOS, and the comparison is expressed by a behavioural equivalence or preorder relation. This approach is further explored by means of proofs based on the paradigm of equational reasoning, implemented by term rewriting.

Initially, only Basic LOTOS (i.e. the process algebra) is considered. A complete (i.e. confluent and terminating) rule set for weak bisimulation congruence over a subset of Basic LOTOS is developed using RRL (Rewrite Rule Laboratory). Although fully automatic, this proof technique is found to be insufficient for anything other than finite toy examples. In order to give more power, the rule set is supplemented by an incomplete set of rules expressing the expansion law. The incompleteness of the rule set necessitates the use of a strategy in applying the rules, as indiscriminate application of the rules may lead to non-termination of the rewriting. A case study illustrates the use of these rules, and also the effect of different interpretations of the verification requirement on the outcome of the proof.

This proof technique, as a result of the deficiencies of the tool on which it is based, has two major failings: an inability to handle recursion, and no opportunity for user control in the proof. Moving to a different tool, PAM (Process Algebra Manipulator), allows correction of these faults, but at the cost of automation. The new implementation acts merely as computerised pencil and paper, although tactics can be defined which allow some degree of automation. Equations may be applied in either direction, therefore completion is no longer as important. (Note that the tactic language could be used to describe a a complete set of rules which would give an automatic proof technique, therefore some effort towards completion is still desirable. However, since LOTOS weak bisimulation congruence is undecidable, there can never be a complete rule set for deciding equivalence of terms from the full LOTOS language.) The composition of the rule set is re-considered, with a view to using alternative axiomatisations of weak bisimulation congruence: two main axiomatisations are described and their relative merits compared. The axiomatisation of other LOTOS relations is also considered. In particular, we consider the pitfalls of axiomatising the cred preorder relation.

In order to demonstrate the use of the PAM proof system developed, the case study, modified to use recursion, is re-examined. Four other examples taken from the literature, one substantial, the others fairly small, are also investigated to further demonstrate the applicability of the PAM proof system to a variety of examples.

The above approach considers Basic LOTOS only; to be more generally applicable the verification of properties of full LOTOS specifications (i.e. including abstract data types) must also be studied. Methods for proving the equivalence of full LOTOS specifications are examined, including a modification of the technique used successfully above. The application of this technique is illustrated via proofs of the equivalence of three variants of the well-known stack example. The proofs are carried out by hand as neither of the implementation tools used above are able to handle data types. The approaches of other authors to verification of full LOTOS specifications are also described and illustrated by examples in order to propose an approach to verification comprising several complementary techniques.

Finally, the verification of LOTOS specifications where the abstract requirements are expressed using temporal/modal logic is briefly considered. Specific reference is made to the existing linear temporal logic used in conjunction with LOTOS and also to the use of HML (Hennessy-Milner Logic) in conjunction with CCS. The possibility of using HML with Basic LOTOS is discussed at length, with examples drawn from earlier in the thesis. Also considered is the possibility of extending the logic for use with full LOTOS. Both of these proposals require further investigation.

Research

Teaching

CV

Personal

Home

Email: ces@cs.stir.ac.uk