Clove (Cress Language-Oriented Verification Environment)
Introduction
This project was initially undertaken by Larry Tan under the supervision of Ken Turner. Clove (Cress Language-Oriented Verification Environment) is a notation and a tool for defining and verifying specification properties.
Clove is independent of the application domain, the target language, and the tools used to support this. (However, its implementation is very Lotos-oriented at present.) Properties are therefore expressed in a neutral notation. They are translated into a suitable target language (Mu Calculus at present) and then model-checked against the specification. Verification results are interpreted in simple tree-like terms, thus avoiding the user having to be familiar with the target language.
Clove has been used in the following major application areas with Lotos (Language Of Temporal Ordering Specification) as the specification language:
Clove has specialised support to verify specifications generated by Cress (Communication Representation Employing Systematic Specification). Clove is also complementary to the validation performed by Mustard (Multiple-Use Scenario Test And Refusal Description).
The following is a condensed description of Clove, using Web Services as a sample problem domain. Clove has also been used to describe verification properties for GS, IVR and PD. See the referenced publications for more details.
The absence, existence, precedence, response and universality properties below are Clove representations of the Mu Calculus properties developed by Radu Mateescu. In turn, these are based on the work of the Specification Patterns project. Each such property can be applied in five modes: after some action (after), after some action and until another (afteruntil), before some action (before), between two actions (between), and globally (global).
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) |
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))
Clove is accompanied by a tool that uses M4 (a macro processor), REGLDG (Regular Expression Grammar Language Dictionary Generator) and Perl (a scripting language) to perform the translation and verification. In addition, Clove needs support for the target language, such as CADP for Lotos and Mu Calculus.
Clove is copyright by the authors and is not open-source. Nonetheless, the authors will normally provide it to others for non-commercial research purposes. See the author's Lotos software page for more information.
Further work planned includes more 'canned' properties for making certain kinds of verification more convenient.
The technical basis of Clove is contained in the following published papers (a subset of those written):
Koon Leai Larry Tan. Case Studies using Cress to develop Web and Grid Services. Technical Report CSM-183, Computing Science and Mathematics, University of Stirling, December 2009.
Koon Leai Larry Tan. An Integrated Methodology for Creating Composed Web/Grid Services. Technical Report CSM-186, Computing Science and Mathematics, University of Stirling, October 2010.
Koon Leai Larry Tan and Kenneth J. Turner. Automated Analysis and Implementation of Composed Grid Services. In Dimitrios Dranidis and Ilias Sakellariou, editors, Proc. 3rd South-East European Workshop on Formal Methods, pages 51-64, Thessaloniki, Greece, November 2007.
Kenneth J. Turner and Koon Leai Larry Tan. A Rigorous Methodology for Composing Services. In Maria Alpuente, Byron Cook and Christophe Joubert, editors, Proc. Formal Methods for Industrial Critical Systems 14, Lecture Notes in Computer Science 5825, pages 165-180, Copyright Springer, Berlin, November 2009.
A number of the papers cited on the Cress home page are also relevant.
Up one level to Ken Turner - Research
Projects