Package uk.ac.sheffield.vtts.model

This package contains Broker@Cloud components for modelling service specifications and test suites, and for modelling expressions in the formal expression language.

See: Description

Class Summary

Class	Description
Alphabet	Alphabet represents the complete set of events recognised by a machine.
Analysis	Analysis is a kind of Notice analysing a property of the associated model.
Annotated	Annotated is the ancestor of all annotated elements in the metamodel.
Arithmetic	Arithmetic represents a numerical function with an arithmetic operator root node.
Assignment	Assignment represents a single variable-binding expression.
Atomic	Atomic is a degenerate predicate representing an atomic Boolean value.
Binding	Binding represents a particular set of value-bindings to parameters.
Comparison	Comparison represents an inequality expression, comparing two operands.
Condition	Condition represents a logical guard, or a precondition.
Constant	Constant is a kind of parameter standing for some fixed constant value.
Coverable	Coverable is the abstract ancestor of coverable parts of a specification.
Effect	Effect represents a particular set of value-modifications to parameters.
Element	Element is the root Element of the metamodel.
Entity	Entity is the model entity used to simulate all uninterpreted basic types.
Event	Event represents a unique named event recognised by a finite state machine.
Expression	Expression represents a computable expression, with a name and a type.
Failure	Failure is an exception or error parameter associated with an operation.
Function	Function represents a functional expression with a function root node.
Input	Input is an input parameter associated with an operation.
Language	Language represents a set of sequences of various lengths.
Machine	Machine represents a named finite state Machine.
Manipulation	Manipulation represents an expression manipulating a collection of items.
Membership	Membership represents a cardinality or membership predicate on a collection.
Memory	Memory represents the collection of state variables in a software service.
Named	Named is the ancestor of all named elements in the metamodel.
Notice	Notice is the ancestor of different notice, analysis and warning messages.
Operation	Operation represents an operation in the public interface of a service.
Output	Output is an output parameter associated with an operation.
Parameter	Parameter is a kind of expression denoting a named and typed parameter.
Predicate	Predicate represents a boolean valued function with a predicate root node.
Projection	Projection represents a function creating, or projecting from, a tuple.
Proposition	Proposition represents a logical expression with a Boolean operator root node.
Protocol	Protocol is a model of the abstract behaviour of a software service.
Scenario	Scenario represents one branching path through a single operation.
Scope	Scope represents a scope within which parameters may be declared.
Sequence	Sequence represents a sequence of events to present to a finite state machine.
Service	Service represents a a model or specification of a software service.
Specification	Specification is the abstract ancestor of different kinds of specification.
State	State represents a named state in a finite state machine.
TestSequence	TestSequence represents a test whose steps are to be executed in order.
TestStep	TestStep represents a single executable test step within a test sequence.
TestSuite	TestSuite represents a set of generated high-level test testSequences.
Transition	Transition represents a named transition in a finite state machine.
Variable	Variable is a state parameter representing part of the system's memory.
Warning	Warning is a kind of Notice indicating a fault in the associated model.

Error Summary

Error	Description
SemanticError	SemanticError reports semantic construction errors when building the model.

Package uk.ac.sheffield.vtts.model Description

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/.

Package uk.ac.sheffield.vtts.model

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.

Specification Concepts

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.

Test Suite Concepts

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.

Expression Language Concepts

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.