Guide to Verification and Testing
Introduction
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.
Verification and Testing of Cloud 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.
Using the Verification and Testing Tools
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
TestStep s. Typically, the early TestStep s 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 TestSequence s
may also have intermediate verified TestStep s. 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!
Using the VTTS Demonstration Java Swing GUI
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!
Using the VTTS Back-End CGI Web Programs
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.
|