Specification - Plastic

$Header: /cvsroot/ist-plastic/Plastic/web/docs/plastic0_3.html,v 1.1 2006/07/10 11:29:17 jwskene Exp $


$Log: plastic0_3.html,v $

Revision 1.1  2006/07/10 11:29:17  jwskene

First addition of project webpages.



Revision 1.1  2006/07/04 14:04:11  francoraimondi

changes for plastic0_3


Revision 1.7  2006/06/28 12:59:39  jwskene
Preliminary merge of conceptual model with technology-independent concepts from SLAng.


Revision 1.6  2006/06/28 02:50:14  francoraimondi
End of comments from D1.1


Revision 1.5  2006/06/27 01:51:52  francoraimondi
More documentation included


Revision 1.4  2006/06/23 16:23:13  francoraimondi
Some corrections from latest version of deliverable


Revision 1.3  2006/06/22 15:48:43  francoraimondi
Initial documentation


Revision 1.2  2006/06/21 16:29:07  francoraimondi
Added CVS fields

This is the EMOF translation of the conceptual model for PLASTIC, based on Deliverable 1.1 (see http://www-c.inria.fr:9098/plastic/deliverable/year-1).

This preamble establishes the basis for interpreting the specification. The specification is written in a combination of three languages: English, a concrete syntax for EMOF, and OCL2.

EMOF and OCL are defined respectively by the following specifications:

- The OMG MOF 2.0 Core Final Adopted Specification

Available: http://www.omg.org/cgi-bin/doc?ptc/2003-10-04

- The OMG UML 2.0 OCL Final Adoped Specification

Available: http://www.omg.org/cgi-bin/doc?ptc/2003-10-14

The relationship between the EMOF concrete syntax and the EMOF abstract syntax is straightforward. It is implemented in the JavaCC grammar contained in the UCL MDA Tools project on sourceforge.net in the file EMOFOCL/uk/ac/ucl/cs/emofocl/parser/emof.jj

The language definition consists of a model of SLAs and the service environment that forms their context. The part of the model that models SLAs defines the abstract syntax of the language. The relationships between the syntactic part of the model and the part of the model modelling services define the semantics of the language.

Disregarding any statement to the contrary made in the MOF or OCL2 specifications, this is a model of real-world objects and relationships, at a particular level of abstraction. The types of services, parties and data described in the model are descriptions of these things as they exist in the real world. The types of specification artifacts such as SLAs, and parts of these artefacts, are descriptions of concrete artefacts in the real world.

This specification offers several things:

1. A model of the commonly understood reference concepts for the Plastic project and architecture.

and 2. A definition of when a scenario can be considered to be an instance of this Plastic model, and therefore a Plastic scenario.

and 3. A definition of how the parties interacting with the Plastic architecture should behave, for example when they are bound by SLAs.

and 4. Informal comments on the use of the model and its meaning, which are not definitive.

A scenario in the real world can be considered to be a Plastic scenario under the following conditions:

1. All objects in the real world relevant to the scenario conform to one of the concrete types defined in this specification, according to the definition of type conformance given below.

For every type of real-world object relevant to scenarios, we offer:

1. A definition of the type in our concrete syntax for EMOF, including a name (in English), properties with names (in English), and a full type definition according to the EMOF specification.

and 2. A comment on the type, in English, that is labelled "Definitive:"

and 3. A comment on each property, in English, that is labelled "Definitive:"

and 4. Possibly one or more type invariants expressed using OCL2, labelled "Wellformedness:". These constraints must always hold true in any situation in which an agreement on a SLAng SLA can be said to exist. The English description accompanying these constraints is not meaningful for the purposes of determining type conformance, but is intended to assist human interpretation of the accompanying OCL constraint.

and 5. Any number of comments on aspects of the type labelled "Informal:". These comments are not definitive of the language, but are intended to aid comprehension of the definitive parts of the specification.

A real-world object under inspection can be interpreted as conforming to a type described in this model if:

a. It is compatible with the definitive description of objects of this type given in this specification.

and b. It has all of the properties of objects of this type, and all those properties are compatible with the definitive descriptions of the properties given in this specification, and the values of those properties conform to the definitions of the types of the respective properties given in this specification, per the definition of compatibility defined here.

and c. It meets all "Wellformedness" constraints on those objects defined in this specification, as per the semantics of OCL2, and the interpretation of all properties as objects conforming to types described in this specification.

How parties should behave:

Parties and their behaviour are construed as objects conforming to types in the model. They should therefore behave according to the descriptions and constraints associated with the model. If parties violate these constraints, for example by refusing to participate in the administration of an SLA, then a scenario may no longer be considered to be a normal Plastic scenario, and the Plastic project will not formally address these cases.

Informal advice:

Non-definitive comments in this specification are labelled as "Informal:".

Contents:

Package - ::conceptualmodel

Definitive: The conceptual model package contains types representing the key concepts of Plastic at their highest level of abstraction.

Class - ::conceptualmodel::Location

Informal: Location is an identifier of a context and it can be related both to physical and logical context. This entity is useful to model mobility in the PLASTIC platform.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::AdaptionSpecs

Informal: This entity models the rules used to adapt a software component to a specific context.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::SoftwareComponent

Informal: A software component can be a COTS, a newly implemented one, or an Assembled component.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ComponentDescription

Informal: Component Description contains functional and non-functional specifications of the software component it corresponds. Among non-functional aspects the PLASTIC platform requires that QoS attributes of the component are explicitly defined.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ContextDescription

Informal: This entity represents the information the PLASTIC platform is able to retrieve from the environment, suitably structured. In general this information is partial since it is too heavy (and useless) to gather the complete information on context. It contains descriptions of the (logical and physical) available resources.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::Actor

Informal: a person (superclass for Service Developer, Service Provider, Service Consumer, Service Integrator, Service Registry, and Component Assembler).

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ComponentAssembler

Extends: ::conceptualmodel::Actor

Informal: this entity identifies the actor responsible of composing Software Components into an Assembled Component.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::AssembledComponent

Extends: ::conceptualmodel::SoftwareComponent

Informal: An assembled component is Software Component.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ProvidedFunctionality

Informal: A provided functionality is a service [TODO]

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ServiceDeveloper

Extends: ::conceptualmodel::Actor

Informal: a Service Developer is an Actor and it identifies the developer of a software service. It may coincide with the Service Provider.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ServiceProvider

Extends: ::conceptualmodel::Actor

Informal: a Service Provider is an Actor providing software services for future usage when these are implemented. It is network addressable. It accepts and executes requests from Service Consumers. The Service Provider may coincide with the Software Developer.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ServiceSpecification

Informal: This entity contains information about a service.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::Context

Informal: This entity represents the logical and physical context in which the service will be executed.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ComposedSoftwareService

Extends: ::conceptualmodel::SoftwareService

Informal: a Composed Software Service is a Software Service. This entity identifies software services when they result from the composition of other software services.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::SoftwareService

Extends: ::conceptualmodel::ProvidedFunctionality

Informal: a Software Service is a Provided Functionality. This entity model a simple Software Service.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ServiceRegistry

Extends: ::conceptualmodel::Actor

Informal: the Service Registry is an Actor modelling a network-based directory, possibily distributed, that contains available services, building upon service discovery technology. It accepts and stores service descriptions from Service Integrator.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ServiceIntegrator

Extends: ::conceptualmodel::Actor

Informal: The Service integrator is an Actor, responsible for the composition of Software Services and Composed Software Services, to obtain more complex services (as required by Service Consumers).

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ServiceConsumer

Extends: ::conceptualmodel::Actor

Informal: the Service Consumer is an Actor interested in Software Services.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ServiceRequest

Informal: a request for a Service (expressed by a Service Consumer).

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::AbstractService

Informal: This entity models Abstract Services according to the SecSE model, see p.89 of D1.1.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ServiceDescription

Informal: the Service Description associated to Software Services.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::AvailableResourcesSpecs

Extends: ::conceptualmodel::Context

Informal: Available resource Specs is (part of) a Context and it contains the description of the resources available at the service consumer side (in other words, it contains specifications about the device the service consumer uses).

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ServiceRequestRequirements

Informal: the Service Request Requirements associated with a Service Request. These cover functional and non functional aspects.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::SLA

Informal: see the package slang.

Properties:

Operations:

Invariants:

Class - ::conceptualmodel::ServiceAdditionalInformation

Informal: (Customer-Side) Service Additional Information contains user supplied information about a service. Such information is collected and stored by the user during and after the execution of the service. It contains usage history, the satisfaction degree of the service, information related to execution environments, the profile of the typical user of the service and the typical access devices used.

Properties:

Operations:

Invariants:

Package - ::types

Informal: Contains types used in both the syntactic or semantic model.

Enumeration - ::types::TimeUnit

Definitive: An enumeration type used to indicate a unit of time associated with some quantity in the model.

  • S

    Definitive: Seconds.

  • mS

    Definitive: Milli-seconds.

  • nS

    Definitive: Nano-seconds.

  • min

    Definitive: Minutes.

  • hr

    Definitive: Hours.

  • day

    Definitive: Days (24 hours).

Class - ::types::Percentage

Definitive: In the syntactic model, indicates a percentage written in an SLA. In the services model, this is the type of features of an object that can be interpreted as a degree of completeness of some totality.

Properties:

Operations:

Invariants:

  • Wellformedness: Percentages are expressed as a value greater than 0. 

    value >= 0

Class - ::types::Duration

Definitive: In the syntactic model a duration is the specification of a length of time. In the services model, a duration is either an actual length of time, or a record of a length of time.

Properties:

  • value : ::types::Real

    Definitive: Interpreted as a number of units of the type specified in the unit property of the duration object, the value is the length of the duration.

  • unit : ::types::TimeUnit

    Definitive: The time unit, by which the value of this duration may be interpreted as an actual duration.

Operations:

  • inMs() : ::types::Real

    Informal: Converts this duration to a number of milliseconds.

    Evaluates to: 

    if unit = TimeUnit.mS then value
        else
          if unit = TimeUnit.nS then value / 1000
          else
            if unit = TimeUnit.S then value * 1000
            else
              if unit = TimeUnit.min then value * 1000 * 60
              else
                if unit =
 TimeUnit.hr then value * 1000 * 60 * 60
                else
                  value * 1000 * 60 * 60 * 24 
                endif
              endif
            endif
          endif
        endif
  • eq(s : ::types::Duration) : ::types::Boolean

    Informal: Defines non-object equality for duration objects.

    Evaluates to: 

    inMs() = s.inMs()

Invariants:

  • Wellformedness: Durations should never be negative. 

    not (value < 0)

Class - ::types::Date

Definitive: In the syntactic model a date is the specification of an instant in time. In the services model, a duration is either an actual instant time, or a record of an instant of time.

Properties:

Operations:

  • inMs() : ::types::Real

    Informal: Converts this date to the number of milliseconds that the date is after 00:00 Jan 1, 2000, UTC+0.

    Evaluates to: 

    sinceJan12000.inMs()
  • eq(d : ::types::Date) : ::types::Boolean

    Informal: Defines non-object equality for date objects.

    Evaluates to: 

    sinceJan12000.eq(d.sinceJan12000)

Invariants:

Primitive type - ::types::Real

Definitive: In the syntactic model, indicates real numbers written into SLAs. In the service model, this is the type for attributes of an object that can be interpreted as having a value within a continous range.

Equivalent to the OCL real type.

Primitive type - ::types::Boolean

Definitive: In the syntactic model, indicates a value of true or false written into SLAs. In the service model, this is the type for attributes of an object that can be interpreted as being either true or false.

Equivalent to the OCL boolean type.

Primitive type - ::types::Integer

Definitive: In the syntactic model, indicates an whole number written into an SLA. In the service model, this is the type for attributes of an object that can be interpreted as being a natural quantity.

Equivalent to the OCL integer type.

Primitive type - ::types::String

Definitive: In the syntactic model, indicates some text included in an SLA. In the service model, indicates some information present in the domain.

Equivalent to the OCL string type.

Package - ::slang

Informal: The slang package contains type specifications for SLAs expressible in the SLAng language and their component expressions. Subpackages contain types specific to particular kinds of SLA, for example electronic service SLAs.

Abstract class - ::slang::SLA

Extends: ::conceptualmodel::SLA

Definitive: SLAng is a language for expressing SLAs. Concrete SLAs otherwise conforming to this type and its related SLAng syntactic types are instances of this class if and only if the parties described in the concrete SLA also agree that the SLA is in force.

Properties:

  • terms : ::slang::Terms

    Opposite: ::slang::Terms.sLA : ::slang::SLA

    Definitive: All SLAs define a set of terms.

    Informal: Terms identify things in the real world that are constrained by the SLA, including, most importantly, services.

  • conditions : ::slang::Conditions

    Opposite: ::slang::Conditions.sLA : ::slang::SLA

    Definitive: All SLAs define a set of conditions.

    Informal: Conditions set the parameters for constraints imposed on those objects identified in the terms by the SLA, the violation of which will require a penalty to be levied against some party.

  • schedule : ::slang::Schedule[0, *] unique

    Opposite: ::slang::Schedule.sLA : ::slang::SLA

    Definitive: SLAs may contain the specification of schedules.

    Informal: Conditions may be associated with schedules defined in the SLA. Schedules define periods of time in which the constraints implied by a condition apply.

  • limitationPeriod : ::types::Duration

    Definitive: The limitation period defines the maximum age of evidence that can be included in a reconciled account.

    Informal: No evidence older than this duration is considered relevant when calculating violations.

    Occasionally, non-obvious violations of SLAs can go unnoticed and unrectified for long periods, potentially implying serious penalties for a party who was otherwise acting in good faith, and who would have rectified the problem had they been aware of it. This poses a risk for any party wishing to enter an SLA. By specifying a limitiation period, this risk is limited, although at the expense of requiring the parties to be extra vigilant in spotting non-obvious failures.

    If a limitation period is not required in practice, this field can be set to a duration longer than the duration of the agreement.

Operations:

Invariants:

Abstract class - ::slang::AdministeredSLA

Extends: ::slang::SLA

Definitive: Some types of SLA are administered, meaning that the client and provider consult on the evidence upon which the determination of violations will be based. SLAs that are mutually monitorable, but not arbitratable by a third party may need to be administered in order to maintain trust relationships between the parties.

Properties:

  • administrationDate : ::slang::AdministrationDate[1, *] unique

    Opposite: ::slang::AdministrationDate.sLA : ::slang::AdministeredSLA

    Definitive: SLAs define a number of administration dates.

    Informal: SLAs are occasionally administered, an activity which consists of reconciling the parties' views on what occurred that is relevant to the SLA during the preceeding administrative period, and then calculating whether the SLA has been violated based on the reconciled account and these semantics.

    Administration dates define the end of an administrative period, and a subsequent deadline by which the parties should have finished administering the SLA.

  • reconciliation : ::types::String

    Definitive: The first stage in the adminstration of an SLA is for the parties to agree on an account of what occurred that is relevant to the SLA. This process is called reconciliation. The SLA includes a field that allows the parties to specify a procedure for reconciliation before it must occur, reducing the likelihood of disputes arising. Parties agreeing to an SLA agree to follow the reconciliation procedure specified in the SLA.

    Informal: Various informal comments in this specification include further advice on the content of this field.

  • administration : ::services::Administration[0, *] unique

    Opposite: ::services::Administration.sLA : ::slang::AdministeredSLA

    Definitive: SLAs are associated with a number of administrations, which are the activity of producing a reconciled account of the events pertinent to the SLA, and using that account and these semantics to calculate violations.

  • typeIErrorRate : ::types::Percentage

    Definitive: The likelihood that a report gathered honestly according to accuracy constraints defined for all uncertain parameters will contain an unacceptable number of errors.

    Informal: This parameter effectively sets a limit on the number of errors that can included in an report, either through dishonesty or by accident. See the invariant below for a fuller discussion of the effect of this parameter.

    A very small value should be chosen for this property of the SLA. A significant degree of cheating in an account will rapidly make the account highly unlikely. However, the probability of seeing at least one reasonably unlikely account in a set of accounts associated with an SLA rises with the size of the set. This likelihood should therefore be kept low to avoid unnecessary disagreements in the event of occasional unlikely accounts being submitted in good faith.

    In the event that the invariant associated with this parameter is violated, the SLA is invalidated and the parties will have to take whatever action they deem necessary.

  • confidence : ::types::Percentage

    Definitive: Confidence that any measured value falls within its expected error margins.

Operations:

  • fact(n : ::types::Integer) : ::types::Integer

    Informal: Calculates the factorial of a positive integer, or -1 otherwise.

    Evaluates to: 

    if n = 0 
then 1
else 
  if n < 0
  then -1
  else n * fact(n - 1)
  endif
endif
  • pick(n : ::types::Integer,
    r : ::types::Integer) : ::types::Integer

    Informal: Calculates the number of ways to chose r objects from n possibilities in a particular order

    Evaluates to: 

    if r > n then
  r * choose(n, r - 1)
else n
endif
  • choose(n : ::types::Integer,
    r : ::types::Integer) : ::types::Integer

    Informal: Calculates the number of ways to choose r objects from n possibilities in no particular order

    Evaluates to: 

    pick(n, r) div fact(r)
  • raise(value : ::types::Real,
    power : ::types::Integer) : ::types::Real

    Informal: Raise a value to an integer power

    Evaluates to: 

    if power = 0 then 1
else
  value * raise(value, power - 1)
endif
  • errorCountProbability(n : ::types::Integer,
    r : ::types::Integer) : ::types::Real

    Informal: Calculate the probability of seeing r errors in n measurements.

    Evaluates to: 

    choose(n, r) * raise(1 - confidence.value, r) *
  raise(confidence.value, n - r)
  • findD(sum : ::types::Real,
    n : ::types::Integer,
    d : ::types::Integer

    Evaluates to: 

    let p = errorCountProbability(n, d) in
if sum > typeIErrorRate.value
then -1
else
  if sum + p > typeIErrorRate.value
  then d
  else findD(sum + p, n, d - 1)
  endif
endif
  • getMaximumAcceptableErrors(measurementCount : ::types::Integer) : ::types::Integer

    Informal: Calculates the maximum number of acceptable errors in an account of the specified size, assuming the confidence in the measurements is as specified in the SLA, and given the target typeIErrorRate.

    Evaluates to: 

    findD(0, measurementCount, measurementCount)

-- getMaximum(
--  Sequence(::types::Integer) { 1..measurementCount }->select(
--    r : Integer |
--    
--    Sequence(::types::Integer) {
--      r..measurementCount }->collect(
--      rprime : Integer |
--      
--      errorCountProbability(measurementCount, rprime)
--    )->sum() < typeOneErrorCount()
-- ))

Invariants:

  • Wellformedness: All accounts associated with reconciliations of this SLA should have a likelihood greater than the specified minimum account likelihood. This constraint cannot be monitored. However, it can be approximately monitored by comparing an account to a trusted account of the same service over the same interval, with known error characteristics. 

    administration.reconciliation.account->forAll(
  a : ::services::Account |


  (a.getMeasurementCount(self) - 
    a.getAccurateMeasurementCount(self)) <
    getMaximumAcceptableErrors(a.getMeasurementCount(self))
)

Class - ::slang::AdministrationDate

Definitive: An administration date defines the end of an administrative period for an SLA, and a subsequent deadline by which the SLA must have been administered for that period.

Properties:

Operations:

Invariants:

  • Wellformedness: If an administration is associated with this date then it should be associated with the SLA of which this date is a part. 

    not administration.oclIsUndefined()
implies
administration.sLA = sLA
  • Wellformedness: An administration associated with this date should be completed after the end of the period and before the deadline. 

    not administration.oclIsUndefined()
implies
administration.date.inMs() >= endOfPeriod.inMs()
and
administration.date.inMs() < endOfPeriod.inMs() +
  administrativeDeadline.inMs()

Class - ::slang::Terms

Definitive: Every SLA contains a set of terms, which are definitions of the things in the real world that the SLA constrains, but not specifically what the constraints are - these are described in the conditions section of the SLA. Different kinds of SLA refer to different types of things, but every SLA expressible in SLAng must define at least who the provider of the service is, and who the client is.

Properties:

Operations:

Invariants:

Abstract class - ::slang::Conditions

Definitive: All SLAs feature a set of conditions, which specify the parameters for the constraints imposed on associated services by the SLA.

Properties:

Operations:

Invariants:

Abstract class - ::slang::Definition

Definitive: The terms of an SLA contain a number of definitions of various types of things in the real world.

Properties:

  • identifier : ::types::String[0, 1]

    Definitive: Definitions may be given an identifying string to allow convenient reference to made to them outside the context of the SLA. The form and content of the identifying string are unconstrained. The identifying string primarily identifies the definition, not the object described by the definition. Therefore the definition should be construed based on the contents of the description field only.

  • description : ::types::String

    Definitive: A description of the thing in the real world being defined. Things associated with this definition must be compatible with the description given for them. The parties to any SLA should ensure before entering the SLA that all terms are defined unambiguously and to their satisfaction. At the agreement of the parties, descriptions included in the SLA may be unambiguous references to descriptions of things maintained externally to the SLA. For example, if the SLA is embedded in a document describing a larger service provision agreement, the SLA may refer to a definition of the service in question contained in the larger document, external to the SLA.

Operations:

Invariants:

Abstract class - ::slang::PartyDefinition

Extends: ::slang::Definition

Definitive: A definition of some person or organisation with a role to play in the service provision scenario.

Properties:

Operations:

Invariants:

Class - ::slang::ClientDefinition

Extends: ::slang::PartyDefinition

Definitive: A client definition is a type of party definition identifying the party that will act as the client to the service constrained by the SLA.

Properties:

Operations:

Invariants:

Class - ::slang::ProviderDefinition

Extends: ::slang::PartyDefinition

Definitive: A provider definition is a type of party definition identifying the party that will act as the provider of the service constrained by the SLA.

Properties:

Operations:

Invariants:

Abstract class - ::slang::ServiceDefinition

Extends: ::slang::Definition

Definitive: A service definition identifies the service being constrained by an SLA.

Properties:

Operations:

Invariants:

Class - ::slang::PenaltyDefinition

Extends: ::slang::Definition

Definitive: A penalty definition is a pre-agreed penalty that some party will have to pay if a violation of a particular type occurs

Properties:

Operations:

Invariants:

Class - ::slang::StateDefinition

Extends: ::slang::Definition

Definitive: A definition of a state of the service or another aspect of the real world. The state of the real world may effect the application of condition clauses.

Informal: In order to preserve the property of monitorability for ES SLAs, authors of the SLA should only refer to states the occupancy of which can be assumed to hold, or can be unambiguously determined from the history of service usages presented in any account of the behaviour of the service.

Properties:

Operations:

Invariants:

Class - ::slang::Schedule

Definitive: Schedules are part of the specification of when conditions in an SLA apply. The conditions specified in an SLA need not all apply at the same time. Moreover, the specification of when the conditions apply may need to be complex. Therefore all condition clauses must be associated with one or more schedules.

Informal: The effect of schedules on the determination of violations is defined by the OCL definitions contributing to the definition of violation invariants.

Each schedule expresses a number of cycles of a specified period. Within these periods, associated condition clauses first apply for a particular duration, then do not apply for the remainder of the duration. These cycles begin at a specified start date and then cease at a specified end date, which need not be a whole number of cycles later. Any clause may be associated with several schedules, and the clause applies whenever any of its schedules apply. By combining schedules in this way, complicated patterns of application can be associated with clauses.

Using schedules, it is possible to specify that several conditions clauses of the same kind apply simultaneously. Depending on the definition of violation behaviour for the clause this may result in several penalties being applied, or only the penalty from the clause that in some sense applies the most restrictive constraint.

Properties:

  • name : ::types::String

    Definitive: Schedules have names that assist in referring to them from an external context, and may provide a reminder as to the intent of the schedule.

    Informal: For example 'Every wednesday'

  • startDate : ::types::Date

    Definitive: Schedules have a start date.

    Informal: Any clauses associated with the schedule will apply for the duration immediately following this date, or until the end date, whichever is sooner. The schedule will then apply again for the duration at the beginning of any subsequent cycle, or until the end date, whichever is sooner.

  • duration : ::types::Duration

    Definitive: Schedules specify a duration.

    Informal: The duration of the schedule. Any clauses associated with the schedule will apply for this amount of time at the beginning of each cycle, or until the end date, whichever is sooner.

  • period : ::types::Duration

    Definitive: Schedules specify a period.

    Informal: The period of cycles in this schedule. Any clauses associated with the schedule will apply for the duration at the beginning of each cycle, or until the end date, whichever is sooner, and then not again until this amount of time has elapsed since the beginning of the last cycle, unless associated with a different schedule that applies.

  • endDate : ::types::Date

    Definitive: Schedules have an end date.

    Informal: The end date. No condition clause associated with this schedule will apply after this date, unless it is associated with a different schedule that applies.

  • scheduledClause : ::slang::ScheduledClause[1, *]

    Opposite: ::slang::ScheduledClause.schedule : ::slang::Schedule[1, *] unique

    Definitive: Schedules are associated with a number of condition clauses in an SLA.

  • sLA : ::slang::SLA

    Opposite: ::slang::SLA.schedule : ::slang::Schedule[0, *] unique

    Definitive: Schedules are part of an SLA.

Operations:

  • eq(s : ::slang::Schedule) : ::types::Boolean

    Informal: Defines non-object equality for schedules. Schedules must be alike in all respects to be considered equal.

    Evaluates to: 

    duration.eq(s.duration) and
period.eq(s.period) and
startDate.eq(s.startDate) and
endDate.eq(s.endDate)
  • applies(t : ::types::Real) : ::types::Boolean

    Informal: Evaluates to true if the schedule applies at time t, false otherwise. t is expressed in milliseconds from 00:00 1 Jan 2000 UTC+0.

    Evaluates to: 

    t > startDate.inMs()
and
t < endDate.inMs()
and 
((t - startDate.inMs()).round().mod(period.inMs().round()) < 
  duration.inMs())
  • cycleNumber(t : ::types::Real) : ::types::Real

    Informal: Evaluates to the number of the cycle that would apply at time t, if t is after the start date and before the end date, and the cycle number is the count of cycles that have applied, starting with 0. t is expressed in milliseconds from 00:00 1 Jan 2000 UTC+0.

    Evaluates to: 

    ((t - startDate.inMs()) / period.inMs()).floor()
  • validateDate(t : ::types::Real) : ::types::Real

    Informal: Filters dates expressed in milliseconds from 00:00 1 Jan 2000 UTC+0. Dates outside of the start and end dates of the schedule are converted to -1, other dates remain as they are.

    Evaluates to: 

    if t < startDate.inMs() or t > endDate.inMs() then -1
else t
endif
  • nextCycleStartDate(t : ::types::Real) : ::types::Real

    Informal: Evaluates to the start date of the next cycle of this schedule that would begin after t, if t is less than the end date of this schedule. t and the result are expressed in milliseconds from 00:00 1 Jan 2000 UTC+0.

    Evaluates to: 

    validateDate(


  if(t < startDate.inMs()) then startDate.inMs()
  else
    startDate.inMs() +
      ((cycleNumber(t) + 1) * period.inMs())
  endif    
)
  • nextDurationEndDate(t : ::types::Real) : ::types::Real

    Informal: Evaluates to the date when the next duration would end after t, if t is less than the end date of this schedule. This amounts to evaluating when the next interval of non-application of the schedule begins, assuming the duration is less than the period. t and the result are expressed in milliseconds from 00:00 1 Jan 2000 UTC+0.

    Evaluates to: 

    validateDate(
  
  if t < startDate.inMs() then startDate.inMs() + duration.inMs()
  else
    if applies(t)
    then 
      startDate.inMs() + (cycleNumber(t) * period.inMs()) +
        duration.inMs()
    else
      nextCycleStartDate(t) + duration.inMs()
    endif
  endif
)
  • nextStartDate(t : ::types::Real) : ::types::Real

    Informal: Returns the next date that this schedule will start to apply after t, or -1 if it will never start again.

    Evaluates to: 

    if duration = period
then
  if t < startDate.inMs()
  then
    startDate.inMs()
  else
    -1
  endif
else
  nextCycleStartDate(t)
endif
  • nextEndDate(t : ::types::Real) : ::types::Real

    Informal: Returns the next date that this schedule will cease to apply after t, or -1 if it will never cease again.

    Evaluates to: 

    if duration = period
then
  if t < endDate.inMs()
  then
    endDate.inMs()
  else
    -1
  endif
else
  nextDurationEndDate(t)
endif

Invariants:

Abstract class - ::slang::ConditionClause

Definitive: All SLAs will define a number of condition clauses, which specify the parameters for the constraints implied by the SLA on the objects in the real world to which it applies.

Properties:

Operations:

Invariants:

Abstract class - ::slang::ScheduledClause

Extends: ::slang::ConditionClause

Definitive: Some types of condition clause are associated with some schedules, with the interpretation that the constraints implied by the clause only apply when any of its associated schedules apply.

Properties:

Operations:

  • applies(t : ::types::Real) : ::types::Boolean

    Informal: Evaluates to true if this clause applies at time t. t is expressed in milliseconds from 00:00 1 Jan 2000 UTC+0

    Evaluates to: 

    schedule->exists(s : Schedule | s.applies(t))
  • nextStartDate(t : ::types::Real) : ::types::Real

    Informal: Returns the date (from 00:00 1 Jan 2000 UTC+0 in mS) that this clause will next start to apply after time t.

    Evaluates to: 

    schedule->iterate(s : Schedule ; 
  next : Schedule = schedule->any(true) |

  if next.nextStartDate(t) = -1
  then s
  else          
      if s.nextStartDate(t) = -1 then next
      else
        if s.nextStartDate(t) < next.nextStartDate(t) then s
        else next
        endif
      endif
  endif
).nextStartDate(t)
  • endDate(t : ::types::Real) : ::types::Real

    Informal: Returns the next time that this clause will cease to apply after t.

    Evaluates to: 

    schedule->iterate(s : Schedule ; 
  next : Schedule = schedule->any(true) |

  if next.nextEndDate(t) = -1
  then s
  else
      if s.nextEndDate(t) = -1 then next
      else
        if s.nextEndDate(t) > next.nextEndDate(t) then s
        else next
        endif
      endif
  endif
).nextEndDate(t)
  • startDatesAfter(t : ::types::Real) : ::types::Real[0, *] unique ordered

    Informal: Evaluates to a list of all of the dates that this clause starts to apply after t.

    Evaluates to: 

    if nextStartDate(t) < 0
then
  OrderedSet(::types::Real) {}
else
  OrderedSet(::types::Real)
  { nextStartDate(t) }->union(
    startDatesAfter(nextStartDate(t))
  )
endif
  • startDates() : ::types::Real[0, *] unique ordered

    Informal: Evaluates to a list of all of the dates that this clause starts to apply.

    Evaluates to: 

    startDatesAfter(-1)

Invariants:

Package - ::services

Informal: This package contains types definitions for all of the types of things that SLAng SLAs describe and constrain.

Class - ::services::Party

Definitive: Parties are people, groups or organisations who can perform some role in a service provision scenario, for example being either the client or provider of a service.

Properties:

Operations:

Invariants:

Abstract class - ::services::Asset

Definitive: Assets are objects in the real world that are identifiably the property and hence responsibility of some party.

Properties:

Operations:

Invariants:

Abstract class - ::services::Service

Extends: ::services::Asset

Definitive: Parties may own services, which are a type of asset.

Properties:

Operations:

Invariants:

Class - ::services::ServiceContext

Definitive: Services exist in a wider context, encompassing all aspects of the world relevant to the behaviour of the service.

Properties:

Operations:

  • getCurrentStatesAt(date : ::types::Real) : ::services::State[0, *] unique

    Informal: Determines the current set of states at a particular date. Note, relies on transitions being ordered by date.

    Evaluates to: 

    transitions->iterate(t : StateTransition;
  current : Set(State) = initialStates |


  if t.event.date.inMs() < date then t.postStates
  else current
  endif
)

Invariants:

  • Wellformedness: Initial states are a subset of all states of the context. 

    initialStates->forall(s : State | states->includes(s))
  • Wellformedness: If the state of the context changes then it passes through a sequence of sets of current states, ordered by date, starting with the inital states of the context then related by consecutive state transitions. 

    transitions->notEmpty()
implies
transitions->at(0).priorStates = initialStates
and
Sequence(::types::Integer)
  { 1..transitions->size() }->forAll(i : ::types::Integer |


  transitions->at(i - 1).postStates =
    transitions->at(i).priorStates
  and
  transitions->at(i - 1).event.date.inMs() <=
    transitions->at(i).event.date.inMs()
)

Abstract class - ::services::Event

Definitive: An event is the completion of some activity at a specific instant of time.

Properties:

Operations:

Invariants:

Class - ::services::State

Definitive: A possible condition of the service context.

Properties:

Operations:

Invariants:

  • Wellformedness: All state transitions are within the same context as the state. 

    outgoingTransitions->forall(t : StateTransition |


  t.context = context
)

Class - ::services::StateTransition

Definitive: The occurrance of events may trigger a change of state in the service context.

Properties:

Operations:

Invariants:

  • Wellformedness: All events, prior and post states are part of the same context in which the transition occured. 

    context.events->includes(event)
and
priorStates->forall(s : State | s.context = context)
and
postStates->forall(s : State | s.context = context)
  • Wellformedness: All prior states are exited by this transition, and all post states are entered (prior and post state sets may intersect though). 

    priorStates->forall(s : State |


  s.outgoingTransitions->includes(self)
)
and
postStates->forall(s : State |


  s.incomingTransitions->includes(self)
)

Class - ::services::Violation

Definitive: Violations are determined to have occurred when the behaviour of a system or a party associated with an SLA is inconsistent with the conditions established in a SLAng SLA. Violations are always the fault of a specific party, and may result in penalties being levied against that party, depending on what has been agreed in the SLA.

Properties:

Operations:

  • eq(v : ::services::Violation) : ::types::Boolean

    Informal: Defines a non-object equality for violations. Violations are equal if they are supported by the same evidence, and indicate the same violator and violated clause.

    Evaluates to: 

    violator = violator
and
evidence = evidence
and
violatedClause = violatedClause

Invariants:

  • Wellformedness: Violations should be unique according to the non-object equality defined by the eq() function for the class. Informal: This implies that violations are only ever levelled against a party once for any particular set of evidence. Therefore the same violation cannot be associated with multiple administrations, and in practice violations are associated with the earliest administration in which they could be detected. 

    calculation.administration.sLA.administration.
  calculation.violation->forAll(
  v : Violation |
  
  v.eq(self)
  implies
  v = self
)

Abstract class - ::services::Evidence

Definitive: Evidence is any kind of information presented by a party for the purpose of determining whether an SLA has been violated.

Properties:

Operations:

  • getMeasurementCount(sLA : ::slang::SLA) : ::types::Integer

    Informal: A single piece of evidence may contain any number of measurements subject to accuracy constraints in the specified sLA. This operation determines how many.

    Evaluates to: 

    0
  • getAccurateMeasurementCount(sLA : ::slang::SLA) : ::types::Integer

    Informal: A single piece of evidence may contain any number of measurements subject to accuracy constraints in the specified sLA. This reports how many measurements are accurate compared to the real behaviour of the service, according to the accuracy constraints specified in the parameter.

    In practice, this operation could never be evaluated, because the true performance of the service cannot be known, but only approximated by evidence gathered by measurement. However, constraints over the distribution of the results returned by this operation are used to constrain the precision of the measurements that the parties must return, and conformance to those constraints can be estimated by comparing the behaviour of any party to a set of measurements with trusted error characteristics.

    Evaluates to: 

    0

Invariants:

Abstract class - ::services::Report

Definitive: Reports are communications between parties that are not a technical part of the delivery or use of a service.

Informal: It is sometimes necessary for parties to communicate in a manner that does not use the service being constrained by the SLA. For example, if the service is broken, the client may not communicate with the server, but will wish to notify the server that an error condition needs to be rectified. Also, In the electronic service scenarios covered by our ES SLAs, there is also no way for the service provider to initiate communications with the client using the service, he must wait until the client submits a request. However, the service provider needs to communicate some information to the client when an error condition has been rectified. Reports are an abstraction of these communications, and may in fact be emails, telephone calls, carrier pigeon, or any other appropriate form of communication between the parties.

Properties:

Operations:

Invariants:

Class - ::services::ReportRecord

Extends: ::services::Evidence

Definitive: A report record is evidence presented by a party to the effect that a particular report was sent at a particular time.

Properties:

Operations:

Invariants:

Class - ::services::Administration

Extends: ::services::Event

Definitive: An administration is an event indicating the culmination of the activity of the parties performing a reconciliation of their accounts of the service provision scenario for the administration period prior to the administration, and then calculating violations based on the reconciled account.

Properties:

Operations:

Invariants:

  • Wellformedness: Reconciliation occurs before violation calculation. 

    reconciliation.date.inMs() < calculation.date.inMs()
  • Wellformedness: Reconciliation and violation calculation should occur before this administration is complete, but after the end of the administrative period. Administration should be complete before the administrative deadline. 

    reconciliation.date.inMs() < date.inMs()
and
calculation.date.inMs() <= date.inMs()
and
reconciliation.date.inMs() >
  administrationDate.endOfPeriod.inMs()
and
calculation.date.inMs() >
  administrationDate.endOfPeriod.inMs()
and
date.inMs() <= administrationDate.endOfPeriod.inMs() +
  administrationDate.administrativeDeadline.inMs()
  • Wellformedness: Administrations are events occurring within the context of the service to which the sLA is applied. 

    sLA.terms.serviceDefinition.service.context.events->includes(
  self)
  • Wellformedness: Administration is mutually monitorable by the client and provider of the SLA. 

    witnesses->includes(sLA.terms.clientDefinition.party)
and
witnesses->includes(sLA.terms.providerDefinition.party)

Class - ::services::Reconciliation

Extends: ::services::Event

Definitive: Reconciliation is the first stage in an administration of an SLA. The parties to the SLA submit accounts of the service behaviour as they recorded it over the period being administered. These accounts are then reconciled into a single account on which violation calculations are to be based, according to the reconciliation procedures specified in the SLA and agreed on by the parties.

Properties:

Operations:

Invariants:

  • Wellformedness: Reconciliations are events occurring within the context of the service to which the sLA is applied. 

    administration.sLA.terms.serviceDefinition.service.context.
  events->includes(
  self)
  • Wellformedness: Reconciliation is mutually monitorable by the client and provider of the SLA. 

    witnesses->includes(
  administration.sLA.terms.clientDefinition.party)
and
witnesses->includes(
  administration.sLA.terms.providerDefinition.party)

Class - ::services::ViolationCalculation

Extends: ::services::Event

Definitive: Violation calculation is the second stage in the administration of an SLA. Violations should be calculated in a manner equivalent to the evaluation of the violation calculation operations specified in this specification, over the account resulting from the prior reconciliation in the administration of which this calculation forms a part, with the evidence interpreted as objects conforming to the evidence types specified in this specification.

Properties:

Operations:

Invariants:

  • Invariant: All evidence used in violations comes from the agreed account produced by the administration of which this calculation forms a part. 

    administration.reconciliation.agreed.evidence->includesAll(
  violation.evidence
)
  • Wellformedness: Violation calculation is mutually monitorable by the client and provider of the SLA. 

    witnesses->includes(
  administration.sLA.terms.clientDefinition.party)
and
witnesses->includes(
  administration.sLA.terms.providerDefinition.party)
  • Wellformedness: Violation calculations are events occurring within the context of the service to which the sLA is applied. 

    administration.sLA.terms.serviceDefinition.service.context.
  events->includes(
  self)

Class - ::services::Account

Definitive: An account is a collection of evidence. It is either submitted by a party prior to reconciliation, or is the result of several reconciled accounts following reconciliation.

Properties:

Operations:

  • getMeasurementCount(sLA : ::slang::SLA) : ::types::Integer

    Informal: Returns the total number of measurements in this account, given the accuracy constraints in the SLA.

    Evaluates to: 

    evidence->collect(getMeasurementCount(sLA))->sum()
  • getAccurateMeasurementCount(sLA : ::slang::SLA) : ::types::Integer

    Informal: Returns the total number of accurate measurements in this account, given the accuracy constraints in the SLA.

    Note that this operation could never be evaluated in practice because true values for system performance cannot be known with certainty. However, conformance to constraints based on the result of this operation can be estimated statistically.

    Evaluates to: 

    evidence->collect(getAccurateMeasurementCount(sLA))->sum()

Invariants:

  • Wellformedness: Evidence is ordered by date. 

    Sequence(::types::Integer) { 1..evidence->size() }->forAll(
  i : ::types::Integer, j : ::types::Integer |
  
  i > j
  implies
  evidence->at(i).date.inMs() >= evidence->at(j).date.inMs()
)