Information Technology Reference
In-Depth Information
a)
b)
Machine
Impl.
Idle
Idle
y>=2
y = 0
y==6
y <= 6
coin?
tea!
coin?
tea!
y=0
y=0
cof!
Serving
tea!
cof!
Serving
y>=4
y==5
y<=6
y<=5
coin?
coin?
cof
tea
cof
tea
coin
coin
Fig. 1.
a)Specificationofacoffeeandtea
Machine
andb)animplementation
Definition 5.
Let
A
S
and
A
T
betwospecificationautomataand
S
=(
St
S
,s
0
,Σ,
→
S
)
and
T
=(
St
T
,t
0
,Σ,
→
T
)
betheircorrespondingtimedtransitionsystems.We
saythat
A
S
refines
A
T
,written
A
S
≤
A
T
,iffthereexistsabinaryrelation
R
⊆
St
S
×
St
T
containing
(
s
0
,t
0
)
andforallstates
sRt
implies:
T
t
for some
t
∈
St
T
then
s
i
−−→
S
s
and
s
Rt
for some
s
∈
St
S
1. whenever
t
i
−−→
S
s
forsome
s
∈
St
S
then
t
o
−−→
T
t
and
s
Rt
forsome
t
∈
St
T
2. whenever
s
o
−−→
3. whenever
s
−→
S
s
for
d
∈
R
≥
0
then
t
−→
T
t
and
s
Rt
for some
t
∈
St
T
It is easy to see that the refinement is reflexive and transitive, so it is a pre-
orderonthesetofallspecifications.Refinementcanbecheckedforspecification
automata by reducing the problem to a specific refinement game, and using a
symbolicrepresentationtoreasonaboutit.SeeSection5formoredetails.
Satisfaction
isasimpleapplicationofrefinement.Moreprecisely,wesaythat
animplementationsatisfiesaspecificationautomatoniffitrefinesthisspecifica-
tion.Asanexample,observethattheautomatoninFigure1bisarefinementof
theoneinFigure1a,andthusitisalsoanimplementationofit.
Thesetofallimplementationsof
A
isdenoted
[[
A
]]
mod
.In[12],wehaveshown
that the refinement relation is complete for our specification model, i.e,
A
S
refines
A
T
iffthesetofimplementationsthatsatisfy
A
S
isincludedinthesetof
implementationsthatsatisfy
A
T
.
A specification may be
locally inconsistent
in the sense that it may contain
bad states
, i.e., states that do not satisfy the
independent progress
property
2
.
We say that a specification is
consistent
, and thus useful, if it admits at least
one implementation. It is important to have a procedure to decide whether a
specificationadmitsatleastoneimplementation.In[12],wehaveshownthatthis
questionreducestotheoneofdecidingifthereexistsastrategyforthesystem
(Output player) to avoid reaching
bad states
in the specification. A
pruning
facilityremovesfromtheTIOAallthebehavioursthatarenotcoveredbythe
strategy.Itcandrasticallyreducethestate-spaceoftheautomaton.Intherest
ofthepaper,weassumethatbadstatesarealwaysprunedaway.
2
Insection4,weshallobservethatthecombinationoftwospecificationswithoutbad
statesmayleadtoaspecificationwithbadstates.
