Information Technology Reference
In-Depth Information
WenowdefineimplementationsandspecificationsintermsofTIOAs.
Definition 3.
A specification automaton is a TIOAthat is input-enabled, i.e.,
ineachstatealltheinputsshouldbeavailable.
The assumption of input-enabledness, also seen in many interface theories[28,
18,34,37,32], reflects our belief that an input cannot be prevented from be-
ing sent to a system, but it might be unpredictable how the system behaves
after receiving it. Input-enabledness encourages explicit modelling of this un-
predictability,andcompositionalreasoningaboutit;forexample,decidingifan
unpredictablebehaviourofonecomponentinducesunpredictabilityoftheentire
system. Observethat it is easy to check whether a TIOA is input-enabled. In
practicetools caninterpret absentinput transitionsin at least two reasonable
ways.First,theycanbeinterpretedasignoredinputs,correspondingtolocation
loops in the automaton. Second, they may be seen as unavailable ('blocking')
inputs,whichcanbeachievedbyassumingimplicittransitionstoadesignated
errorstate.Later,inSection4.2wewillcallsuchastate
strictlyundesirable
and
givearationaleforthisname.
The role of specifications in a specification theory is to abstract, or under-
specify, sets of possible implementations.
Implementations
are concrete exe-
cutablerealizationsofsystems.Wewillassumethatimplementationsoftimed
systems have fixed timing behaviour (outputs occur at predictable times) and
systemscanalwaysadvanceeitherbyproducinganoutputordelaying.Formally:
Definition 4.
An implementation is a specification that satisfies the two
following conditions:
1.
Independent progress:
implementationscannotgetstuckinastatewhere
itisuptotheenvironmenttoinduceprogress.Ineachimplementationstate
eitheranoutputispossible oronecandelayuntilanoutputisenabled.
2.
Output urgency:
ifanoutputisavailable, thenitcannotbedelayed.
Since specifications and implementations are TIOAs, their semantics are still
givenintermsofTIOTs.Werefertheinterestedreaderto[12]formoredetails.
Example.
Figure1aspecifiesavendingmachinethatcanserveteaorcoffee.A
possible implementation of this machine can be found in Figure 1b. Both au-
tomataaredeterministic.Notethattheoutputtransitionsoftheimplementation
Impl
arriveatafixedmomentintimeandcannotbedelayed,whichguarantees
outputurgency(theinvariantguaranteesprogressandtheguardconstrainsthe
transition). Each time the output
tea!
from
Idle
to
Idle
is taken, the clock
y
isreset.Withoutthis reset,independent progresswouldnotbeguaranteedfor
valuationsoftheclock
y
thataregreaterthan
6
.
We now introduce
refinement
—a notion of comparison between two specifica-
tionsandawaytorelateimplementationstospecifications.Refinementshould
satisfythefollowing
substitutability
condition.If
A
S
refines
A
T
,itshouldbepos-
sibletoreplace
A
T
with
A
S
ineverycontextandobtainanequivalentsystem.
Contrarytotheotheroperations,refinementisdefinedatthelevelofTIOTSs.
