Guide to Verification and Testing

This page is an introductory user guide to the Broker@Cloud Verification and Testing Tool Suite. These tools were developed for the EU FP7 Broker@Cloud project, to support the continuous quality assurance objective.

The Broker@Cloud Verification and Testing Tool Suite is offered both as an online service and as a download bundle, to be integrated with your own Cloud service development framework. The following instructions describe how to get started with the downloaded version of the tools and assume you have downloaded and installed the software following instructions given in the Download Centre. To explore the online demonstration, please follow the trail through specification, validation, verification and test generation for Cloud software services.

The overall goal of of the EU FP7 Broker@Cloud project is to provide new methods and mechanisms for continuous quality assurance for enterprise cloud service brokers. The expectation is that many more software vendors will become involved as cloud ecosystem partners, offering competing services on brokered platforms. Keeping track of standards and quality in this rapidly expanding market is challenging. Some of the Broker@Cloud tools offer support for the governance of the service lifecycle, to ensure that offered services meet the expectations of brokerage platforms.

The verification and testing tools provide a measure of functional quality control, to ensure that offered services meet certain specification standards and can be used interchangeably with other services meeting the same standards. The standard for a service is developed as a service specification, which can be checked by tools (verification) and from which exhaustive test-suites may be generated automatically (testing), to ensure that aspiring instances of the service are actually compliant to the specification. The benefits of this approach include:

• standard service specifications - these apply a gentle standardising force to the way in which services are designed and developed, which will in the future support the creation of many interoperable services.
• automatic validation - allows the designer to validate a specification to ensure that the states and transitions of the service correspond intuitively to the way they want the service to behave.
• automatic verification - allows the designer to verify the specification for consistency and completeness, in particular to ensure that every specified operation is deterministic and non-blocking.
• automatic test generation - allows the designer to generate technology-neutral test-suites that completely cover the states and transitions of the specification and all equivalence-partitions of its operations.
• automatic test grounding - allows the designer to select technology-specific translations of test-suites into executable JUnit test libraries for Java, SOAP or REST services (with POJO, JAX-WS or JAX-RS Java clients).

Further kinds of test grounding to other formats are possible, if you wish to extend our framework, which offers a standard Visitor Pattern style of translator.

The Broker@Cloud Verification and Testing Tool Suite (VTTS) supplied in the download bundle is designed to be consumed in several different ways, according to preference. To find out more about each of these ways of launching the tools, please create the Javadoc documentation from the source code distribution, which has detailed navigable guidance on all aspects of usage. The tools are offered as:

• command-line programs - Java main programs executable in the JRE 7 runtime, that accept all parameters on the command-line, then read and write XML files; these are found in the main package: uk.ac.sheffield.vtts.
• Java Swing demonstrator - a Java Swing GUI that has four tabs to execute the four main tools as a standalone application, reading files and displaying formatted output; this is found in the package: uk.ac.sheffield.vtts.gui.
• back-end CGI programs - Java programs designed to be launched by CGI scripts, that read web form parameters on standard input, read XML via URLs and display XML in a web browser; these are found in the package: uk.ac.sheffield.vtts.web.

All of the tools expect to consume and produce XML files, a format chosen for ease of transmission, and to allow both human- and machine-processing of the results (but the test grounding tool generates Java source code as output). By default, they use the folder-structure of the distribution to store further generated files. There are separate folders for XML documents, generated Java test-drivers and Java service clients (further subdivided into POJO, JAX-WS and JAX-RS flavours).

Cloud Service Specification

The starting point for developing high-quality cloud services is to develop a model specification for what the service is expected to do. Conceptually, a specifcation is a combination of a finite state machine, expressing the different responsive modes of the service in which certain operations are available or unavailable, and a functional protocol expressing the equivalence-partitioned behaviour of each operation, according to different specified input or memory conditions.

A specification is developed as an XML document that conforms to the Broker@Cloud standard schema for service specifications: https://staffwww.dcs.shef.ac.uk/people/A.Simons/broker/ServiceSchema.xsd (which is maintained on the Sheffield website). Since developing a specification may be a new venture for some, we have developed a Guide to Writing Service Specifications which explains the concepts and develops a specification in stages. Otherwise, the software distribution comes with several example service specifications that progressively introduce more aspcts of the specification language:

• xml/Login.xml - is a simple two-state login service, mainly to show the design of the state machine;
• xml/Account.xml - is a two-state bank account service that offers banking operations that update memory variables;
• xml/ContactList.xml - is a three-state example that mimics the selection behavior of GUIs with list insertion and deletion;
• xml/HolidayBooking.xml - is a three-state vacation booking service that also introduces stronger conditions;
• xml/ShoppingCart.xml - is a four-state shopping service with a strong modal flavour and introducing symbolic types;
• xml/DocumentStore.xml - is a complex versioned document storage service, with symbolic types and server exceptions.

Cloud Service Validation

Validation is a semi-formal human inspection process in which aspects of the specification are reflected back to the designer, to help determine whether the right design has been developed. This is done by checking the completeness of the state machine for the cloud service and reporting back to the designer, who may then decide whether further states or transitions are desired in the design. There is no right or wrong answer; but the designer should be able to determine whether the state machine for the service should handle, or ignore particular events in each state.

The validation tool checks the completeness of a service's state machine (it checks statically whether each event is explicitly handled by a specified transition in every state). The tool reads the XML file containing the service specification in XML format. It writes machine-readable output in XML format, describing the state machine with extra annotations indicating the analysis of states and transitions.

java uk.ac.sheffield.vtts.ValidateMachine <specFile.xml>

If the input file can be read, the output will be an XML file containing the analysed state machine specification (otherwise an error message will be displayed). The root Machine node will contain a Notice node, which may contain further Analysis or Warning nodes. A Warning is issued if any states cannot be reached in the machine, or if known events are not handled by the machine. These are faults in the specification that should be rectified. An Analysis is issued if any state ignores certain events. This is not necessarily a fault, and is provided for information.

A Notice is then also attached to each State node, giving an Analysis of which events are ignored by that state. A state may legitimately choose to ignore certain events; but the analysis allows you to check that events are handled as you really intend. The Warning is repeated for each unreachable state, as a reminder.

Cloud Service Verification

Verification is a formal process in which a specification is checked for completeness and consistency. This is done by checking each operation, to ensure that whatever the current state of variables in memory, and whatever values are supplied as inputs, there will always be one path that is executable. The verification process uses symbolic evaluation to determine possible partitions in the input space and symbolic subsumption to check which path is enabled. The verification process can detect whether the specification contains nondeterminism (more than one path enabled) or blocking (no path enabled) for particular inputs and states.

The verification tool checks the completeness of a service's protocol (it checks statically whether single branches exist for each logical input and memory condition of each operation). The tool reads the XML file containing the service specification in XML format. It writes machine-readable output in XML format, describing the service protocol with extra annotations indicating the analysis of input/memory partitions and whether the specified operations cover all of these cases.

java uk.ac.sheffield.vtts.VerifyProtocol <specFile.xml>

If the input file can be read, the output will be an XML file containing the analysed protocol specification (otherwise, an error message will be displayed). The root Protocol node will contain a Notice node, which may contain further Analysis or Warning nodes. An Analysis node is issued if the memory is correctly initialised and each operation is found to be deterministic. A Warning node is issued if the memory is not fully initialised, or operation inputs are not all bound, or known events are not handled by the protocol specification. A Warning is also issued if an operation is found to be blocking (unable to respond), or non-deterministic (able to respond ambiguously) under certain inputs. These warnings indicate faults in the specification that should be corrected.

Cloud Service Test Generation

Model-based testing is a formal process in which all the paths through a specification are systematically explored to generate all possible test sequences that the service might encounter. Test sequences are typically generated to some finite bounded depth, to avoid an explosion of cases. However, it is important to cover all of the states and transitions of the service, and also to attempt all significant input partitions that might trigger different behaviour. The formal specification captures both of these aspects, such that the test generation tool can provide an ideal test suite that covers all the paths in the service specification. The high-level test suite is expressed in a technology-agnostic way that must then be grounded in any particular implementation technology.

The test generation tool generates a high-level test suite from a software service specification. The tool reads the XML file containing the service specification in XML format. Two further parameters may be supplied, either as attributes of the Service node, or as extra command-line/GUI/web-form parameters. These are: testDepth (the maximum path length to be explored from each state) and multiTest (a boolean flag indicating whether to generate fewer multi-objective tests). It writes machine-readable output in XML format, describing a complete test-suite, with annotations indicating optimisations that were performed.

java uk.ac.sheffield.vtts.GenerateTests <specFile.xml> [<testDepth:int> <multiTest:bool>]

If the input file can be read, the output will be an XML file containing the high-level tests (otherwise an error message will be displayed). The root node TestSuite will contain a Notice node, whose children nodes consist of Advice nodes describing the stages in generating and filtering the resulting tests, and Warning nodes describing any transitions and states that were not covered in the specification, for the chosen depth of exploration. The remaining TestSequence nodes are the paths to test, presented as an ordered set.

Each TestSequence describes a unique test case, consisting of a sequence of TestSteps. Typically, the early TestSteps in a sequence denote set-up actions and the final TestStep is the particular step under observation, to be verified (any step annotated with verify="true" should later be checked using e.g. JUnit assertions). However, if multi-objective tests were selected, some TestSequences may also have intermediate verified TestSteps. This is where shorter tests have been merged into longer tests, where the shorter sequence is a prefix of the longer sequence.

Cloud Service Test Grounding

Test grounding is the final stage in the model-based testing process, whereby technology-neutral XML test sequences are converted into concrete tests that can be executed on a given platform. The conversion process is achieved using a Visitor Pattern algorithm which traverses the memory model of the high-level XML test suite generated earlier. Having a separate test grounding stage is useful, because it decouples the test generation phase, a formal process, from any particular implementation technology for the service. Test grounding is normally something to be accomplished by the service provider, to ground the tests according to the particular service technology used. However, we provide three standard groundings as demonstrations. In the following examples, we assume that the System-Under-Test is either a plain old Java object (POJO), or a Java SOAP client built using JAX-WS, or a REST client build using JAX-RS (Apache Jersey) and generate tests grounded in Java for a JUnit test driver fixture.

The test grounding tool generates a concrete JUnit test driver from a technology-neutral test-suite. The tool reads the XML file containing the high-level test suite. It writes a Java source code output file, defining the JUnit test driver, in one of three demonstration formats. Two further parameters may be supplied, either as attributes of the TestSuite node, or as extra command-line/GUI/web-form parameters. These are: grounding (the particular grounding to use, one of: Java, JAX-WS or JAX-RS) and metaCheck (a boolean flag indicating whether to generate assertions to verify the full state and transition behaviour of the service, assuming the service records such metadata for testing purposes). Different versions of this tool also accept further optional arguments for specifying a REST URI (used only in the JAX-RS grounding), or Java package names (the target package for the JUnit test driver; and source packages for the Java service client and resources; the first package is assumed to be the target).

java uk.ac.sheffield.vtts.GroundTests <testFile.xml> [<grounding:enum> <metaCheck:bool> <endpoint:uri>? <packageName>*]

If the input file can be read, the output will be Java source file containing the executable tests (otherwise an error message will be displayed). The file will define a JUnit test driver class, named following JUnit conventions, and executable in any environment supporting JUnit 4. The test driver's @Before setUp() method creates an instance of the Service-Under-Test, presumed here to be either a plain old Java object, or a Java SOAP client interface built using JAX-WS, or an Apache Jersey REST client built using JAX-RS. The driver and the SUT can be in different Java packages (if none are supplied, the tools assume by default the package structure defined in the software distribution, which has separate folders for client and test software, and subdivisions within these for each kind of grounding). The @Test testN() methods of the driver correspond to the test sequences generated by the high-level test generator. By default, each test consists of set-up steps, followed by a verified step, in which the outputs of methods are verified using JUnit assertions.

If multi-objective testing was selected in the test generation phase, each test may contain multiple verified steps, corresponding to additional JUnit assertions inserted in each sequence. Multi-objective testing merges shorter test sequences into longer sequences. This minimises the number of test sequences, while still testing the same objectives. If a full meta-check of state and transition behaviour was requested, further JUnit assertions are generated, to query the system about the last scenario executed and the last reached state. The implemented service must follow certain design-for-test conditions to be fully testable, with operations to reveal its last action and reached state. The example Java POJO clients supplied with the software distribution illustrate how to develop such a testable service. These examples all use the State Pattern for their implementation.

Finally, it should be noted that all generated JUnit software will depend on the existence of a suitable Java client for the tested service. We have provided full implementations of Java POJO clients for all the example specifications, and skeletons for a few JAX-WS clients (really, the service developer should supply these using JAX-WS tools). We have made assumptions that the JAX-RS client is an Apache Jersey REST server that translates JSON data using Google's Gson parser. Warning: when you first generate JUnit test drivers, these will have unresolved dependencies and you will have to include the relevant libraries on your build-path. Please see the: installation instructions. If you rely on the default package structure, this will appear to create unresolved dependencies within the distributed software bundle - this is not then our responsibility!

To use the Java Swing GUI demonstrator, which also reads and writes files by default to the standard package structure, you only need to launch the main-class in the gui package. You can either launch this using Run within your Eclipse IDE, or you can launch the class within your JDK environment as shown here:

java uk.ac.sheffield.vtts.gui.BrokerAtCloudVTTS

You can also compile a separate executable jar-file whose manifest names: uk.ac.sheffield.vtts.gui.BrokerAtCloudVTTS as the entry point (you will have to include the library files jast-1.1.jar and jsyntaxpane-1.0.jar in the build, if you wish to export this as a standalone tool). The executable jar-file can then be launched by double-clicking on the icon.

Thereafter, the usage should be intuitive, assuming you have read the above principles. The GUI tool invokes the same programs described above, but also displays the input and output files in two large panes. It uses Google's JSyntaxPane software to pretty-print both XML and Java text, using syntax highlighting to make the input and output easier to browse. Warning: we have discovered that the syntax highlighting code can be very s..l..o..w.. for longer files (e.g. for test-suites generated to depth 3, or higher) and will take many seconds to render. So we have provided a check-box to disable syntax highlighting!

To use the CGI programs, which read XML files from supplied public URLs and write output to a web-browser, you will need to configure your own cgi-bin set-up. Instructions are given in the Javadoc documentation for the software distribution. The basic steps are as follows:

• Compile the VTTS software distribution and make the model, ground and web packages' binary class files available in some directory that is readable by scripts in your cgi-bin directory. You will also need JAST 1.1's ast package to marshal the XML.
• Write four short CGI shell-scripts that launch your Java JRE (6/7) runtime and one of the back-end programs: WebValidateMachine, WebVerifyProtocol, WebGenerateTests and WebGroundTests. These are in the web package.
• Create four web pages that each contain a web form that invokes one of your CGI scripts as its action, and uses the HTTP POST method to supply all web form parameters on standard input. Parameter names and their meanings are described in the Javadoc for the web package.

As an example of such a web service, you may: follow the trail on this website, which uses these programs.