Clove (Cress Language-Oriented Verification Environment)

Clove Logo
Cyan Dot Introduction
Cyan Dot Approach
Cyan Dot Clove Literals
Cyan Dot Clove Notation
Cyan Dot Property Examples
Cyan Dot Tool Support
Cyan Dot Future Plans
Cyan Dot Publications

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:

Grid Service Orchestration (GS)
This application supports the orchestration of grid computing services. The target languages are BPEL (Business Process Execution Language), WSDL (Web Services Description Language) and Lotos (Language Of Temporal Ordering Specification).
Interactive Voice Response (IVR)
This application allows interactive but automated conversations over the telephone. The target languages are VoiceXML (Voice XML), Lotos (Language Of Temporal Ordering Specification) and SDL (Specification and Description Language).
Prompting Dialogues (PD)
As a specialisation of IVR, this application supports prompting dialogues for people with cognitive impairment. The target languages are VoiceXML (Voice XML), Lotos (Language Of Temporal Ordering Specification) and SDL (Specification and Description Language).
Web Service Orchestration (WS)
This application supports orchestration of web services for program-to-program over the Internet. The target languages for Cress are BPEL (Business Process Execution Language), WSDL (Web Services Description Language) and Lotos (Language Of Temporal Ordering Specification).

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).

Approach

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

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

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))
  

Tool Support

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.

Future Plans

Further work planned includes more 'canned' properties for making certain kinds of verification more convenient.

Publications

The technical basis of Clove is contained in the following published papers (a subset of those written):

A number of the papers cited on the Cress home page are also relevant.


Up Arrow Up one level to Ken Turner - Research Projects

Web Ken Turner Home   Email    Search Search Web Pages

Last Update: 17th March 2012
URL: http://www.cs.stir.ac.uk/~kjt/research/clove.html