Cress (Communication Representation Employing Systematic Specification)
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:
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).
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.
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.
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 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).
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.
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.
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.
The technical basis of Cress 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.
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. Formalising Graphical Behaviour Descriptions, Proc. 10th. International Conference on Algebraic Methodology and Software Technology, 537-552, Copyright Elsevier Science Publishers, Amsterdam, March 2004.
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. 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.
In addition, the following papers are relevant:
Kenneth J. Turner. An Architectural Foundation for Relating Features. In Petre Dini, Raouf Boutaba and Luigi Logrippo, editors, Proc. Feature Interactions in Telecommunication Networks IV, pages 226-241, IOS Press, Amsterdam, June 1997.
Nikolaos Kosmas and Kenneth J. Turner. Requirements for Service Creation Environments. In Ignac Lovrek, editor, Proc. 2nd International Workshop on Applied Formal Methods in System Design, pages 133-137, Zagreb, June 1997.
Kenneth J. Turner. Relating Services and Features in the Intelligent Network. In Marijan Kunstic, editor, Proc. 4th International Conference on Telecommunications, pages 235-243, Zagreb, June 1997.
Kenneth J. Turner. Validating Architectural Feature Descriptions using LOTOS. Proc. Feature Interactions in Telecommunication Networks V, pages 1389-1419, IOS Press, Amsterdam, September 1998.
Kenneth J. Turner. An Architectural Description of Intelligent Network Features and Their Interactions (pre-publication version), Computer Networks and ISDN Systems, Petre Dini and Luigi Logrippo, editors, Special Issue on Feature Interactions in Telecommunications Software, 30(15):1389-1419, September 1998.
Kenneth J. Turner. Realising Architectural Feature Descriptions using LOTOS. Parallel Computers, Networks and Distributed Systems (Calculateurs Parallèles, Réseaux et Systèmes Répartis), Editions Hermès, Paris, August 2000.
Up one level to
Ken Turner - Research Projects