Cress (Communication Representation Employing Systematic Specification)

Cress Logo

See the download page about obtaining this software

Cyan Dot Introduction
Cyan Dot Approach
Cyan Dot Validation
Cyan Dot Verification
Cyan Dot Tool Support
Cyan Dot Future Plans
Cyan Dot Publications

Introduction

This project is being undertaken by Ken Turner. Larry Tan has been a major contributor to the work on Grid/Web Services. Dean McMenemy developed support for the Call Processing Language.

Cress (Communication Representation Employing Systematic Specification) is a notation and set of tools for graphical specification and analysis of features. Cress is designed as a flexible notation for describing and combining services and features. It is graphical in order to improve its attractiveness to an industrial audience. Automated tool support has been developed to check the correctness of diagrams and to translate them into various formal languages and implementation languages. The toolset is portable and can run on a variety of platforms with a variety of front-end diagram editors and back-end target languages.

Cress was initially loosely based on the Chisel notation developed by BellCore for describing telephony features. An important reason for choosing Chisel as the basis is that it was developed to meet industrial needs. As far as practicable, Cress is a strict (though substantial) extension of Chisel. This means that practically any Chisel diagram can be used with Cress, although it is highly desirable to use the new capabilities of Cress.

Cress has been used in a number of distinct application areas:

Device Service Orchestration (DS)
This application supports programmable logic for managing device input and output events. This is performed through a proxy that maps device events in OSGi (Open Services Gateway initiatve) to/from SOAP calls. The target languages in this application are BPEL (Business Process Execution Language), WSDL (Web Services Description Language) and Lotos (Language Of Temporal Ordering Specification).
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).
Intelligent Networks (IN)
This application models services/features in the Intelligent Network (ITU Q.1200 series). The target languages are Lotos (Language Of Temporal Ordering Specification) and SDL (Specification and Description Language).
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. This work in in conjunction with the Guide project. The target languages are VoiceXML (Voice XML), Lotos (Language Of Temporal Ordering Specification) and SDL (Specification and Description Language).
Session Initiation Protocol (SIP)
This application deals with signalling and Internet telephony (RFC 3261). The target languages are Lotos (Language Of Temporal Ordering Specification) and SDL (Specification and Description Language).
Voice over Internet Protocol, i.e. Internet Telephony (VoIP)
This application deals with call control in Internet telephony (RFC 3880). The target languages are CPL (Call Processing 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).

Cress has a tightly defined notation that is translated automatically into formal specifications (Lotos, SDL) and implementations (BPEL/WSDL, CPL, VoiceXML). Cress descriptions may be validated by use-case scenarios defined using Mustard (Multiple-Use Scenario Test And Refusal Description). Cress descriptions may also be verified to model-check properties defined using Clove (Cress Language-Oriented Verification Environment).

A different approach by the author to service creation is that of Anise (Architectural Notions In Service Engineering).

Approach

The following is a very condensed description of Cress, using telephony and IN (Intelligent Network) services as an example problem domain. Cress has also been used to describe services for Device Services, Grid Services, Interactive Voice Response, Session Initiation Protocol, Voice over Internet Protocol and Web Services. See the referenced publications for more details.

A Cress diagram is a graph of nodes linked by arcs. A basic node has a number and an associated event, e.g. 1 Off-hook A to indicate subscriber A picking up the phone. A node carries a signal such as Off-hook and optional parameters like A.

Nodes are classified as inputs or outputs (as far as the system being specified is concerned). A composite node may contain several events in parallel, but these must be all inputs or all outputs. Each event may be associated with explicit assignments. These are normally separated by '/'. Cress expressions allow the usual kinds of arithmetic, comparison, logical and set operators.

The arcs linking nodes may be plain or may carry a condition on what follows. If the branches of a choice are not guarded in this way, the decision is determined by the events that follow. Conditions are either boolean expressions or event triggers. An arcs may be associated with assignments separated by '/'.

A large diagram may be split over several pages. Each section is lettered (to avoid confusion with the numeric node labels). An arrow symbol points to the next diagram section, which begins with this target label.

The variables used by a diagram are defined explicitly. In addition to diagram variables, Cress supports status variables that capture globally significant information. For example, a phone call needs to know if the called party is busy or not.

A rule box provides a formal definition of how variable values are changed by events. Although the assignments triggered by an event can be written explicitly after the event, this clutters a diagram and becomes repetitious. Instead, Cress allows rules to be formulated for assignments. Other kinds of rules may be given for variable initialisation, expression rewrites (macros), and signal transformations.

As an example of the Cress notation, here is a slightly simplified graphical description of POTS (Plain Old Telephone Service). To understand it fully would need more investigation of Cress.

Cress POTS Description

The Cress notation mentioned so far describes the flow among service actions. Where Cress makes a significant contribution is in its capabilities for defining and combining features. A feature describes how it is inserted into another diagram. Typically this is the root diagram, although features may modify features. If features depend on each other hierarchically, the subsidiary diagrams are imported automatically. Feature behaviour may be inserted into another diagram through template instantiation or through splicing.

Cress permits features to be defined as templates. The initial feature node defines the event that may trigger it. For each matching trigger in the root diagram, an instance of the feature is inserted. The template is copied with substitution of actual parameters and placed after the triggering node in the root diagram.

The following shows CND (Calling Number Delivery) as a feature template. This allows the destination to see the number of the caller. The plus in the triggering node ('1+') starts a template that is appended to the matching node: CND event 1 will match any node in the root diagram that contains a Start Ringing event with two parameters. P and Q are formal parameters of the template, matched to the actual parameters in the triggering event. If the number being rung has caller display (CallingNumber P), the number of the caller (Q) will be displayed: CND event 2. After this, or if the destination does not have caller display, the call progresses as normal.

Cress CND Description

When a feature is to be spliced it defines its attachment point in the root diagram. This source node gives the diagram name and node number. Here is a relatively complex example of a spliced feature. INTL (IN Teen Line) is spliced into POTS. The idea of INTL is that use of the phone between certain hours requires a PIN to be entered (e.g. to prevent teenagers from calling within peak hours). This feature makes use of signals between the telephone switch and the SCP (Service Control Point, as used in the IN).

The INTL feature is defined to replace POTS node 1 and its transition to node 2: the initial off-hook progressing to dial tone, as shown below. When the phone goes off-hook, the SCP is alerted: INTL events 1 and 2. If INTL is not enabled for this phone or for the current time, the SCP allows the call to continue: INTL event 13, POTS event 2. Otherwise a voice message M1 (e.g. 'Enter PIN') is provided by the SCP and announced to the user: INTL events 3 and 4. The user may hang up and abort the call attempt: INTL events 5 and 6. Alternatively, the user may dial a PIN in the form of a phone number A1: INTL event 7. The PIN is sent as a resource value to the SCP. If the PIN is correct, the SCP allows the call to continue: INTL event 13, POTS event 2. Otherwise the SCP causes a voice message M2 (e.g. 'Wrong PIN') to be announced, and the call is forcibly terminated: INTL events 9 to 12.

Cress INTL Description

Validation

Cress is accompanied by a scenario language called Mustard (Multiple-Use Scenario Test And Refusal Description). This allows service validation tests to be formulated and applied rigorously. Services can be checked in isolation and also in combination. It is in this latter case that dynamic interactions among features may appear. Tests are applied automatically, and any failures or inconclusive results are also diagnosed automatically. As well as detecting design flaws, this also allows feature interactions to be detected dynamically.

The Mustard tool automatically translates validation scenarios into Lotos or MSCs, and runs them in parallel with a specification. When features are combined individually with a root diagram, this merely confirms the validity of the scenarios. More importantly, the scenarios can be run against the root diagram combined with all features. A common interpretation of feature interaction is that a feature fails to perform as expected when other features are present. The manifestation of feature interaction when using Mustard is either deadlock or non-determinism. Deadlock means that one feature prevented another from working; for example, CNDB (Calling Number Delivery Blocking) prevents CND from working - a desired interaction! Non-determinism means that an ambiguity arose; for example, flash-hook is used by both CW (Call Waiting) and TWC (Three-Way Calling).

Verification

Larry Tan has created the complementary tool Clove (Cress Language-Oriented Verification Environment) for formal verification of Cress designs through model-checking desirable properties. Clove is patterned after Mustard in that it takes files of verification properties and checks them against a (Lotos) specification. Because Clove employs verification, the kinds of things it can check are rather different from those checked by Mustard. For example, Clove can prove properties of a specification in general and not just check specific test cases (as used by Mustard). Clove can also check generic properties such as freedom from deadlock and livelock.

Although model-checking offers the promise of 'push-button' verification, it requires highly specialised and mathematical expertise to use it effectively. It also requires expert knowledge of the specification language and the tools that support this. Clove aims to hide many of these details. The Clove tool automatically translates verification properties into Regular Alternation-Free Mu Calculus (RAFMC), and verifies them against a Lotos specification. Where properties do not hold, counterexamples are presented in simple tree form.

Tool Support

Cress is accompanied by a substantial toolset: roughly 34000 lines of source code and 30 modules. Cress is provided with roughly 80 sample service/feature specifications. In total the toolset consists of roughly 1800 files.

The toolset is copyright by the author and is not open-source. Nonetheless, the author will normally provide it to others for non-commercial research purposes. See the author's graphical software page for more information.

Cress can be used with three diagram editors, though the recommended one is Chive (Cress Home-grown Interactive Visual Editor).

Cress has automated tool support for the translation of service/feature specficiations into various target languages. Through Mustard, automation is also provided to validate services/features. Most of the Cress tools are written in Perl, so they are very portable. The toolset has been used unchanged on three different operating systems.

A target language framework is created using the target development environment. The framework provides the architecture in which the services/features are embedded. Since the framework is fixed for a given domain and target language, it is provided as standard - only the services/features need be specified.

The tool architecture is as follows. The boxed area represents the Cress tools; the tools outside this box are provided by others.

Cress Tools

Future Plans

In future work, the author intends to apply techniques he developed from protocol conformance testing to derive use-case scenarios automatically. Another avenue to be explored is the use of symbolic model-checking to verify that feature properties are preserved in the presence of other features. The current validation approach checks properties only for specific parameters. Model-checking should allow such properties to be proved in general.

Cress has demonstrated its generality in many somewhat different application domains. It is believed that it is readily extensible to new ones.

Publications

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

In addition, the following papers are relevant:


Up Arrow Up one level to Ken Turner - Research Projects

Web Ken Turner Home   Email    Search Search Web Pages

Last Update: 18th July 2016
URL: http://www.cs.stir.ac.uk/cress/cress.html