Cloud Service Specification

Introduction

This page grants access to a web standard for specifying the functional behaviour of a cloud software service. The standard was developed for the EU FP7 Broker@Cloud project, to support the continuous quality assurance objective.

The XML Schema Definition for software service specifications is given below. Specifications developed to this standard may be validated and verified by tools developed for the project, one of which generates a high-level functional test suite from the specification. To assist users in seeing how a valid service specification may be defined according to the schema, several service specifications are also provided below, as valid exemplars of the schema.

The following is a link to the current version of the XML Schema Definition for service specifications. This XML schema may be used with any XML document validation tool, to determine whether the service specification document conforms to the schema:

• https://staffwww.dcs.shef.ac.uk/people/A.Simons/broker/ServiceSchema.xsd, Service Schema, current version (beta-1).

Note that this is the XML Schema Definition, not an example service specification (instance of the schema). Several valid examples are provided below.

The following are examples of XML service specifications. More will be added in due course. These are actual service specifications that conform to the XML Schema above. These specifications may be used as exemplars with the validation, verification and testing tools provided elsewhere on this site (right-click and select copy link address, then paste into the URL text field).

• https://staffwww.dcs.shef.ac.uk/people/A.Simons/broker/Login.xml, a basic login service with two states {LoggedOut, LoggedIn} modelling the authenticated state of a user. This example illustrates the specification of a simple state machine and has no need for further memory variables. Memory contains constants, representing test inputs.
• https://staffwww.dcs.shef.ac.uk/people/A.Simons/broker/Account.xml, a simple bank account service with two states {Closed, Open} and memory variables storing the account holder and current balance. This example illustrates how to initialise and update memory variables and how to design guarded scenarios with compound conditions. It also illustrates operations with inputs and Boolean outputs, representing success or failure (one possible error-handling strategy, where the service is designed to be fail-safe).
• https://staffwww.dcs.shef.ac.uk/people/A.Simons/broker/ContactList.xml, an updatable table of contacts, with three states, {EmptyTable, NonEmptyTable, RowSelected}, representing the selection-state of a GUI. Memory is a single list of pairs, where each pair is a forename and a surname string. This example is more complex, illustrating how guarded scenarios may branch on the state of memory-variables; and extra row-selection scenarios are provided to ensure that all states can be reached during testing.
• https://staffwww.dcs.shef.ac.uk/people/A.Simons/broker/HolidayBooking.xml, an application for requesting periods of leave, with three states, {ViewDays, BookDays, DeleteDays}, representing the screen-state of a simple SAP OpenUI5 application running on the SAP HANA Cloud Platform. Models realistically complex scenarios, in which single days, short blocks or long blocks of days may be booked, overlapping dates are refused and booking more than five days is refused. Operations correspond to button actions or selection actions. Some operations return multiple values (the start and end date).
• https://staffwww.dcs.shef.ac.uk/people/A.Simons/broker/ShoppingCart.xml, a shopping cart service, with four states {Ready, Shopping, Checkout, Payment} representing the stages in the online shopping cycle. Memory represents both the contents of the cart and the shop's level of stock as variable maps. This example illustrates the pure functional style of map and list manipulations in the expression language: only the assignment operator modifies variable states. It also introduces the user-defined uninterpreted type "Dvd" to model the items for sale. It shows off the test generator's ability to optimise the test-explosion (there are 4 states and 13 distinct events).
• https://staffwww.dcs.shef.ac.uk/people/A.Simons/broker/DocumentStore.xml, a Cloud-based document storage service, that supports versioned storage, with user-specific SLAs for storage limits and encryption standards. Although this specification only has two states {LoggedOut, LoggedIn}, it has memory-variables with complex structured types, representing maps from IDs to lists of document versions, using a user-defined uninterpreted type "Document" to model the items stored. It has complex conditions with up to 81 equivalence-partitions detected by the verification tool; and also illustrates the use of failure-outputs to signal not-found errors when a bad document or version ID is requested (another possible error-handling strategy, where a service is designed to raise exceptions).
• https://staffwww.dcs.shef.ac.uk/people/A.Simons/broker/VatClearance.xml, a simple VAT clearance service, as implemented by Singular Logic on the Orbi platform, that guides a self-employed customer through the stages of submitting their VAT number, submitting a number of VAT invoices, and then determining during the clearance phase whether they have to pay a tax bill, or receive a tax refund from the authorities. This specification has a linear sequence of states {Initial, VatDeclaration, Clearance, Final}, but uses two user-defined uninterpreted types "Vat" and "Invoice" to model sets of VAT identifiers and sets of VAT invoices. The memory models a set of blacklisted VAT numbers, a set of processed VAT invoices and the total tax bill. While most guard conditions are simple membership tests, this example also illustrates the use of an internal counter to select unseen, or previously-seen invoices from a list of test exemplars.

The following is a link to a tutorial guide to Writing service specifications. It introduces the concepts of a service specification, such as high-level states to model the responsive modes of a service, and detailed protocols to model the operation signatures, inputs, outputs, preconditions and effects, and goes on to develop an example similar to the shopping cart, above:

• https://staffwww.dcs.shef.ac.uk/people/A.Simons/broker/ServiceSpecificationGuide.pdf, Service Specification Guide, version 1.0.

Use this guide to help develop your own service specifications. If you make your specifications available via a public URL, you will be able to load their URLs into the validation, verification and test generation tools offered by this website.