University of Stirling (SCOTLAND)
Verification of data-based temporal properties of LOTOS programs
CADP (Construction and Analysis of Distributed Processes)
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
model-checker for a (subset) of FULL has been developed using the XTL
tool of CADP.
The FULL logic is based upon a variant of HML (Hennessy-Milner 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 [Bryans-Shankland-01], 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 functional-like 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 model-checking 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.
XTL allowed a successful implementation of (a subset of) the modal
logic FULL designed for expressing data-based temporal properties of
full LOTOS specifications. The CADP toolbox and the XTL tool provide
a very accessible way of building prototype model-checkers. Further
work directions include the extension of FULL with parameterized
versions of the modal mu-calculus fixed point operators, which could
also be defined as recursive functions in XTL.
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. 201-218, Kluwer Academic Publishers,
Available on-line at: http://www.cs.stir.ac.uk/~ces/Papers/forte01b.ps
or from our FTP site in PDF or PostScript
Dr. Carron Shankland
University of Stirling
Department of Computing Science and Mathematics
Stirling FK9 4LA
Tel: +44 1786 467444
Fax: +44 1786 464551
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|