See the download page to obtain this program
Cress is an acronym for Communication Representation Employing Systematic Specification. Cress allows graphical description of a wide variety of services such as in data communications/telecommunications, but Cress is not limited to this. The approach allows services to be described graphically as (work)flows of activities. Cress diagrams are automatically translated into formal languages for rigorous analysis and verification, and are also automatically translated into implementation languages for deployment and validation.
Cress was mostly developed by Ken Turner of Computing Science and Mathematics at the University of Stirling. Larry Tan made substantial contributions to the support of grid/web services, including their verification/validation and implementation. Dean McMenemy developed support for the Call Processing Language. Jamie Boyd implemented the core of the Chive diagram editor.
The aim of Cress has been to make service design as easy as possible without requiring specialist development knowledge. For the service designer, Cress simplifies service creation to drawing diagrams, clicking buttons and defining a few tool parameters. All key functions of Cress can be controlled from the Chive diagram editor.
The Cress compilers accept diagrams in a number of source formats (Chive, Diagram! and yEd). Depending on the application domain these are translated into a variety of target languages depending on the application domain (BPEL/WSDL, CPL, Lotos, SDL, VoiceXML).
Cress is written using portable and widely used languages (Perl and Java). It can be extended by a developer for other kinds of services that can be characterised by activity flows. The following kinds of services are already supported:
The Cress Tool Suite provides the following main tools, each with its own documentation and software:
Internally, Cress has the form of a compiler with a preprocessor (for various diagram formats), a lexical analyser (to check basic diagram elements), a parser (to check syntactic and static semantic correctness) and a code generator (for various target languages). The flow through Cress is as follows:
The following is a brief illustration of Cress notation, using Intelligent Network telephony services as an example application. Cress has also been used to describe many other kinds of services.
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 arc 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 graphical description of POTS (Plain Old Telephone Service). To understand it fully would need more investigation of Cress.
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 (e.g. for POTS), 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.
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 (Intelligent Network 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 Intelligent Network.
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-defined services can optionally be formally analysed through verification (checking the formal correctness of a service specification) and through validation (checking the formal correctness of a service implementation). This requires the service diagrams to be automatically translated into a formal language: Lotos (Language of Temporal Ordering Specification) or SDL (Specification and Description Language).
The following diagram illustrates the approach to formal verification and validation, here for a web service translated to a Lotos specification and implemented in BPEL/WSDL:
For verification, Clove (Cress Language-Oriented Verification Environment) is used to automatically verify the correctness of Cress specifications through model-checking desirable properties. Clove takes 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 through formal validation. For example, Clove can prove properties of a specification in general and not just check specific test cases (as in validation). 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. It automatically translates verification properties into RAFMC (Regular Alternation-Free Mu Calculus), and verifies them against a Lotos specification. Where properties do not hold, counterexamples are presented in simple tree form.
For validation, Mustard (Multiple-Use Scenario Test And Refusal Description) is used to automatically validate the correctness of Cress services. Tests are applied automatically, and any failures or inconclusive results are also diagnosed automatically. In effect this is like unit testing using specific tests. Services can be checked in isolation and also in combination. It is in this latter case that dynamic interactions among services may appear. As well as detecting design flaws, this also allows 'feature interactions' to be detected dynamically.
For validating specifications, the Mustard tool automatically translates and checks validation tests. This is useful for any kind of service but particularly for feature-based services (e.g. in telephony). When features are combined with a root service (e.g. POTS) they may interfere with each other. Formal validation allows their compatibility to be checked.
For validating implementations, Mint (Mustard Interpreter) is used to automatically validate the correctness of Cress-generated implementations. In theory a verified specification should result in a correct implementation. In practice a number of issues may arise such as performance problems, low-level resource conflicts, or errors in the implementation infrastructure. It is therefore useful to formally validate the generated implementation. Mint is used specifically for grid and web services, where it checks that Mustard-defined tests are respected by the network-based implementation.
Cress-defined services are automatically translated to an implementation. What constitutes an implementation depends on the application domain:
This program is free software. You can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation - either version 2 of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful but without any warranty, without even the implied warranty of merchantability or fitness for a particular purpose. See the GNU General Public License for more details.
You may re-distribute this software provided you preserve this description of the Cress Tool Suite. Bug reports should be sent to Ken Turner, who would also appreciate receiving any corrections and comments.
The technical basis of the Cress Tool Suite 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. Orchestrating Grid Services using BPEL and Globus Toolkit 4. In Madjid Merabti, Rubem Pereira, Carol Oliver and OmarAbuelma'atti, editors, Proc. 7th PGNet Symposium, pages 31-36, ISBN 1-902560-13-9, School of Computing, Liverpool John Moores University, Liverpool, UK, June 2006.
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. Formalising the Chisel Feature Notation. In Muffy H. Calder and Evan H. Magill, editors, Proc. Feature Interactions in Telecommunication Networks VI, pages 241-256, IOS Press Amsterdam, May 2000.
Kenneth J. Turner. Modelling SIP Services using CRESS. In Moshe Vardi and Doron Peled, editors, Proc. Formal Techniques for Networked and Distributed Systems (FORTE XV), Lecture Notes in Computer Science 2529, pages 162-177, Copyright Springer, Berlin, November 2002.
Kenneth J. Turner. Representing New Voice Services and Their Features. In Daniel Amyot and Luigi Logrippo, editors, Proc. Feature Interactions in Telecommunication Networks VII, 123-140, IOS Press, Amsterdam, June 2003.
Kenneth J. Turner. Formalising Graphical Service Descriptions using SDL. In Rick Reed and Jeanne Reed, editors, Proc. SDL 2003, Lecture Notes in Computer Science 2708, 183-202, Copyright Springer, Berlin, Germany, July 2003.
Kenneth J. Turner. Specifying and Realising Interactive Voice Services. In Harmut Koenig, Monica Heiner and Adam Wolisz, editors, Proc. Formal Techniques for Networked and Distributed Systems (FORTE XVI), Lecture Notes in Computer Science 2767, 15-30, Copyright Springer, Berlin, September 2003.
Kenneth J. Turner. Analysing Interactive Voice Services (pre-publication version), Computer Networks, 45:665-685, Copyright Elsevier Science Publishers, Amsterdam, March 2004.
Kenneth J. Turner. Formalising Graphical Behaviour Descriptions, Proc. 10th International Conference on Algebraic Methodology and Software Technology, 537-552, Copyright Elsevier Science Publishers, Amsterdam, March 2004.
Kenneth J. Turner. Validating Feature-Based Specifications, Software Practice and Experience, 36(10):999-1027, August 2006 (pre-publication version, copyright John Wiley).
Kenneth J. Turner. Device Services for The Home, In Khalil Drira, Ahmed Hadj Kacem and Mohamed Jmaiel, editors, Proc. 10th Int. Conf. on New Technologies for Distributed Systems, 41-48, Copyright IEEE Computer Society, Los Alamitos, California, USA, June 2010.
Kenneth J. Turner. Representing and Analysing Composed Web Services using CRESS (pre-publication version), Network and Computer Applications, 30(2):541-562, Copyright Elsevier Science Publishers, Amsterdam, April 2007.
Kenneth J. Turner and Koon Leai Larry Tan. Graphical Composition of Grid Services. In Didier Buchs and Nicolas Guelfi, editors, Proc. International Conference on Rapid Introduction of Software Engineering Techniques, Lecture Notes in Computer Science 4401, pages 1-17, Copyright Springer, Berlin, May 2007.
Kenneth J. Turner and Koon Leai Larry Tan. A Rigorous Approach to Orchestrating Grid Services. Computer Networks, 51(15):4421-4441, Copyright Elsevier, Amsterdam, October 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.
See the individual tools for their own history. For the complete Cress Tool Suite the release history is as follows:
Version 1.0: First SourceForge Version, Ken Turner, 12th July 2016