|
Printer friendly version
Disclaimer: None of the information provided on this page should be
construed as legal advice. SLAng is under development and should not yet be
used for real SLAs.
Specification - SLAng
Definitive: This is the SLAng Language specification $Revision: 1.2 $.
It defines the structure and meaning of all SLAs written in this version
of the language. New revisions of the language may be published from
time to time. However, SLAs written in a particular revision of the
language retain the interpretation documented in the specification of the
original revision in which they were written.
WARNING: The constraints in this version of the language have not been
validated, so may not correspond to the intent stated in any accompanying
informal comments. If you wish to use SLAng to write electronic service
SLAs, you may wish to wait for a subsequent version that has been validated.
Please contact j.skene@cs.ucl.ac.uk for more information.
WARNING: The document you are reading may have been automatically generated
from the definitive specification of this version of the language, which is
located at http://www.cs.ucl.ac.uk/staff/j.skene/slang/slangv1.emof.
If so, the document you are reading is not definitive.
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 SLAs
and parts of SLAs described in the syntactic part of the model, are
descriptions of SLAs in the real world. The types of services, parties
and data described in the semantic part of the model are descriptions
of these things as they exist in the real world.
This specification offers several things:
1. A definition of when an agreement on a SLAng SLA exists
and 2. A definition of how the parties and services related to an SLA should
behave if an SLA is in force and being respected.
and 3. A definition of what violations should be calculated in relation to
a particular set of evidence concerning the behaviour of services and
parties.
and 4. A definition of which penalties specified in the SLA should be levied
against parties when particular types of violation are detected.
and 5. Informal comments on the use of the language and its meaning, which
are not definitive, and cannot be used in any determination of violations
or allocations of penalties.
An agreement exists on a SLAng SLA under the following conditions:
1. An object (the 'SLA') exists in the real world, conforming to
one of the concrete SLA types defined in this specification, according to
the definition of type conformance given below.
and 2. The parties referenced by that SLA have agreed that an agreement
exists.
For every type of real-world object relevant to SLAng SLAs, 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.
Because this definition recursively requires the properties of an object
to conform to the types specified in this specification, an SLA document
is only a SLAng SLA if all of its components conform to the structures and
definitions described in this specification, and if it is associated
with a real service provision scenario as modelled in this specification.
How parties should behave:
Certain wellformedness or multiplicity constraints included in this
specification oblige parties to an SLA to cooperate to ensure that the
SLA is administered. If these constraints are violated, it indicates
that a party is not cooperating in administering the agreement. The
agreement is thus broken and it makes no sense to define penalties in
such a case, as the party at fault could equally refuse to cooperate in
suffering such penalties. In such an event the remaining parties must
perform whatever action needs to be taken to recover or dissolve the
agreement to their satisfaction.
What violations should be calculated:
Violations are a type of object in this model, associated with
administration events, which occur when the parties cooperate to determine
violations and award penalties. Wellformedness constraints relate
the evidence presented by the parties to the existence of violations. They
also relate that evidence to the actual performance of the service, such
that it is an obligation for parties to present only complete and
correct evidence pertaining to the behaviour of a service during an
administrative period.
What penalties should be applied:
Violations are related to penalties defined in the SLA that has been
violated, and to parties responsible for causing the violation. These
relationships are defined in the model using wellformedness constraints.
The penalty that should be levied is the penalty related to the violation,
and it should be levied against the party indicated as the violator in the
violation.
Informal advice:
Non-definitive comments in this specification are labelled as "Informal:".
The remainder of this preamble is hence informal.
Informal:
This is an attempt to define a class of agreements based on SLAs defined
in a technical language. The boilerplate text above bootstraps the
effect of any agreement by establishing a basis for interpreting this
specification. However, it is not particularly helpful for knowing how
to use the language.
In practice the language should be used as follows:
- The provider and client of a service get together and agree that the
service should be provided.
- Both provider and client read this specification, which is definitive,
and any other documentation, which is not definitive but which may be
helpful, to determine if this language is going to be suitable for
defining the kind of agreement they want to make about the service that
is to be provided.
- The provider and client cooperate to define the terms for the agreement.
These establish what service is being constrained by the SLA. Terms are
directly related to domain elements defined in this specification for the
purpose of defining the semantics of the language, so it is helpful to look
at the domain model, and check that the service being defined is going to
behave in the same way as those elements, because that is the statement that
you make when you define your terms.
- The provider and client cooperate to determine what condition clauses
should be included in the SLA, and what their parameters should be.
Some clauses interact, so wellformedness constraints insist that if one
is present then others are needed. Parameters will imply constraints
on the service that are described by violation constraints, so consider
what these constraints mean when picking them.
- The provider and client cooperate to determine schedules for the
conditions.
- The provider and client cooperate to determine penalties associated with
violations, and procedures for delivering those penalties to each other.
- The provider and client cooperate to determine a schedule for
administering the SLA. Administering the SLA consists of cooperating to
determine what violations have occurred, and thereby starting the
process of making good on penalties.
- The SLA is shown to be wellformed by evaluating the wellformedness
constraints on a representation of the SLA as objects.
- The provider and client, having cooperated to write an SLA, agree that
an agreement on that SLA exists, and the SLA comes into force.
- The provider and client cooperate to administer the SLA according to
the procedure specified in the SLA. Should either party violate the SLA
by reneging on this responsibility, the other party takes any action they
see fit.
Contents:
Informal: Contains types used in both the syntactic or semantic model.
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).
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
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)
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:
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.
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.
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.
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.
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.
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:
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 > 1 then
(n - (r - 1)) * pick(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) : ::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:
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: 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()
-
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
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:
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:
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:
Extends: ::slang::Definition
Definitive: A definition of some person or organisation with a role to
play in the service provision scenario.
Properties:
Operations:
Invariants:
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:
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:
Extends: ::slang::Definition
Definitive: A service definition identifies the service being
constrained by an SLA.
Properties:
Operations:
Invariants:
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:
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:
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:
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:
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:
Informal: The es package defines all types of objects that are used only
in the syntax of SLAng electronic service SLAs. At present electronic
service SLAs are the only well defined type of SLA in SLAng. However,
in the future there may be more types, possibly including ISP and
hosting SLAs.
Definitive: This enumeration type is used to identify the type
of a failure mode definition.
- PARAMETER
Definitive: The operation fails for a particular combination
of parameters.
- OPERATION
Definitive: The operation fails in some way for any combination
of parameters.
- DATA
Definitive: The service fails in some way when accessing a
data type.
- SERVICE
Definitive: The service fails in some way regardless of the
operation attempted and the parameters submitted.
Extends: ::slang::AdministeredSLA
Definitive: Electronic Service SLAs are a type of SLAng SLA
that places constraints on the use and operation of electronic
services.
Properties:
Operations:
Invariants:
-
Wellformedness: Accounts submitted during the administration
of an electronic service SLA should be electronic service
accounts.
administration.reconciliation->forAll(
r : ::services::Reconciliation |
r.agreed.oclIsTypeOf(
::services::es::ElectronicServiceAccount)
)
-
Wellformedness: The terms of an ES SLA should be electronic
service terms.
terms = electronicServiceTerms
-
Wellformedness: The conditions of an ES SLA should be electronic
service conditions.
conditions = electronicServiceConditions
Extends: ::slang::Terms
Definitive: Electronic service terms are a set of definitions
forming part of a SLAng ES SLA.
Properties:
Operations:
Invariants:
Extends: ::slang::ServiceDefinition
Definitive: An electronic service definition unambiguously
identifies the service being provided in the service provision
scenario that is being governed by a SLAng ES SLA. If reliability
constraints are included in the SLA, the electronic service
definition should include or refer to a description of the service
from which it is possible to determine the correct functional
behaviour of the operations of the service.
Informal: The degree of ambiguity in any referenced description of
the service will affect the precision of the SLA with regards
to reliability properties. The description should hence be as
precise as is practically possible.
Properties:
Operations:
Invariants:
Extends: ::slang::Definition
Definitive: An operation definition unambiguously identifies an
operation of the electronic service being provided in the
service provision scenario that is being governed by a SLAng ES
SLA. If a functional description of the service is provided or
referenced in the service description provided in the same
ES SLA, then all operation definitions should reference or
reproduce parts of that description pertaining to the operation
being identified. This is in order that reliability clauses
associated with the operation definition can be identified with
a specification of their functional behaviour.
Operation definitions also define a timeout for the operation.
Requests for which responses are not received within the timeout
period are regarded as failures, and should have no effect on
the behaviour of the service.
Informal: An operation is a part of the interface between the
client and provider of the service. The client may submit requests
to the operation, and in due course expect to receive a response.
Properties:
- failure : ::slang::es::AnticipatedFailureDefinition[0, *] unique
Opposite: ::slang::es::AnticipatedFailureDefinition.operation : ::slang::es::OperationDefinition
Definitive: Components of the description of an operation are
descriptions of known ways in which the operation may fail.
Informal: These failure modes may be referred to in the
definition of conditions relating to retries and
unavailability.
- accessedData : ::slang::es::DataTypeDefinition[0, *] unique
Opposite: ::slang::es::DataTypeDefinition.operation : ::slang::es::OperationDefinition[0, *] unique
Definitive: An operation definition refers to the data
type definitions for the types of data that it accesses.
- terms : ::slang::es::ElectronicServiceTerms
Opposite: ::slang::es::ElectronicServiceTerms.operationDefinition : ::slang::es::OperationDefinition[1, *]
Definitive: Operation definitions are a part of the
terms of a SLAng electronic-service SLA.
- operation : ::services::es::Operation
Definitive: An operation definition describes an operation
in the real world.
- timeout : ::types::Duration[0, 1]
Definitive: Operation definitions may define a timeout for
the operations with which they are associated. If a response
is not delivered to the client within the timeout period
following the submission of a request, the request is deemed
to have failed and should have no effect on the state of the
service. If a timeout is not specified for an operation then
the timeout should be specified in the description of the
operation referenced or included in the description field of
the definition clause, or the operation should not be referred
to in any reliability clause.
- dateMeasurementAccuracy : ::types::Duration
Definitive: Operation definitions specify a margin of error
within which the parties are expected to measure the instant
at which the request began to be submitted, with a confidence
also specified in the definition.
- durationMeasurementAccuracy : ::types::Duration
Definitive: Operation definitions specify a margin of error
within which the parties are expected to measure the true
duration between the instant that a request begins to be
submitted to the service, and the instance when receipt of
a response is completed, with a confidence
also specified in the definition.
Operations:
Invariants:
Extends: ::slang::Definition
Definitive: Defines a known failure mode of an operation. Should
reproduce or refer to sections of the description of the service
provided in the service definition in the same ES SLA.
Informal: Anticipated failure definitions are used to identify
sections of the description of the service that identify failure
behaviour related to an operation. If this identification is
omitted from the SLA, the service provider could argue that
the behaviour represents a normal mode of operation for the service
and should therefore not incur penalties under the agreement.
Properties:
Operations:
Invariants:
Extends: ::slang::Definition
Definitive: Defines a type of data manipulated by the service.
Informal: Data types should be defined in the manner most convenient
for defining recovery clauses and failure modes.
Properties:
Operations:
Invariants:
Definitive: Defines a class of failure. This can be failed or
overdue responses from operations, the service as a whole, or
an operation that fails repeatedly with a particular combination
of parameters. It can also be failure to access up-to-date
information.
Informal: Failure modes define the type of failure that reliability
and availability clauses constrain.
Properties:
- kind : ::slang::es::FailureModeKind
Definitive: Failure mode definitions identify the kind of
failure mode being described.
Informal: Can be PARAMETER, OPERATION, DATA or SERVICE.
- operations : ::slang::es::OperationDefinition[0, *] unique
Definitive: If kind is PARAMETER or OPERATION then the
clause must specify to what operations the clause applies.
- states : ::slang::StateDefinition[0, *] unique
Definitive: If kind is PARAMETER, OPERATION or SERVICE then the
failure mode may be qualified by a set of states. The service
or world must be occupying at least one of these states for any
failure or overdue response to contribute to the failure mode.
- dataTypes : ::slang::es::DataTypeDefinition[0, *] unique
Definitive: If this failure mode definition is of the DATA kind,
then in combination with a reliability clause it can be used to
place constraints on the reliability of operations access data
of these types. The operations will have to access the youngest
data of the types associated with this clause, that is also
older than the minimum age specified, with at least the
reliability specified in the reliability clause.
- maximumLatency : ::types::Duration[0, 1]
Definitive: If this failure mode definition is not of the DATA
kind, then it should define a maximum amount of time that
operations associated with this clause should take to return a
response to the client. This applies to all operations if
the failure mode is of the service kind.
- minimumAge : ::types::Duration[0, 1]
Definitive: If this failure mode definition is of the DATA kind,
then in combination with a reliability clause it can be used to
place constraints on the reliability of operations access data
of these types. The operations will have to access the youngest
data of the types associated with this clause, that is also
older than this minimum age, with at least the
reliability specified in the reliability clause.
Informal: A minimum age may be specified because it is
often impossible for a service to guarantee that the most
up-to-date data of a particular type will be available, due
to concurrency or the need to process data in batches. If the
kind of this definition is DATA, then a minimum age must be
specified for wellformedness, but may be specified as zero.
- terms : ::slang::es::ElectronicServiceTerms
Opposite: ::slang::es::ElectronicServiceTerms.failureModeDefinition : ::slang::es::FailureModeDefinition[0, *] unique
Definitive: Failure mode definitions are a component of a
collection of terms in an electronic service SLA.
- overriddenMode : ::slang::es::FailureModeDefinition[0, *] unique
Opposite: ::slang::es::FailureModeDefinition.overriddenBy : ::slang::es::FailureModeDefinition[0, *] unique
Definitive: A failure mode may be overridden by another
failure mode. If a failure is in both modes, it will only
count towards the overriding mode in any reliability constraint.
Informal: This can be used to avoid assigning parameter mode
penalties when an operation mode penalty also applies, or
similarly to control penalties when failures occur while the
service in several overlapping states.
- overriddenBy : ::slang::es::FailureModeDefinition[0, *] unique
Opposite: ::slang::es::FailureModeDefinition.overriddenMode : ::slang::es::FailureModeDefinition[0, *] unique
Definitive: A failure mode may be overridden by other modes
Operations:
- isOfFailureMode(attempt : ::services::es::ServiceUsageRecord) : ::types::Boolean
Informal: Evaluates to true if attempt is of this failure mode.
Evaluates to:
if kind = FailureModeKind.PARAMETER
then
operations->includes(attempt.operation)
and
(
not (attempt.outcome =
::services::es::Outcome.SUCCEEDED)
or
attempt.duration.inMs() > maximumLatency.inMs()
)
and
states->exists(s : ::slang::StateDefinition |
attempt.states->includes(s)
)
else
if kind = FailureModeKind.OPERATION
then
operations->includes(attempt.operation)
and
(
not (attempt.outcome =
::services::es::Outcome.SUCCEEDED)
or
attempt.duration.inMs() > maximumLatency.inMs()
)
and
states->exists(s : ::slang::StateDefinition |
attempt.states->includes(s)
)
else
if kind = FailureModeKind.DATA
then
attempt.dataFailureModes->exists(
mode : FailureModeDefinition |
mode = self
)
and
attempt.outcome =
::services::es::Outcome."DATA_ACCESS_ERROR"
else
if kind = FailureModeKind.SERVICE
then
attempt.request.operation.electronicService =
terms.electronicServiceDefinition.
electronicService
and
(
not (attempt.outcome =
::services::es::Outcome.SUCCEEDED)
or
attempt.duration.inMs() >
maximumLatency.inMs()
)
and
states->exists(s : ::slang::StateDefinition |
attempt.states->includes(s)
)
else
false
endif
endif
endif
endif
- overrides(m : ::slang::es::FailureModeDefinition) : ::types::Boolean
Informal: Evaluates whether this mode overrides a specified
mode.
Evaluates to:
overriddenMode->includes(m)
or
overriddenMode->exists(sub : FailureModeDefinition |
sub.overrides(m)
)
- eq(otherMode : ::slang::es::FailureModeDefinition) : ::types::Boolean
Informal: Evaluates to true if the other mode describes exactly
the same failures as this mode.
Evaluates to:
kind = otherMode.kind
and
operations = otherMode.operations
and
dataTypes = otherMode.dataTypes
and
minimumAge = otherMode.minimumAge
and
states = otherMode.states
Invariants:
-
Wellformedness: All operation definitions referred to by this
definition must be components of the same set of terms.
operations->forAll(o : OperationDefinition |
o.terms = terms
)
-
Wellformedness: All data type definitions referred to by this
definition must be components of the same set of terms.
dataTypes->forAll(d : DataTypeDefinition |
d.terms = terms
)
-
Wellformedness: A parameter type failure mode must specify
an operation. An operation type failure mode must also
specify an operation. A data failure mode must specify
at least one data type and a minimum age for the data. A
service failure type should specify nothing, as it will be
automatically associated with the service constrained by
the SLA in which it is contained.
if kind = FailureModeKind.PARAMETER
then
operations->size() > 0
and
dataTypes->size() = 0
and
minimumAge.oclIsUndefined()
else
if kind = FailureModeKind.OPERATION
then
operations->size() > 0
and
dataTypes->size() = 0
and
minimumAge.oclIsUndefined()
else
if kind = FailureModeKind.DATA
then
operations->size() = 0
and
dataTypes->size() > 0
and
(not minimumAge.oclIsUndefined())
else
if kind = FailureModeKind.SERVICE
then
operations->size() = 0
and
dataTypes->size() = 0
and
minimumAge.oclIsUndefined()
else
false
endif
endif
endif
endif
-
Wellformedness: No failure mode description overridden by this
failure mode should override this failure mode.
overriddenMode->forAll(m : FailureModeDefinition |
not m.overrides(self)
)
-
Wellformedness: All events causing transitions into states in
which the failure mode is defined must be mutually monitorable
by the client and provider of the agreement. This constraint
asserts that mutual monitorability must be preserved even when
referring to the state of external systems or state transitions
of the service other than those caused by requests and
responses.
states.state.outgoingTransitions->union(
states.state.incomingTransitions)->forall(
t : ::services::StateTransition |
t.event.witnesses->includes(
terms.clientDefinition.party)
and
t.event.witnesses->includes(
terms.providerDefinition.party)
)
-
Wellformedness: No failure mode description overridden by this
failure mode should override any other.
Informal: This invariant ensures SLA specifications are as
concise as possible, and is included largely to assist the
author in choosing sensible sets of states when defining
failure modes.
overriddenMode->forAll(m1 : FailureModeDefinition,
m2 : FailureModeDefinition |
not m1.overrides(m2)
)
Extends: ::slang::Conditions
Definitive: Electronic service conditions are the part of a SLAng
electronic service SLA that defines the parameters for the
constraints implied by the SLA over the service to which it is
applied.
Properties:
- securityProvisions : ::types::String[0, 1]
Definitive: The SLA contains a field allowing the specification
of the security provisions relating to access to the SLA. This
field has no associated semantic definition, and is provided
as a convenience to the parties to the agreement. The parties
should ensure before agreeing to an SLA that they agree with
the contents of this field, and that their mutual understanding
is consistent. No penalties are associated with deviations
from the content of this field, but to do so would invalidate
the agreement as written, and require at minimum a
renegotiation of the SLA. The field may be left blank.
- inputThroughputClause : ::slang::es::InputThroughputClause[0, *] unique
Opposite: ::slang::es::InputThroughputClause.conditions : ::slang::es::ElectronicServiceConditions
Definitive: Electronic service conditions may contain input
throughput clauses, which limit the rate at which requests
can be delivered to the service.
- outputThroughputClause : ::slang::es::OutputThroughputClause[0, *] unique
Opposite: ::slang::es::OutputThroughputClause.conditions : ::slang::es::ElectronicServiceConditions
Definitive: Electronic service conditions may contain output
throughput clauses, which limit the rate at which reponses
can be returned by the service.
- reliabilityClause : ::slang::es::ReliabilityClause[0, *] unique
Opposite: ::slang::es::ReliabilityClause.conditions : ::slang::es::ElectronicServiceConditions
Definitive: Electronic service conditions may contain
reliability clauses, which constrain the number of failures
in specified modes that can be observed over a period of time.
- availabilityClause : ::slang::es::AvailabilityClause[0, *] unique
Opposite: ::slang::es::AvailabilityClause.conditions : ::slang::es::ElectronicServiceConditions
Definitive: Electronic service conditions may contain
availability clauses, which constrain the amount of time that
the service can be unavailable for a particular type of request
between an extended period of unreliability, and a communication
from the service provider indicating that a problem with the
service has been rectified.
- recoveryClause : ::slang::es::RecoveryClause[0, *] unique
Opposite: ::slang::es::RecoveryClause.conditions : ::slang::es::ElectronicServiceConditions
Definitive: Electronic service conditions may contain
recovery clauses, which constrain the age of data recovered
following a period of unavailability of data.
- electronicServiceSLA : ::slang::es::ElectronicServiceSLA
Opposite: ::slang::es::ElectronicServiceSLA.electronicServiceConditions : ::slang::es::ElectronicServiceConditions
Definitive: Electronic service conditions are part of an
electronic service SLA.
Operations:
Invariants:
Extends: ::slang::ScheduledClause
Definitive: Input throughput clauses place restrictions on the
rate at which request are submitted to the service by the
client program.
Properties:
Operations:
- relevantUsages(account : ::services::Account) : ::services::es::ServiceUsageRecord[0, *] unique
Informal: Evaluates to all usages occurring on the operations
associated with this clause, while the clause applies.
Evaluates to:
account.evidence->select(e : ::services::Evidence |
e.oclIsTypeOf(::services::es::ServiceUsageRecord)
)->collect(e : ::services::Evidence |
e.oclAsType(::services::es::ServiceUsageRecord)
)->select(r : ::services::es::ServiceUsageRecord |
self.applies(r.date.inMs())
and
self.operation->includes(r.operation)
)->asSet()
- inputTimes(account : ::services::Account) : ::types::Real[0, *]
Informal: Evaluates to the collection of times at which
service usages documented in the specified account returned
results.
Evaluates to:
relevantUsages(account)->collect(r :
::services::es::ServiceUsageRecord |
r.date.inMs()
)
- violationFirstUsage(account : ::services::Account) : ::services::es::ServiceUsageRecord[0, *] unique
Informal: Evaluates to the set of services usages occurring
first in each group of usages violating this clause.
Evaluates to:
relevantUsages(account)->select(r :
::services::es::ServiceUsageRecord |
inputTimes(account)->select(t : ::types::Real |
t >= r.date.inMs()
and
t < r.date.inMs()
)->size() > inputConcurrency + 1
)
- violationEvidence(account : ::services::Account,
first : ::services::es::ServiceUsageRecord) : ::services::es::ServiceUsageRecord[1, *] unique
Informal: Given the first usage in a group of usages violating
this clause, this operation evaluates to the complete group.
Evaluates to:
relevantUsages(account)->select(r :
::services::es::ServiceUsageRecord |
r.date.inMs() >= first.date.inMs()
and
r.date.inMs() < first.date.inMs()
)
Invariants:
-
Wellformedness: The schedules associated with this clause are
part of the same SLA as this clause.
schedule->forAll(s : ::slang::Schedule |
s.sLA = conditions.electronicServiceSLA
)
-
Informal: This clause is violated by groups of service requests
submitted too closely together. For each administration of
this SLA, for every violating group, a violation must be
recorded identifying the group, this clause, and the
client as the violator.
conditions.electronicServiceSLA.administration->forAll(
a : ::services::Administration |
violationFirstUsage(a.reconciliation.agreed)->forAll(
first : ::services::es::ServiceUsageRecord |
a.calculation.violation->one(
v : ::services::Violation |
v.violator =
conditions.sLA.terms.clientDefinition.party
and
v.violatedClause = self
and
v.penaltyDefinition = penalty
and
v.evidence = violationEvidence(
a.reconciliation.agreed, first)
)
)
)
-
Wellformedness: The operation definitions associated with this
clause are part of the same SLA as this clause.
operation->forAll(o : OperationDefinition |
o.terms.electronicServiceSLA =
conditions.electronicServiceSLA
)
-
Wellformedness: The penalty referenced by this clause is
part of the same SLA as this clause.
penalty.terms.sLA = conditions.sLA
Extends: ::slang::ScheduledClause
Definitive: Output throughput clauses place restrictions on the
rate at which responses are returned from the service to the
client program.
Informal: Output throughput clauses are only useful if responses
tend to be delivered to a single client that could be overwhelmed by
responses, and if input throughput and service performance clauses
permit responses to be delivered in bursts.
Properties:
Operations:
- relevantUsages(account : ::services::Account) : ::services::es::ServiceUsageRecord[0, *] unique
Informal: Evaluates to all usages occurring on the operations
associated with this clause, while the clause applies.
Evaluates to:
account.evidence->select(e : ::services::Evidence |
e.oclIsTypeOf(::services::es::ServiceUsageRecord)
)->collect(e : ::services::Evidence |
e.oclAsType(::services::es::ServiceUsageRecord)
)->select(r : ::services::es::ServiceUsageRecord |
self.applies(r.date.inMs())
and
self.operation->includes(r.operation)
)->asSet()
- outputTimes(account : ::services::Account) : ::types::Real[0, *]
Informal: Evaluates to the collection of times at which
service usages documented in the specified account returned
results.
Evaluates to:
relevantUsages(account)->collect(r :
::services::es::ServiceUsageRecord |
r.date.inMs() + r.duration.inMs()
)
- violationFirstUsage(account : ::services::Account) : ::services::es::ServiceUsageRecord[0, *] unique
Informal: Evaluates to the set of services usages occurring
first in each group of usages violating this clause.
Evaluates to:
relevantUsages(account)->select(r :
::services::es::ServiceUsageRecord |
outputTimes(account)->select(t : ::types::Real |
t >= r.date.inMs() + r.duration.inMs()
and
t < r.date.inMs() + r.duration.inMs()
)->size() > outputConcurrency + 1
)
- violationEvidence(account : ::services::Account,
first : ::services::es::ServiceUsageRecord) : ::services::es::ServiceUsageRecord[1, *] unique
Informal: Given the first usage in a group of usages violating
this clause, this operation evaluates to the complete group.
Evaluates to:
relevantUsages(account)->select(r :
::services::es::ServiceUsageRecord |
r.date.inMs() + r.duration.inMs() >=
first.date.inMs() + first.duration.inMs()
and
r.date.inMs() + r.duration.inMs() <
first.date.inMs() + first.duration.inMs()
)
Invariants:
-
Informal: This clause is violated by groups of service responses
occurring too closely together. For each administration of
this SLA, for every violating group, a violation must be
recorded identifying the group, this clause, and the
service provider as the violator.
conditions.electronicServiceSLA.administration->forAll(
a : ::services::Administration |
violationFirstUsage(a.reconciliation.agreed)->forAll(
first : ::services::es::ServiceUsageRecord |
a.calculation.violation->one(
v : ::services::Violation |
v.violator =
conditions.sLA.terms.providerDefinition.party
and
v.violatedClause = self
and
v.penaltyDefinition = penalty
and
v.evidence = violationEvidence(
a.reconciliation.agreed, first)
)
)
)
-
Wellformedness: The schedules associated with this clause are
part of the same SLA as this clause.
schedule->forAll(s : ::slang::Schedule |
s.sLA = conditions.electronicServiceSLA
)
-
Wellformedness: The penalty referenced by this clause is
part of the same SLA as this clause.
penalty.terms.sLA = conditions.sLA
-
Wellformedness: The operation definitions associated with this
clause are part of the same SLA as this clause.
operation->forAll(o : OperationDefinition |
o.terms.electronicServiceSLA =
conditions.electronicServiceSLA
)
Extends: ::slang::ScheduledClause
Definitive: Reliability clauses are part of SLAng ES SLAs,
and define the reliability characteristics that the server must
exhibit, and the penalties for the service provider if it does not.
Reliability clauses are associated with a number of failure modes,
and constrain the number of failures that can be seen in each
of those modes within the duration of a sliding window. This
effectively defines the amount of time that can be wasted in bad
usages during such a window. The time wasted by a particular
failure is determined as being the reciprocal of the minimum
input-throughput constraint applying to the client concurrently,
as on average this represents the amount of time that the client
is obliged to wait before trying again.
The notion of the sliding window implies a notion of a period of
unreliability, within which all possible positions for the
window violate the reliability property. Each period of
unreliability for an operation associated with this clause
implies one violation of this clause.
Properties:
Operations:
- usages(account : ::services::Account,
startDate : ::types::Real,
endDate : ::types::Real) : ::services::es::ServiceUsageRecord[0, *] unique
Informal: Evaluates to the set of usage records included in
the specified account and recorded as occurring between
the specified start and end dates.
Evaluates to:
account.evidence->select(e : ::services::Evidence |
e.date.inMs() <= startDate
and
e.date.inMs() >= endDate
and
e.oclIsTypeOf(::services::es::ServiceUsageRecord)
)->collect(e : ::services::Evidence |
e.oclAsType(::services::es::ServiceUsageRecord)
)->asSet()
- relevantFailures(account : ::services::Account,
failureMode : ::slang::es::FailureModeDefinition,
parameters : ::services::es::ParameterRecord[0, *] unique ordered,
startDate : ::types::Real,
endDate : ::types::Real) : ::services::es::ServiceUsageRecord[0, *] unique
Informal: Evaluates to the set of failures described in the
account as occurring between the dates specified on the
operation specified.
Evaluates to:
usages(account, startDate, endDate)->select(
r : ::services::es::ServiceUsageRecord |
failureMode.isOfFailureMode(r)
and
not conditions.availabilityClause->exists(
clause : AvailabilityClause |
clause.failureModes->exists(
other : FailureModeDefinition |
other.overrides(failureMode)
)
and
clause.unavailableAtTime(account,
failureMode, parameters, r.date.inMs())
)
and
(
failureMode.kind = FailureModeKind.PARAMETER
implies
failureMode.operations->includes(r.operation)
and
r.parameters->size() = parameters->size()
and
Sequence(::types::Integer)
{ 1..parameters->size() }->forAll(
i : ::types::Integer |
r.parameters->at(i).value =
parameters->at(i).value
)
)
)->asSet()
- minThroughput(t : ::types::Real,
o : ::slang::es::OperationDefinition) : ::types::Real
Informal: Calculates the minimum average throughput allowable
on an operation at a particular time; evaluates to -1 if no
constraint applies.
Evaluates to:
conditions.inputThroughputClause->select(
c : InputThroughputClause |
c.operation->includes(o)
and
c.applies(t)
)->collect(c : InputThroughputClause |
c.inputConcurrency / c.inputWindow.value
)->iterate(next : ::types::Real;
least : ::types::Real = -1 |
if least < 0 then next
else least.min(next)
endif
)
- timeWastedByFailure(failure : ::services::es::ServiceUsageRecord) : ::types::Real
Informal: Evaluates to the amount of time that the client
wastes on a particular failure.
Evaluates to:
if minThroughput(failure.date.inMs(),
failure.operation) <= 0 then 0
else 1 / minThroughput(failure.date.inMs(),
failure.operation)
endif
- timeWastingLimit() : ::types::Real
Informal: Evaluates the amount of time that can be wasted by
failures within the sliding window.
Evaluates to:
window.inMs() * (1 - reliability.value)
- timeWastedByFailures(failures : ::services::es::ServiceUsageRecord[0, *] unique) : ::types::Real
Informal: Returns the amount of time wasted by an ordered
set of failures.
Evaluates to:
failures->iterate(
failure : ::services::es::ServiceUsageRecord;
wasted : ::types::Real = 0 |
wasted + timeWastedByFailure(failure)
)
- failuresInWindow(first : ::services::es::ServiceUsageRecord,
failures : ::services::es::ServiceUsageRecord[0, *] unique) : ::services::es::ServiceUsageRecord[0, *] unique
Informal: Evaluates to the set of failures following the
first in a window.
Evaluates to:
failures->select(sequenceElement :
::services::es::ServiceUsageRecord |
sequenceElement.date.inMs() >
first.date.inMs()
and
sequenceElement.date.inMs() <=
first.date.inMs() + window.inMs()
)
- timeWastedInWindow(first : ::services::es::ServiceUsageRecord,
failures : ::services::es::ServiceUsageRecord[0, *] unique) : ::types::Real
Informal: Evaluates to the total amount of time wasted in
a window, identified by the first failure in the window.
Evaluates to:
timeWastedByFailures(
failuresInWindow(first, failures)->including(first))
- firstSignificantFailures(failures : ::services::es::ServiceUsageRecord[0, *] unique) : ::services::es::ServiceUsageRecord[0, *] unique
Informal: Returns the failures that begin a period of
unreliability.
Evaluates to:
failures->select(failure :
::services::es::ServiceUsageRecord |
timeWastedInWindow(failure, failures) >
timeWastingLimit()
and
not failures->exists(earlier :
::services::es::ServiceUsageRecord |
not (earlier = failure)
and
earlier.date.inMs() < failure.date.inMs()
and
timeWastedInWindow(earlier, failures) >
timeWastingLimit()
and
failureSequence(earlier, failures)->includes(
failure)
)
)
- failureSequence(first : ::services::es::ServiceUsageRecord,
failures : ::services::es::ServiceUsageRecord[0, *] unique) : ::services::es::ServiceUsageRecord[0, *] unique
Informal: Starting from a failure that begins a period of
unreliability, returns all of the failures in that period
of unreliability.
Evaluates to:
if timeWastedInWindow(first, failures) < timeWastingLimit()
then
Set(::services::es::ServiceUsageRecord)
{ first }
else
failuresInWindow(first, failures)->iterate(
failure : ::services::es::ServiceUsageRecord;
allFailures :
Set(::services::es::ServiceUsageRecord) =
Set(::services::es::ServiceUsageRecord)
{ first } |
allFailures->union(
failureSequence(failure, failures))
)
endif
- failureSequenceStart(failureSequence : ::services::es::ServiceUsageRecord[0, *] unique) : ::types::Real
Informal: Given a sequence of failures, calculates the
date of the earliest failure.
Evaluates to:
if failureSequence->size() = 0
then -1
else
failureSequence->iterate(
next : ::services::es::ServiceUsageRecord;
earliest : ::types::Real = -1 |
if earliest = -1
then
next.date.inMs()
else
if next.date.inMs() < earliest
then
next.date.inMs()
else
earliest
endif
endif
)
endif
- failureSequenceEnd(failureSequence : ::services::es::ServiceUsageRecord[0, *] unique) : ::types::Real
Informal: Given a sequence of failures, calculates the end
of the failure sequence, which is latest end of a period of
wasted time caused by any of the failures.
Evaluates to:
if failureSequence->size() = 0
then -1
else
failureSequence->iterate(
next : ::services::es::ServiceUsageRecord;
latest : ::types::Real = -1 |
if latest = -1
then
next.date.inMs()
else
if next.date.inMs() +
timeWastedByFailure(next) > latest
then
next.date.inMs() + timeWastedByFailure(next)
else
latest
endif
endif
)
endif
- failureSequenceLength(failureSequence : ::services::es::ServiceUsageRecord[0, *] unique) : ::types::Real
Informal: Given a failure sequence, returns the length of the
failure sequence in mS.
Evaluates to:
if failureSequence->size() > 0
then
failureSequenceEnd(failureSequence) -
failureSequenceStart(failureSequence)
else
0
endif
- applicablePenalty(failureSequence : ::services::es::ServiceUsageRecord[0, *] unique) : ::slang::PenaltyDefinition[0, 1]
Informal: Calculates the applicable penalty for a failure
sequence. This is defined by the unreliability penalty clause
associated with this clause with the largest period less than
the duration of the failure sequence.
Evaluates to:
penalties->any(penalty : UnreliabilityPenaltyClause |
penalty.lengthOfPeriod.inMs() <=
failureSequenceLength(failureSequence)
and
not penalties->exists(
other : UnreliabilityPenaltyClause |
other.lengthOfPeriod.inMs() >
penalty.lengthOfPeriod.inMs()
and
penalty.lengthOfPeriod.inMs() <=
failureSequenceLength(failureSequence)
)
).penalty
Invariants:
-
Wellformedness: For all adminstrations of the SLA, and all
failure modes associated with this reliability clause,
if the failure mode is of the parameter kind look at
each usage occuring in a period during which this clause
applies, find all the failure sequences associated with that
combination of parameters, and apply a penalty for each of those
sequences according to their length.
If the failure mode is not of the parameter kind, then consider
all failure sequences occuring whenever this clause applies
of the kind prescribed by the failure mode regardless of the
value of the parameters, and apply a penalty
for each of those sequences according to their length.
conditions.electronicServiceSLA.administration->forAll(
a : ::services::Administration |
failureModes->forAll(
failureMode : FailureModeDefinition |
if(failureMode.kind = FailureModeKind.PARAMETER)
then
startDates()->forAll(startDate : ::types::Real |
usages(a.reconciliation.agreed, startDate,
endDate(startDate))->forAll(
usage : ::services::es::ServiceUsageRecord |
firstSignificantFailures(
relevantFailures(
a.reconciliation.agreed,
failureMode,
usage.parameters,
startDate,
endDate(startDate)))->forAll(
failure : ::services::es::ServiceUsageRecord |
a.calculation.violation->one(v : ::services::Violation |
v.violator = conditions.sLA.
terms.providerDefinition.
party
and
v.violatedClause = self
and
v.penaltyDefinition =
applicablePenalty(
failureSequence(failure,
relevantFailures(
a.reconciliation.agreed,
failureMode,
usage.parameters,
startDate,
endDate(startDate))))
and
v.evidence =
failureSequence(failure,
relevantFailures(
a.reconciliation.agreed,
failureMode,
usage.parameters,
startDate,
endDate(startDate)))
)
)
)
)
else
startDates()->forAll(startDate : ::types::Real |
firstSignificantFailures(
relevantFailures(a.reconciliation.agreed,
failureMode,
OrderedSet(::services::es::ParameterRecord) {},
startDate,
endDate(startDate)))->forAll(
failure : ::services::es::ServiceUsageRecord |
a.calculation.violation->one(v : ::services::Violation |
v.violator = conditions.sLA.terms.
providerDefinition.party
and
v.violatedClause = self
and
v.penaltyDefinition =
applicablePenalty(
failureSequence(failure,
relevantFailures(
a.reconciliation.agreed,
failureMode,
OrderedSet(::services::es::ParameterRecord) {},
startDate,
endDate(startDate))))
and
v.evidence =
failureSequence(failure,
relevantFailures(
a.reconciliation.agreed,
failureMode,
OrderedSet(::services::es::ParameterRecord) {},
startDate,
endDate(startDate)))
)
)
)
endif
)
)
-
Wellformedness: The schedules associated with this clause are
part of the same SLA as this clause.
schedule->forAll(s : ::slang::Schedule |
s.sLA = conditions.electronicServiceSLA
)
Definitive: Unreliability penalty clauses are components of
reliability clauses, and relate a penalty to the duration of
a period of unreliability.
Properties:
- lengthOfPeriod : ::types::Duration
Definitive: All periods of unreliability, according to the
parent reliability clause, that are longer than this duration
incur the penalty specified in this clause for the service
provider, unless they incur a penalty specified in another
unreliability penalty clause with a longer length of period.
- penalty : ::slang::PenaltyDefinition
Definitive: All periods of unreliability, according to the
parent reliability clause, that are longer than the lenght
of period specified in this clause incur this penalty for the
service provider, unless they incur a penalty specified in
another unreliability penalty clause with a longer length of
period.
- reliabilityClause : ::slang::es::ReliabilityClause
Opposite: ::slang::es::ReliabilityClause.penalties : ::slang::es::UnreliabilityPenaltyClause[0, *]
Definitive: Unreliability penalty clauses are components of
reliability clauses.
Operations:
Invariants:
Extends: ::slang::ScheduledClause
Definitive: Availability clauses apply penalties to periods during
which the service is unavailable. A service becomes unavailable
either when the service provider issues a bug report to the client,
or if the client issues a bug report to the service provider
following a period of unreliability,
within the reporting time limit. Unavailability ends when the
provider issues a bug fix report to the client. Unavailability is
always relative to a particular failure mode.
Properties:
Operations:
- bugReports(account : ::services::Account) : ::services::ReportRecord[0, *] unique
Informal: Evaluates to the set of bug reports detailed by an
account of service behaviour.
Evaluates to:
account.evidence->select(e : ::services::Evidence |
e.oclIsTypeOf(::services::ReportRecord)
)->collect(e : ::services::Evidence |
e.oclAsType(::services::ReportRecord)
)->asSet()->select(
r : ::services::ReportRecord |
r.report.oclIsTypeOf(::services::es::BugReport)
)
- startsUnavailability(account : ::services::Account,
failureMode : ::slang::es::FailureModeDefinition,
parameters : ::services::es::ParameterRecord[0, *] unique ordered,
evidence : ::services::Evidence) : ::types::Boolean
Informal: Determines whether a report begins a period of
unavailability for a failure type associated with this clause.
The report must be legitimate, in that it is either
submitted by the provider or proceeded by
a period of unreliability.
Evaluates to:
not unavailableBefore(account, failureMode, parameters,
evidence.date.inMs())
and
evidence.oclIsTypeOf(::services::ReportRecord)
and
evidence.oclAsType(::services::ReportRecord).
report.oclIsTypeOf(::services::es::BugReport)
and
(
-- Same failure type and parameters
failureModes->exists(
own : FailureModeDefinition |
own.eq(evidence.oclAsType(::services::ReportRecord).
report.oclAsType(::services::es::BugReport
).failureMode)
)
and
evidence.oclAsType(::services::ReportRecord).
report.oclAsType(::services::es::BugReport
).parameters = parameters
)
and
not conditions.availabilityClause->exists(
other : AvailabilityClause |
other.failureModes->exists(
otherMode : FailureModeDefinition |
otherMode.overrides(failureMode)
)
and
other.unavailableBefore(account, failureMode,
parameters, evidence.date.inMs())
)
and
(
evidence.oclAsType(::services::ReportRecord).
report.oclAsType(::services::es::BugReport
).dispatcher =
conditions.sLA.terms.providerDefinition.party
or
-- Must occur within a certain period of unreliability in
-- this failure mode (compatible service usages are
-- part of a period of unreliability)
account.reconciliationAsAgreed.administration.
calculation.violation->exists(
v : ::services::Violation |
v.violatedClause.oclIsTypeOf(ReliabilityClause)
and
v.violatedClause.oclAsType(ReliabilityClause).
failureModes->exists(
other : FailureModeDefinition |
other.eq(failureMode)
)
and
v.evidence->exists(other : ::services::Evidence |
other.date.inMs() <= evidence.date.inMs()
and
other.date.inMs() >=
evidence.date.inMs() - reportingLimit.inMs()
)
and
v.evidence->forAll(e : ::services::Evidence |
failureMode.isOfFailureMode(
e.oclAsType(::services::es::ServiceUsageRecord))
)
and
failureMode.kind = FailureModeKind.PARAMETER
implies
v.evidence->forAll(e : ::services::Evidence |
e.oclAsType(::services::es::ServiceUsageRecord).
parameters = parameters
)
)
)
- endsUnavailability(account : ::services::Account,
failureMode : ::slang::es::FailureModeDefinition,
parameters : ::services::es::ParameterRecord[0, *] unique ordered,
evidence : ::services::Evidence) : ::types::Boolean
Informal: Evaluates whether a bug fix report ends a period
of unavailability started with a bug report.
Evaluates to:
unavailableBefore(account, failureMode, parameters,
evidence.date.inMs())
and
evidence.oclIsTypeOf(::services::ReportRecord)
and
evidence.oclAsType(::services::ReportRecord).
report.oclIsTypeOf(::services::es::BugFixReport)
and
(
evidence.oclAsType(::services::ReportRecord).
report.oclAsType(::services::es::BugFixReport
).failureMode.overrides(failureMode)
and
evidence.oclAsType(::services::ReportRecord).
report.oclAsType(::services::es::BugFixReport
).parameters = parameters
)
- unavailableAtTime(account : ::services::Account,
failureMode : ::slang::es::FailureModeDefinition,
parameters : ::services::es::ParameterRecord[0, *] unique ordered,
time : ::types::Real) : ::types::Boolean
Informal: Determines whether the system is unavailable according
to the failure mode of this clause, at a particular time. If
the failure mode is PARAMETER, this returns true if any
parameter unavailability is in effect.
Evaluates to:
account.evidence->exists(e : ::services::Evidence |
e.date.inMs() <= time
and
startsUnavailability(account, failureMode,
parameters, e)
and
not account.evidence->exists(
later : ::services::Evidence |
later.date.inMs() > e.date.inMs()
and
later.date.inMs() <= time
and
endsUnavailability(account, failureMode,
parameters, later)
)
)
- unavailableBefore(account : ::services::Account,
failureMode : ::slang::es::FailureModeDefinition,
parameters : ::services::es::ParameterRecord[0, *] unique ordered,
time : ::types::Real) : ::types::Boolean
Informal: Evaluates to whether the service was unavailable
before the specified time. It does this by determining whether
the system was unavailable at the date of the piece of
evidence concerning an event at the latest time before the time
specified.
Evaluates to:
unavailableAtTime(account, failureMode, parameters,
account.evidence->iterate(
next : ::services::Evidence;
latest : ::types::Real = -1 |
if
next.date.inMs() < time
and
next.date.inMs() > latest
then
next.date.inMs()
else latest
endif
)
)
- endOfUnavailabilityAfter(account : ::services::Account,
failureMode : ::slang::es::FailureModeDefinition,
parameters : ::services::es::ParameterRecord[0, *] unique ordered,
t : ::types::Real) : ::types::Real
Informal: Evaluates to the end date of any period of
unavailablity in effect or occurring after the specified time.
Evaluates to:
account.evidence->iterate(
next : ::services::Evidence;
earliest : ::types::Real = -1 |
if
endsUnavailability(account, failureMode, parameters,
next)
and
next.date.inMs() > t
then
if
earliest = -1
then
next.date.inMs()
else
if next.date.inMs() < earliest
then
next.date.inMs()
else
earliest
endif
endif
else
earliest
endif
)
- applicablePenalty(clauseStart : ::types::Real,
clauseEnd : ::types::Real,
unavailabilityStart : ::types::Real,
unavailabilityEnd : ::types::Real) : ::slang::PenaltyDefinition[0, 1]
Informal: Determines the applicable penalty based on the
duration of the period of unavailability.
Evaluates to:
penalties->any(penalty : UnavailabilityPenaltyClause |
penalty.lengthOfPeriod.inMs() <=
clauseEnd.min(
if unavailabilityEnd = -1
then clauseEnd
else unavailabilityEnd
endif
) - clauseStart.max(unavailabilityStart)
and
not penalties->exists(
other : UnavailabilityPenaltyClause |
other.lengthOfPeriod.inMs() >
penalty.lengthOfPeriod.inMs()
and
penalty.lengthOfPeriod.inMs() <=
clauseEnd.min(
if unavailabilityEnd = -1
then clauseEnd
else unavailabilityEnd
endif
) - clauseStart.max(unavailabilityStart)
)
).penalty
Invariants:
-
Wellformedness: For each administration of the SLA, and each
failure mode associated with this clause, determine periods
of unavailability, and ensure that violations correspond
and are associated with the applicable penalty based on the
length of the period of unavailability.
conditions.electronicServiceSLA.administration->forAll(
a : ::services::Administration |
failureModes->forAll(
failureMode : FailureModeDefinition |
bugReports(a.reconciliation.agreed)->forAll(
record : ::services::ReportRecord |
startsUnavailability(a.reconciliation.agreed,
failureMode,
record.report.oclAsType(::services::es::BugReport).parameters,
record)
implies
startDates()->forAll(start : ::types::Real |
record.date.inMs() < endDate(start)
and
endOfUnavailabilityAfter(
a.reconciliation.agreed,
failureMode,
record.report.oclAsType(
::services::es::BugReport).parameters,
start) > start
and
(not applicablePenalty(
start, endDate(start),
record.date.inMs(),
endOfUnavailabilityAfter(
a.reconciliation.agreed,
failureMode,
record.report.oclAsType(
::services::es::BugReport).
parameters,
start)).oclIsUndefined())
implies
a.calculation.violation->one(
v : ::services::Violation |
v.violator = conditions.sLA.terms.
clientDefinition.party
and
v.violatedClause = self
and
v.penaltyDefinition = applicablePenalty(
start, endDate(start),
record.date.inMs(),
endOfUnavailabilityAfter(
a.reconciliation.agreed,
failureMode,
record.report.oclAsType(
::services::es::BugReport).
parameters,
start))
and
v.evidence = Set(::services::Evidence) {
record
}
)
)
)
)
)
Definitive: Unavailability penalty clauses are a component of an
availability clause that associates a penalties with a periods of
unavailability of particular minimum periods.
Properties:
- lengthOfPeriod : ::types::Duration
Definitive: All periods of unavailability, according to the
parent availability clause, that are longer than this duration
incur the penalty specified in this clause for the service
provider, unless they incur a penalty specified in another
unavailability penalty clause with a longer length of period.
- penalty : ::slang::PenaltyDefinition
Definitive: All periods of unavailability, according to the
parent availability clause, that are longer than the length
of period specified in this clause incur this penalty for the
service provider, unless they incur a penalty specified in
another unavailability penalty clause with a longer length of
period.
- availabilityClause : ::slang::es::AvailabilityClause
Opposite: ::slang::es::AvailabilityClause.penalties : ::slang::es::UnavailabilityPenaltyClause[1, *] unique
Definitive: The availability of which this unavailability
penalty clause is a component.
Operations:
Invariants:
Extends: ::slang::ConditionClause
Definitive: Recovery clauses are not scheduled, but apply whenever
a backup recovery report is submitted by the service provider
to the client (perhaps to end a period of unavailability related
to a data type failure mode) in respect of one of the data types
defined by the data type definitions associated with the recovery
clause.
Properties:
Operations:
- applicablePenalty(age : ::types::Real) : ::slang::PenaltyDefinition[0, 1]
Informal: Determines the applicable penalty given the age
of the recovered backup.
Evaluates to:
penalties->any(penalty : BackupAgePenaltyClause |
penalty.age.inMs() <= age
and
not penalties->exists(
other : BackupAgePenaltyClause |
other.age.inMs() > penalty.age.inMs()
and
penalty.age.inMs() <= age
)
).penalty
Invariants:
Definitive: A backup age penalty clause associate penalties with
certain ages of backups recovered. If a recovered backup is older
than the age specified, it incurs the penalty specified, unless
it incurs a penalty for being even older. The implication of
old backups being recovered is that some intermediate data has
been lost.
Properties:
- age : ::types::Duration
Definitive: All recovery reports, according to the
parent backup clause, that are longer than this age
incur the penalty specified in this clause for the service
provider, unless they incur a penalty specified in another
backup age penalty clause with a longer length of period.
- penalty : ::slang::PenaltyDefinition
Definitive: All recovery reports, according to the
parent backup clause, that are longer than the length
of period specified in this clause incur this penalty for the
service provider, unless they incur a penalty specified in
another backup age penalty clause with a longer length of
period.
- recoveryClause : ::slang::es::RecoveryClause
Opposite: ::slang::es::RecoveryClause.penalties : ::slang::es::BackupAgePenaltyClause[1, *] unique
Definitive: Backup age penalty clauses are components of
recovery clauses.
Operations:
Invariants:
Informal: This package contains types definitions for all of the types
of things that SLAng SLAs describe and constrain.
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:
- receivedReport : ::services::Report[0, *] unique
Opposite: ::services::Report.recipient : ::services::Party
Definitive: Parties may receive a number of reports.
Informal: Reports are communications from other parties outside
of the normal operation of a service.
- violation : ::services::Violation[0, *] unique
Opposite: ::services::Violation.violator : ::services::Party
Definitive: Parties may be responsible for violations of
SLAng service level agreements. This specification defines when
this occurs.
- evidence : ::services::Evidence[0, *] unique
Opposite: ::services::Evidence.owner : ::services::Party
Definitive: Parties own evidence relating to events occurring
in a service provision scenario, pertinent to determining violations
of SLAng SLAs.
- dispatchedReport : ::services::Report[0, *] unique
Opposite: ::services::Report.dispatcher : ::services::Party
Definitive: Parties dispatch reports to communicate outside of the
normal operation of a service.
- account : ::services::Account[0, *] unique
Opposite: ::services::Account.owner : ::services::Party[0, 1]
Definitive: Parties provide accounts of service behaviour for
reconciliation with other parties prior to the determination
of violations in the administration of an SLA.
- asset : ::services::Asset[0, *] unique
Opposite: ::services::Asset.owner : ::services::Party
Definitive: Parties own, and are hence responsible for, assets,
which are real world things, such as services.
Operations:
Invariants:
Definitive: Assets are objects in the real world that are identifiably
the property and hence responsibility of some party.
Properties:
Operations:
Invariants:
Extends: ::services::Asset
Definitive: Parties may own services, which are a type of asset.
Properties:
Operations:
Invariants:
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: 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()
)
-
Wellformedness: Initial states are a subset of all states of the
context.
initialStates->forall(s : State | states->includes(s))
Definitive: An event is the completion of some activity at a specific
instant of time.
Properties:
Operations:
Invariants:
Definitive: A possible condition of the service context.
Properties:
Operations:
Invariants:
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)
)
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:
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:
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:
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:
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: 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)
-
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: Reconciliation occurs before violation calculation.
reconciliation.date.inMs() < calculation.date.inMs()
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)
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:
-
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)
-
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 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)
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:
Informal: The ES package contains types specific to the description
of an electronic service provision scenario.
Definitive: This enumeration type is used to indicate the outcome
of a service usage in a service usage record.
- SUCCEEDED
Definitive: The service usage succeeded.
- NO_RESPONSE
Definitive: No response was received from the service.
- OBVIOUS_FAILURE
Definitive: The service usage was an obvious failure, related
to a known failure kind of the operation on which the usage
was invoked.
- NON_OBVIOUS_FAILURE
Definitive: The service usage was a non-obvious failure.
- DATA_ACCESS_ERROR
Definitive: The service usage resulted in a data access error.
Extends: ::services::Service
Definitive: An electronic service is a computing service delivered
by one party, the provider, to another, the client, using only
electronic communication under the normal operation of the
service, and not requiring the client to devote their own resources
to the completion of the service. For the purposes of this
specification, electronic services are accessed by the client
by the submission of requests to operations, which result in
responses. The only constraints on when the client may
submit requests are those specified in an SLAng SLA associated
with the service to which the client is party.
Properties:
Operations:
Invariants:
Definitive: An operation is part of the interface to an electronic
service. Requests may be submitted to operations by a client
program and in due course a response expected (although if the
service is not functioning correctly a response may not be
produced).
Properties:
Operations:
Invariants:
Extends: ::services::Event
Definitive: A service request is an event in which the client
submits a request to the service across the service interface.
Informal: This is a real-world event, described in this
specification for the purpose of explicating the responsibilities
of the parties for service monitoring. The wellformedness
invariants in ::services::es::ServiceUsageRecord describe the
relationship that reported monitoring data should bear to
service requests.
Properties:
Operations:
Invariants:
Definitive: Parameters are components of requests to electronic
services that allow the client to pass data to the service. A
parameter is also a component of a response that allows the service
to pass data back to the client.
Properties:
Operations:
Invariants:
Extends: ::services::Event
Definitive: Processing is activity performed on behalf of the
client by the service, initiated by a ServiceRequest. Processing
is not always performed following a request, because the service
may be unavailable. Processing may result in
a response being sent to the client, if it is successful or failure
does not prevent a response being sent. Processing is not
always successful. Processing may create or access some
data stored by the service on behalf of the client.
Informal: This is a real-world event, described in this
specification for the purpose of explaining that processing is
not always successful, and that services store and modify data.
These concepts are necessary to define aspects of service
monitoring and data restoration.
Properties:
Operations:
Invariants:
Extends: ::services::Event
Definitive: A response is a message sent to the client following
some processing, which in turn will have been initiated by a request
submitted by the client. If the service completed successfully
then the service response may return some data to the client in
the form of a parameter. However, responses may also indicate
an error condition.
Informal: This is a real-world event, described in this
specification for the purpose of explicating the responsibilities
of the parties for service monitoring. The wellformedness
invariants in ::services::es::ServiceUsageRecord describe the
relationship that reported monitoring data should bear to
service responses.
Properties:
Operations:
Invariants:
-
Wellformedness: Service responses are mutually monitorable by
the client and service provider.
witnesses->includes(processing.serviceRequest.client)
and
witnesses->includes(
processing.serviceRequest.operation.electronicService.
owner)
-
Wellformedness: Service responses are events in the context of
the service.
processing.serviceRequest.operation.electronicService.
context.events->includes(self)
Definitive: Data is information stored by a service on behalf of
a client. Data is created at a particular date. Any subsequent
modification of that data results in new data created when the
modification occurs. The original data continues to be an
object of this model, because it may be recoverable, or its
loss may be significant.
Informal: This description of data is used to define various
constraints whose intent is to ensure that service providers
protect their clients against data loss.
Properties:
Operations:
Invariants:
Definitive:
Properties:
Operations:
Invariants:
Extends: ::services::Account
Definitive:
Properties:
Operations:
Invariants:
Extends: ::services::Evidence
Definitive: A service usage record is a piece of evidence concerning
the use of a service. An episode of service usage incorporates
a request, possibly some processing, and possibly a response. A
service usage record records when the request was submitted
(subject to the error characteristics of the monitor responsible
for creating the record), records a possibly subjective outcome
for the episode, and if a response is returned, a duration for
the episode, from the request being issued to the response being
returned, again subject to error.
Informal: As a piece of evidence, a service usage record is
ultimately related to a particular SLA. The
subjective judgements made concerning the outcome of the usage
are related to the definitions included in that SLA.
Properties:
- duration : ::types::Duration[0, 1]
Definitive: Records the amount of time between the request and
the response.
- operation : ::slang::es::OperationDefinition
Definitive: Identifies the operation that was invoked in this
usage.
- states : ::slang::StateDefinition[0, *] unique
Definitive: States that the system was in when the request
was submitted.
- parameters : ::services::es::ParameterRecord[0, *] unique ordered
Opposite: ::services::es::ParameterRecord.serviceUsageAsParameter : ::services::es::ServiceUsageRecord
Definitive: Service usage records record the parameters
that were passed in the request.
- outcome : ::services::es::Outcome
Definitive: Records the outcome of the usage, relative to
the SLA with which the account containing this record is
associated, and relative to the behaviour of the service.
- request : ::services::es::ServiceRequest
Opposite: ::services::es::ServiceRequest.measurement : ::services::es::ServiceUsageRecord[0, *] unique
Definitive: Service usage records are the result of
recording a usage of the service, which starts with a request.
- result : ::services::es::ParameterRecord[0, 1]
Opposite: ::services::es::ParameterRecord.serviceUsageAsResult : ::services::es::ServiceUsageRecord[0, 1]
Definitive: If a result is returned by the service response
it is recorded as part of the service usage record.
Informal: No violation calculation relies on having a record
of the response. However, it can be useful during
reconciliation to identify failures relative to the
expected behaviour of the service.
- failureType : ::slang::es::AnticipatedFailureDefinition[0, 1]
Definitive: If the outcome is an obvious failure, then it will
be associated with a failure mode documented in the SLA
associated with the account of which this record forms a part.
- dataFailureModes : ::slang::es::FailureModeDefinition[0, *] unique
Definitive: The set of failure modes with unreliability
clauses in effect when this failure occurred.
Operations:
- failedDataModes() : ::slang::es::FailureModeDefinition[0, *] unique
Informal: Returns all of the data access clauses applying
to this usage, where the usage hasn't accessed all of the
data conforming to the datatypes mentioned in the clause
and which is older than the time specified in the clause, but
has not yet been superceded by new data.
Evaluates to:
account.reconciliationAsAgreed.administration.sLA->collect(
oclAsType(::slang::es::ElectronicServiceSLA)
).electronicServiceConditions.availabilityClause->asSet(
)->select(
clause : ::slang::es::AvailabilityClause |
clause.applies(date.inMs())
)->collect(clause : ::slang::es::AvailabilityClause |
clause.failureModes->select(
failureMode : ::slang::es::FailureModeDefinition |
failureMode.kind = ::slang::es::FailureModeKind.DATA
)
)->asSet()->select(
failureMode : ::slang::es::FailureModeDefinition |
not request.processing.data->includesAll(
failureMode.dataTypes.dataType.data->select(
data : Data |
data.created.inMs() <
self.date.inMs() - failureMode.minimumAge.inMs()
and
not failureMode.dataTypes.dataType.data->exists(
laterData : Data |
laterData.conformsTo->includesAll(
data.conformsTo)
and
laterData.created.inMs() <
self.date.inMs() -
failureMode.minimumAge.inMs()
and
laterData.created.inMs() >
data.created.inMs()
)
)
)
)
- dateAccuracy(sLA : ::slang::es::ElectronicServiceSLA) : ::types::Real
Informal: Determines the accuracy required by the parameter
sLA for the date measurement.
Evaluates to:
sLA.electronicServiceTerms.operationDefinition->any(
o : ::slang::es::OperationDefinition |
o.operation = self.operation
).dateMeasurementAccuracy.inMs()
- durationAccuracy(sLA : ::slang::es::ElectronicServiceSLA) : ::types::Real
Informal: Determines the accuracy required by the parameter
sLA for the duration measurement.
Evaluates to:
sLA.electronicServiceTerms.operationDefinition->any(
o : ::slang::es::OperationDefinition |
o.operation = self.operation
).durationMeasurementAccuracy.inMs()
- isDateAccurate(sLA : ::slang::es::ElectronicServiceSLA) : ::types::Boolean
Informal: Assesses whether the date measurement is accurate
according to the parameter sLA.
Evaluates to:
date.inMs() >= request.date.inMs() - dateAccuracy(sLA)
and
date.inMs() <= request.date.inMs() + dateAccuracy(sLA)
- trueDuration() : ::types::Real
Informal: Calculates the true duration of the service request.
Evaluates to:
request.processing.response.date.inMs() +
request.date.inMs()
- isDurationAccurate(sLA : ::slang::es::ElectronicServiceSLA) : ::types::Boolean
Informal: Assesses whether the duration measurement is accurate
according to the parameter sLA.
Evaluates to:
if outcome = Outcome.SUCCEEDED
then
not request.processing.oclIsUndefined()
and
not request.processing.response.oclIsUndefined()
and
duration.inMs() >=
trueDuration() - durationAccuracy(sLA)
and
duration.inMs() <=
trueDuration() + durationAccuracy(sLA)
else
duration.oclIsUndefined()
endif
- getMeasurementCount(sLA : ::slang::SLA) : ::types::Integer
Informal: Reports that ServiceUsageRecords contribute 2
measurements to accounts for ElectronicServiceSLAs.
Evaluates to:
if sLA.oclIsTypeOf(::slang::es::ElectronicServiceSLA)
then 2
else 0
endif
- getAccurateMeasurementCount(sLA : ::slang::SLA) : ::types::Integer
Informal: Reports the number of accurate measurements included
if the sLA is an ElectronicServiceSLA
Evaluates to:
if sLA.oclIsTypeOf(::slang::es::ElectronicServiceSLA)
then
let
dateAcc = isDateAccurate(
sLA.oclAsType(
::slang::es::ElectronicServiceSLA)),
durAcc = isDurationAccurate(
sLA.oclAsType(
::slang::es::ElectronicServiceSLA))
in
if dateAcc
then
if durAcc
then 2
else 1
endif
else
if durAcc
then 1
else 0
endif
endif
else 0
endif
Invariants:
-
Wellformedness:
This invariant establishes the responsibilities of the parties
with respect to reporting on service usages.
Nothing requires parties to report failure outcomes
honestly in this specification (because to do so would require
a model of the correct operation of any system, which is not
feasible). Parties should undertake to report failures
honestly in the reconciliation procedures specified in the
SLA, as well as agreeing to a procedure for resolving
disputes concerning the behaviour of the system. Honest
reporting of outcomes can be weakly protected, assuming that
both parties can determine failures with a negligible degree
of error.
If a both a data access error and a failure occur
then nothing requires either party to prefer to report
one outcome in preference to another. Parties should address
this in their reconciliation procedures.
if request.processing.oclIsUndefined() or
request.processing.response.oclIsUndefined()
then
outcome = Outcome."NO_RESPONSE"
else
if outcome = Outcome."OBVIOUS_FAILURE"
then
(not failureType.oclIsUndefined())
else
failureType.oclIsUndefined()
and
failedDataModes()->size() > 0
implies
(
outcome = Outcome."DATA_ACCESS_ERROR"
and
dataFailureModes = failedDataModes()
)
and
outcome = Outcome."DATA_ACCESS_ERROR"
implies
failedDataModes()->size() > 0
endif
endif
-
Wellformedness: The operation definition referenced should
define the operation upon which the request was made.
operation.operation = request.operation
-
Wellformedness: The state definitions references should
define the states in which the system context resided at the
time of the request.
states.state->asSet() =
request.operation.electronicService.context.
getCurrentStatesAt(request.date.inMs())
Definitive: Parameter records are records of the value of a
service request or response parameter, and form part of
a service usage record.
Properties:
Operations:
Invariants:
Extends: ::services::Report
Definitive: A bug report is a report submitted by either
the client to the service provider or vice versa, indicating that
a bug is making the service unavailable to some extent.
Properties:
Operations:
Invariants:
Extends: ::services::Report
Definitive: A bug-fix report is submitted by the service provider
to the client to indicate that a bug that was causing some
kind of service unavailability has been fixed.
Properties:
Operations:
Invariants:
Extends: ::services::es::BugFixReport
Definitive: A data loss report is a special type of bug-fix
report submitted by the service provider to the client, stating
that in the course of fixing the service, some data was lost.
Properties:
Operations:
Invariants:
|
