This project is being undertaken by Ken Turner with contributions on web/grid service verification from Larry Tan. Mustard (Multiple-Use Scenario Test And Refusal Description) is a notation and a tool for specifying and validating test scenarios. Scenarios may have behaviour that is sequential or parallel, deterministic or non-deterministic, and dependent on features or choices. Acceptance tests (things that must happen) and refusal tests (things that must not happen) can also be specified.
Mustard is independent of the application domain, the target language, and the tools used to support this. Test scenarios are therefore expressed in a neutral notation. Tests are translated into the target language of the system being validated and are executed in this environment. Test results are interpreted in terms of the Mustard notation, thus avoiding the user having to be familiar with the target language.
Mustard has been used in the following major application areas:
Mustard use-case scenarios can be used to validate descriptions written for Cress (Communication Representation Employing Systematic Specification). Mustard is also complementary to the verification performed by Clove (Cress Language-Oriented Verification Environment).
The following is a condensed description of Mustard, using telephony and SIP (Session Ininitiation Protocol, i.e. Internet Telephony) as an example problem domain. Mustard has also been used to describe validation scenarios for DS, GS, IN, IVR, PD, SIP and WS. See the referenced publications for more details.
Mustard literals are as follows:
|£7, L13.25, $67.12, D25.00||currency ('£'/'$' converted to 'L'/'D' internally)|
|@2005 10 04, @10-04, @04||date ('-', '/', space removed)|
|=mark.dta/mark_check.dta, =merge.spss||file to be checked (expect 'mark.dta'/'merge.spss', check contents against 'mark_check.dta'/'.merge.spss')|
|0, +9, -3.14||number|
|:6091, :467 000 x 7423, :801-9134||phone ('-', '+', space removed)|
|'What arrival date?, '45||string (forbidden characters " $ ' ( ) , : ; ? ! [ ] _ ` | removed)|
The core Mustard notation is as follows:
|// text||explanatory comment (removed during translation, use '%%' for literal '//')|
|« text »||quoted text (not subject to translation)|
|call(feature,scenario)||invokes behaviour of another scenario; the feature name is optional, defaulting to the current feature|
|decide(behaviour)||non-deterministic (scenario-decided) choice of alternative behaviours|
|depend(condition,behaviour,...)||behaviour depends on whether the condition holds; an optional final behaviour acts as an `otherwise' case|
|exit(behaviour)||sequential behaviour with normal termination|
|interleave(behaviour)||concurrent execution of behaviours|
|offer(behaviour)||deterministic (system-decided) choice of alternative behaviours|
|present(feature)||holds if the feature is present in the system|
|read(signal,parameters)||inputs a signal from the system; the variant Read absorbs other signals before the desired one is input|
|refuse(behaviour)||sequential behaviour with abrupt termination if the final behaviour occurs, or successful termination if not|
|send(signal,parameters)||outputs a signal to the system; the variant Send absorbs other signals before the desired one is output|
|sequence(behaviour)||sequential behaviour with abrupt termination|
|succeed(behaviour)||sequential behaviour with successful termination|
|test(name,behaviour)||defines a test for the given name and behaviour|
A scenario has a name (which is automatically qualified by the current feature). As an example, the following is a test for a SIP proxy. It defines a simple sequence of events: address 1 goes off-hook, receives dial tone, and goes on-hook. If the specification respects this sequence, a pass verdict is recorded for the scenario.
test(No_Dial, test of call without dialling succeed( successful sequence send(OffHook,1), 1 goes off-hook read(Announce,1,DialTone), 1 gets dial tone send(OnHook,1))) 1 goes on-hook
The following scenario introduces a choice. After address 1 dials address 4, the outcome depends on the status of 4. If this is a valid number, it will start ringing from 1; but if it is an invalid number, then 1 will receive an 'unobtainable' message. The offer combinator allows a deterministic (system-decided) choice. This is appropriate here, as only the system knows whether the callee can be rung.
test(Ring_Or_Unobtainable, test of ring or unobtainable succeed( successful sequence send(OffHook,1), 1 goes off-hook read(Announce,1,DialTone), 1 gets dial tone send(Dial,1,4), 1 dials 4 offer( system choice read(StartRing,4,1), 4 rings from 1 read(Announce,1,Unobtainable)))) 1 gets unobtainable
It is sometimes desirable to use the decide combinator for a non-deterministic (scenario-decided) choice. This ensures that all alternatives are explored.
The depend combinator makes a scenario conditional; the dependency is evaluated when the scenario is defined, not when it is executed. Dependencies are most commonly used when the specification has features. For example, a scenario can be varied according to the features that have been provisioned. The following tests the feature CFBL (Call Forward on Busy Line), deployed in either a user agent or a proxy. Call forwarding is handled differently in each case: a called user agent will announce a temporary change of number to the caller, while a proxy will automatically re-route the call. The following scenario depends on which feature has been deployed.
test(Busy_Forward, test of forward on busy succeed( successful sequence send(OffHook,1), 1 goes off-hook read(Announce,1,DialTone), 1 gets dial tone send(OffHook,3), 3 goes off-hook read(Announce,3,DialTone), 3 gets dial tone send(Dial,1,3), 1 dials 3 depend( feature dependency present(AGENT_CFBL), agent forwarding present? .., behaviour for agent forwarding present(PROXY_CFBL), proxy forwarding present? ...))) behaviour for proxy forwarding
Scenarios can also be made finer-grained, depending on whether a feature applies to a particular pair of users.
Scenarios often begin in similar ways. It is undesirable if the same opening behaviour has to be repeated. Instead, opening sequences can be defined as scenarios that are called by other scenarios.
Many specification problems arise due to concurrency, for example race conditions. It is desirable to check if a specification suffers from these kinds of problems. This requires scenarios that independently execute multiple behaviours in parallel (i.e. through interleaving). In the following example, addresses 1 and 2 concurrently go off-hook and dial address 3. The outcome depends on the system, so there is a system-defined choice: 3 starts ringing from 1, and 2 receives busy; or 3 starts ringing from 2, and 1 receives busy. Note how sequence is used to group the interleaved and alternative behaviours.
test(Raced_Calls, test of simultaneous calls succeed( successful sequence interleave( concurrent behaviour sequence( sequence send(OffHook,1), 1 goes off-hook read(Announce,1,DialTone), 1 gets dial tone send(Dial,1,3)), 1 dials 3 sequence( plus sequence send(OffHook,2), 2 goes off-hook read(Announce,2,DialTone), 2 gets dial tone send(Dial,2,3))), 2 dials 3 offer( system choice sequence( sequence read(StartRing,3,1), 3 rings from 1 read(Announce,2,BusyHere)), 2 gets busy sequence( or sequence read(StartRing,3,2), 3 rings from 1 read(Announce,1,BusyHere))))) 1 gets busy
Refusal tests express what a system must not do. Since the purpose of call screening is to block calls, it might be preferable to state this explicitly in a refusal test. If it is known that address 2 screens calls from address 1, then calls from 1 must not ring 2. The behaviour to be refused is the last parameter of refuse, here the act of ringing 2 from 1.
test(Screen_Caller_Refusal, test of caller refusal refuse( refusal sequence Send(OffHook,1), 1 eventually goes off-hook read(Announce,1,DialTone), 1 gets dial tone send(Dial,1,2), 1 dials 2 Read(StartRing,2,1))) 2 must eventually not ring from 1 (refusal)
Mustard is accompanied by a tool that uses M4 (a macro processor) and Perl (a scripting language) to perform the translation and validation. In addition, Mustard needs support for the target language, such as Lola/Topo (for Lotos), Telelogic Tau SDL Suite (for SDL/MSC) or ActiveBPEL (for BPEL/WSDL).
When validating web/grid services, Mustard is complemented by Mint (Mustard Interpreter). Mint takes Mustard scenarios translated into a simpler representation and executes them against a deployed web/grid service. This allows the functionality and performance of the service implementation to be checked, especially under load conditions.
Mustard 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 Lotos software page for more information. The associated Mint tool is provided on the same basis.
Further work planned includes automatic derivation of useful test scenarios using annotations on the system description.
The technical basis of Mustard 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. Analysing Interactive Voice Services Computer Networks, 45:665-685, Copyright Elsevier Science Publishers, Amsterdam, March 2004 (pre-publication version, copyright Elsevier).
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 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.
Other papers cited on the Cress home page are also relevant.
Up one level to Ken Turner - Research ProjectsLast Update: 29th May 2012