This package contains Broker@Cloud components for modelling service specifications and test suites, and for modelling expressions in the formal expression language. It is part of the Broker@Cloud Verification and Testing Tool Suite, v1.0, © Anthony J H Simons and Raluca Lefticaru, 2015. Main web site: http://staffwww.dcs.shef.ac.uk/people/A.Simons/broker/.
This package contains Broker@Cloud components for modelling service
specifications and test suites. These classes constitute the metamodel for
the tool suite. This package should always be used by the JAST marshalling
and unmarshalling tools ASTReader
and ASTWriter
,
which must be told where to find the Java mappings for parsed XML data.
The metamodel classes are designed with suitable API conventions for
marshalling and umarshalling with JAST, which has the advantage that it
requires no special annotations on classes to be marshalled as XML.
The entire metamodel is designed according to object-oriented principles of
classification, with inheritance of common attributes and methods. The
metamodel hierarchy is rooted in the type Element
, which has
Named
as one of its more important subtypes, since many of the
model components are named; and otherwise leads to an elaboration of concepts
including expressions consisting of functions, predicates, parameters and
assignments; finite state machines, with their alphabets, states and
transitions; or operations with their inputs, outputs and internal branches;
or test suites with their test sequences and individual test steps.
The type Service
is the metamodel type standing for a complete
service specification. It encloses the two types Protocol
and
Machine
, respectively denoting the operation protocol and the
finite-state machine of the service. The former describes each operation of
the service's API in some detail, in terms of its expected inputs, outputs,
preconditions and effects. The latter describes the high-level responsive
modes of the service API in which particular operations are available, or
disabled.
The Protocol
node contains a Memory
node, describing
Constant
and Variable
parameters used later in the
specification. The constants refer to ground values, or specific test values.
The variables refer to the fine-grained memory states of the service. The
Protocol
node also contains a set of Operation
nodes, each describing one service operation with its Input
,
Output
and Failure
parameters. Every
Operation
consists of one or more Scenario
nodes,
denoting the different branching paths through the operation. Each
Scenario
is usually triggered by a Condition
and may
optionally have an Effect
, updating memory variables.
The Machine
node contains several State
nodes
denoting the high-level responsive modes, or states of the service, and each
of these contains Transition
nodes that exit from that source
state, and enter another named target state. Each Transition
has a label that corresponds exactly to the name of one Scenario
from an Operation
. This links the two parts of a specification.
Where no exit-transition exists from a given state, this is understood to mean
that the given request is ignored in that state.
The type TestSuite
is the metamodel type standing for a complete
generated test suite. It contains an ordered set of TestSequence
nodes, representing the tests to be executed on some service, in that order,
so that all test failures are caught at the earliest point. The testing
method assumes that the service starts from a clean state (after creation, or
after a reset). Each TestSequence
consists of a sequence of
TestStep
steps, each naming an Operation
to invoke,
the Input
parameters to supply and the Output
(or
Failure
) parameters to expect. The initial test steps in a test
sequence are to set up a unique memory-state, and the final test step is to be
verified, in the same way that a JUnit test author would write assertions to
verify outcomes.
The TestSuite
node is designed to receive a visitor (in the
sense of the Visitor Design Pattern) of the interface type
Grounding
. Specific implementations of this interface will
generate platform-specific code from the technology-neutral test suite.
Several example groundings are given in another package, as illustrations of
how to ground to Java, SOAP and REST, but it is expected that platform and
service providers will define their own groundings to match the particular
platform technology used.
An important part of the metamodel is the Expression Language, a
mathematical language of values, sets, lists, maps, functions and predicates,
that is used by Condition
and Effect
nodes to
express calculation and computation. The language has a similar expressive
power to the Z Formal Notation, but without quantifiers. The type
Expression
is the ancestor of Function
, denoting a
functional expression with operands, and Parameter
, denoting a
constant, variable, input or output.
Important kinds of Function
include: Arithmetic
,
modelling all kinds of arithmetic, Projection
, modelling pairs
and projections, Manipulation
, modelling all set-theoretic
manipulations on sets, lists and maps, Predicate
, the abstract
ancestor of Comparison
, Membership
and
Proposition
predicates, and Assignment
, the only
expression which causes a side-effect. All other constructions in the
language have pure-functional semantics, in that they do not alter variable
states.
The varieties of Parameter
include: Constant
,
denoting constants, Variable
, denoting global variables,
Input
, Output
and Failure
, denoting
respectively the inputs, outputs and exceptions passed as values to and
from operations. All parameters must be declared before usage in a model
specification; and the model construction API seeks to resolve all uses of
parameters, as the specification is built. A SemanticError
indicates that something is amiss in a model that might otherwise be parsed
as syntactically correct.