Clove (Cress Language-Oriented Verification Environment)

Clove Logo

See the download page about obtaining this under licence

Contents

The current version of Clove is 1.4, dated 16th March 2012.

Overview

Clove is a language and a tool for defining and verifying specification properties. Although Clove was designed for use with Cress, it can be used independently of Cress. See the Clove home page for an overview of Clove. See the Cress home page for an overview of Cress.

Clove has been used to verify services in the following domains:

Clove verifies specifications written in:

Tools

Clove creates and verifies properties expressed using a generic property notation. It relies on the cress_common.pm Perl module borrowed from Cress.

Installation

To run Clove requires Perl 5, M4 (macro processor) and CADP (Construction and Analysis of Distributed Processes). Clove has been run on Windows (XP and 7, under CygWin) but should also run on Unix (Linux, Macintosh).

A Unix-like installation is assumed in the following, though it should be possible to install and run on other platforms where Perl and CADP run. It is assumed that the files are extracted to $HOME/bin/clove.

In a few places in the code, a Unix-like environment is assumed. For example, Macintosh end-of-line may not be correctly handled. Paths and filenames are assumed to have '/' separators. Search paths are assumed to have ':' separators. On a Windows system, it is suggested that CygWin be used; ActivePerl may be suitable but has not been tried.

The following environment variables should be set up (e.g. in your .profile, .cshrc or Windows XP environment variables):

Variable Meaning
CADP (used by CADP) a directory path used to locate the CADP installation
CRESSTEMP (used by Clove) a directory for temporary files (/tmp by default)
M4PATH (used by M4) a colon-separated, Unix-like directory path used to locate M4 macro files, e.g. .:$HOME/bin/clove/m4; if you are using Windows, you will not be able to cite drive letters unless you use CygWin references such as /C/home/me/bin/clove.
PATH (used by command-line) shell search path (no default), e.g. to include $HOME/bin/clove/bin
PERLLIB (used by Perl) a directory path used by Perl to locate modules (cress_*.pm), e.g. $HOME/bin/cress/bin.

Clove

This script takes a filename on the command line. 'file[.lotos]' should contain a Lotos specification (typically one generated by Cress and annotated for CADP). The feature names in this are automatically extracted. The main file can optionally be followed by feature or service names to restrict verification to these.

For each such a feature/service (e.g. LENDER), the location of its diagram is found (e.g. directory $HOME/bin/cress/ws/lender). If a Clove file does not exist (e.g. lender.clove), verification of this feature/service is not performed.

If there is such a verification file, it must contain declarations and properties defined in the Clove property language. Declarations are translated into C header files for CADP, while properties are translated into Mu Calculus. The properties are then model-checked automatically, with output/diagnosis of success or failure.

Command-line options are:

Option Meaning
-b break specification down compositionally (no breakdown by default)
-c suppress Cress mode (Cress mode by default)
-d suppress deadlock freedom check (checked by default)
-e level use the given error reporting level (3 - panics, 2 - these plus errors, 1 (default) - these plus notes, 0 - these plus diagnostics)
-h print help
-i suppress initials safety check (checked by default)
-l suppress livelock freedom check (checked by default)
-m manual verification (automatic by default)
-p show BCG progress (close window when done, default none)
-q qualifier qualifying prefix for visible macros (empty by default)
-r relation reduction relation: none, branch (formerly branching), strong (default), taucomp (tau compression with branching reduction) and tauconf (tau confluence with branching reduction)
-t language target language (lotos by default)
-u user iteration exists in 'file.f' (generated from Clove by default)
-v vocabulary use the named vocabulary (default is the basic filename ignoring any '_' suffix, e.g. file 'ws.lot' has vocabulary 'ws', file 'gs_matcher_scorer.lot' has vocabulary 'gs')
-x perform exit check (not checked by default)

For verification, multiple verification files are created in a temporary directory for each top-level service: '*.custom' for custom enumerations, '*.f' for property enumerations, '*.lotos' for the main Lotos file, '*.mcl' for Mu Calculus properties, '*.svl' as a verification script, '*.t' for type enumerations. For automatic verification, a log file is also created as <service>.log in this directory; verification files are deleted on successful completion.

The script assumes certain formats for a Lotos specification (these rules are respected by Cress):

Lotos Meaning
features: FEATURE1 FEATURE2 names of included features
features: SERVICE1/PARTNER1,PARTNER2 SERVICE2 SERVICE3/PARTNER3 services and associated partners

Clove Literals

Clove literals are as follows:

Clove Meaning
?Type any value
0, -0, +9, -56 natural
0, +9, -3.14, 42., .3 number (decimal places right-extended to six, e.g. -3.140000)
\'(Ken|Larry), \[248]0\.0, \?String, \1 regular expression (each stored for reference as \1, \2, etc.)
'Ken Turner, '15, ' string (forbidden characters " $ ' ( ) , : ; ? ! [ ] _ ` | removed)

Clove Notation

The core Clove notation is as follows:

Clove Meaning
// text explanatory comment
« text »: quoted text (not subject to translation)
absence(mode,action,..) the absent action does not occur according to the given actions: after (absent, after), afteruntil (absent, first, last), before (absent, last), between (absent, first, last), global (absent)
always(action,...) the actions must happen after a finite number of steps
and(action1,action2) both actions occur
any_digit, any_integer, any_natural, any_number, any_string, any_type(type) a regular expression that defines the corresponding kind of value in an action
any_signal, any_signals any action(s)
any_state any system state
choice(action,..,) a choice of alternative actions
existence(mode,action,..,) the present action occurs according to the given actions: after (present, first), afteruntil (present, first, last), before (present, last), between (present, first, last), global (present)
exists(actions[,state]) after actions defined by the first formula, some state exists to satisfy the second formula (if given)
forall(action,state) after actions defined by the first formula, every state must satisfy the second formula (if given)
inevitable([initial,]final) all paths lead to the given final actions (optionally starting with the given initial actions)
initials(action,...) the initial actions of the system
list(type,value,...) returns a list (array) of values of the given type
literals(type,value,...) literal values of type natural, number, string or structure
not(action) the action does not occur
or(action1,action2) either action occurs
patterns(type,value,...) regular expressions defining pattern values of type natural, number, string or structure; the regular expression format is that of REGLDG (Regular Expression Grammar Language Dictionary Generator)
possible([initial,]final) a path leads to the given final actions (optionally starting with the given initial actions)
precedence(mode,action,..,) the later action follows earlier one according to the given actions: after (later, earlier, first), afteruntil (later, earlier, first, last), before (later, earlier, last), between (later, earlier, first, last), global (later, earlier)
property(name,expression) a named property that must hold, defined in terms of the other combinators
Property(name,expression) a named property that must not hold, defined in terms of the other combinators
records(type,parameter) recorded values for type natural, number, string or structure; the effect depends on the parameter: 1 (recording starts for values used in properties), 0 (recording stops), empty (recorded values are produced)
response(mode,action,..,) the request action is followed by the response action according to the given actions: after (request, response, first), afteruntil (request, response, first, last), before (request, response, last), between (request, response, first, last), global (request, response)
sequence(expression,..,) a sequence of actions
Sequence(expression,..,) like sequence, but zero or more internal events are allowed between each action
signal(parameter,..,) an action; for web/grid services, the first parameter is service.port.operation and the second parameter is an action value; for a fault, the second parameter is the fault name and the third parameter is an optional fault value; regular expression metacharacters are escaped in the values
Signal(parameter,..,) similar to signal, but regular expression metacharacters are not escaped in the values (because they are expected to be present)
universality(mode,action,..,) the universal action always occurs according to the given actions: after (universal, first), afteruntil (universal, first, last), before (universal, last), between (universal, first, last), global (universal)

Property Examples

A few examples are provided with Clove:

broker.clove
sample declarations and properties for verifying the Cress car broker
lender.clove
sample declarations and properties for verifying the Cress lender
supplier.clove
sample declarations and properties for verifying the Cress car supplier

The following declaration says that initially the only action possible is a request (partner 'lender', port 'loan', operation 'quote', value any 'Proposal').

  initials(
    signal(lender.loan.quote,?Proposal))
  

The following declaration defines the acceptable patterns for structures (records). The first pattern defines a proposal with name 'Ken Turner' or 'Larry Tan', address 'Scotland', and amount '5000.' or '7000.'. The second pattern defines a proposal with name 'Nancy Smith', address 'Stirling UK' or 'Stirling USA', and amount '9999.'.

  patterns(structures,
    proposal('(Ken Turner|Larry Tan),'Scotland, [57]000\.),
    proposal('Nancy Smith, 'Stirling U(K|SA), 9999\.))
  

A property has a name (which is automatically qualified by the current feature). As an example, the following is a property for a lender. Literally it says that, globally, a request (partner 'lender', port 'loan', operation 'quote', value any 'Proposal') will lead to the corresponding response (a loan rate of any 'Number' or a fault 'Refusal' with value any 'String'). More simply, it says that a proposal request always results in a response with a loan rate or a loan refusal fault.

  property(Any_Loan_Response,
    response(global,
      signal(lender.loan.quote,?Proposal),
      choice(
	signal(lender.loan.quote,?Number),
	signal(lender.loan.quote,Refusal,?String))))
  

The following property also applies to a lender. Literally it says that, successfully, forall states after any signals there is a response (partner 'supplier', port 'car', operation 'order', value any 'Need'). More simply, it says that from any state it is always possible to reach a point where a need request can occur.

  property(Always_Need_Request,
    succeed(
      forall(
	sequence(
	  any_signals,
	  signal(supplier.car.order,?Need)))))
  

If properties share common expressions, these can be defined as macros. The following defines loan rates for a lender that could be used in the definition of several response properties.

  define(Loan_Rates,
    signal(lender.loan.quote,3.5),
    signal(lender.loan.quote,3.7),
    signal(lender.loan.quote,4.1),
    signal(lender.loan.quote,4.4))
  

Licence

This is not open-source software. The authora (Larry Tan and Ken Turner, University of Stirling) retain copyright in it. Nonetheless, the authors will normally approve its use by others subject to the following conditions:

History

Version 1.0: Larry Tan, 20th April 2009

Version 1.1: Ken Turner, 23rd April 2010

Version 1.2: Ken Turner, 11th October 2010

Version 1.3: Ken Turner, 27th October 2010

Version 1.4: Ken Turner, 16th March 2012


Up arrow Up one level to Lotos Utilities

Web Ken Turner Home   Email    Search Search Web Pages

Last Update: 18th July 2016
URL: http://www.cs.stir.ac.uk/~kjt/software/lotos/clove.html