Cloud Service Verification

This page grants access to a web service for verifying a cloud software service specification. This verification tool was developed for the EU FP7 Broker@Cloud project, to support the continuous quality assurance objective.

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.

Protocol Completeness Checker

This web service checks the completeness of a service's protocol (it checks statically whether single branches exist for each logical input condition of each operation). It returns machine-readable data in XML format. Please supply the public URL of the XML file containing the service specification in XML format. (You may copy an example URL from the specification page).

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, 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, or non-deterministic under certain inputs. These warnings indicate faults in the specification that should be corrected.

A Notice node is then attached to each Operation node, describing the analysed behaviour of that operation. If the operation is sensitive to different inputs, another Notice node is attached, containing an Analysis node for each input partition. Otherwise an Analysis node reports that the operation accepts universal input. Then, for each input partition, an Analysis node is created if one scenario that accepts this input; and a Warning node is issued if no scenarios accept the input (blocking); or if multiple scenarios accept the input (non-determinism) - the multiple scenarios are identified in appended Analysis nodes under the warning. In blocking and non-deterministic cases, the specification is faulty and should be corrected.