Organisation: 
University of Stirling (SCOTLAND)


Functionality: 
Verification of databased temporal properties of LOTOS programs

Tools used: 
CADP (Construction and Analysis of Distributed Processes)

Period: 
2001

Description: 
The DIET project aims at providing a framework for reasoning
symbolically about full LOTOS specifications (containing both processes
and data values). In this project, a symbolic early semantics for full
LOTOS was developed, which associates a Symbolic Transition System
(STS) to a LOTOS specification. On top of this symbolic interpretation,
an equivalence relation and an adequate modal logic named FULL (Full
Logic for LOTOS) have been defined. The FULL logic provides a way
of expressing properties involving both data and transitions of STSs.
In order to experiment with the logic at an early stage, a
modelchecker for a (subset) of FULL has been developed using the XTL
tool of CADP.
The FULL logic is based upon a variant of HML (HennessyMilner Logic) extended with quantification over data values. FULL was originally interpreted on STSs, but an alternative interpretation over Labeled Transition Systems (LTS), such as those encoded in the BCG format of CADP, can be defined. In these LTSs, data variables are represented by explicitly enumerating all their values. Note that, contrary of what is stated in [BryansShankland01], the CAESAR compiler for LOTOS does not restrict the range of integer numbers between 0 and 255, but allows the user to specify an external implementation of integers on 2 or 4 bytes. The interpretation of FULL on LTSs represented in BCG format enabled to implement a subset of FULL (in which quantification is restricted to finite data domains) using the XTL language (eXecutable Temporal Language) of CADP. XTL is roughly a functionallike language for describing computations over LTSs containing data values. The modal operators of FULL have been implemented as XTL functions that compute the sets of states satisfying these operators. Then, the actual modelchecking is performed using an XTL macro which evaluates the semantics of a modal formula (seen as a functional expression built from calls of the functions associated to the modal operators) and checks if it contains the initial state of the LTS. 
Conclusions: 
XTL allowed a successful implementation of (a subset of) the modal
logic FULL designed for expressing databased temporal properties of
full LOTOS specifications. The CADP toolbox and the XTL tool provide
a very accessible way of building prototype modelcheckers. Further
work directions include the extension of FULL with parameterized
versions of the modal mucalculus fixed point operators, which could
also be defined as recursive functions in XTL.

Publications: 
[BryansShankland01]
Jeremy Bryans and Carron Shankland.
"Implementing a Modal Logic over Data and Processes using XTL".
Proceedings of the IFIP International Conference on Formal
Description Techniques for Networked and Distributed Systems FORTE'2001
(Cheju Island, Korea), pp. 201218, Kluwer Academic Publishers,
August 2001.
Available online at: http://www.cs.stir.ac.uk/~ces/Papers/forte01b.ps or from our FTP site in PDF or PostScript 
Contact:  Dr. Carron Shankland University of Stirling Department of Computing Science and Mathematics Stirling FK9 4LA Scotland Tel: +44 1786 467444 Fax: +44 1786 464551 Email: ces@cs.stir.ac.uk 
Further remarks:  This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software 