Clove (Cress Language-Oriented Verification Environment)
See the download page about obtaining this under licence
See the download page about obtaining this under licence
The current version of Clove is 1.4, dated 16th March 2012.
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:
Clove creates and verifies properties expressed using a generic property notation. It relies on the cress_common.pm Perl module borrowed from Cress.
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. |
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 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) |
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) |
A few examples are provided with Clove:
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))
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:
initial internal version
adjustments to the Clove notation to make it more convenient and applicative in style
improved diagnostics in the event of property failure
efficient handling of verification when services/processes are interleaved at the top level
numerous small enhancements
addition of support for IVR (Interactive Voice Response) signals, including rendering diagnostics in a Clove-like way
addition of a '-q' option to allow Clove visible macros to be prefixed
the reduction relation specified with '-r' can now be 'none', 'branch' (formerly 'branching'), 'strong' (default), 'taucomp' (tau compression with branching reduction) and 'tauconf' (tau confluence with branching reduction)
addition of a '-x' option and check_exit macro to verify that all paths lead to exit (i.e. there are no deadlocks or indefinite loops)
addition of an inevitable macro that requires the given action(s) to occur at some point on all paths
addition of a possible macro that requires the given action(s) to occur at some point on at least one path
addition of a Sequence macro that allows zero or more internal events between actions in the sequence
properties for always exit, deadlock freedom and livelock freedom now have initial capitals
properties properties are now reported with initial capitals when they are verified
strings for Lotos now have forbidden characters removed: " $ ' ( ) , : ; ? ! [ ] _ ` | =
GS/WS (Grid Service/Web Service) diagnostics are now rendered in a Clove-like way, including failure of a deadlock check
strings for patterns now have fewer forbidden characters removed to allow for metacharacters in regular expressions: " $ ' , : ; ! _ ` =
macro quotes are now guillemets (« ... ») to ease use of {...} in regular expressions
for the top-level behaviour in Cress but non-compositional mode, features other than the current one are removed from the composition (leaving other top-level process calls intact)
features given on the command line are now capitalised on output
the inevitable and possible combinators now take an optional first argument to define the initial behaviour
a list combinator has now been added, much as for Mustard
all function names for structures are now rendered in upper case
boolean constants are now handled in constructors
the DS (Device Service) and SS (Statistics Service) domains are now supported
a configuration file is now not permitted for verification
cress_common.pm is now used for common definitions
verification without an (annotated) CADP file now handled cleanly
Up one level to Lotos Utilities