Implementation of the FULL Logic using XTL

Organisation:	University of Stirling (SCOTLAND)
Functionality:	Verification of data-based 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 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.
Conclusions:	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.
Publications:	[Bryans-Shankland-01] 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, August 2001. Available on-line at: http://www.cs.stir.ac.uk/~ces/Papers/forte01b.ps or from the CADP Web 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 E-mail: ces@cs.stir.ac.uk
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page