Information Technology Reference
In-Depth Information
Act
i
\
Act
o
∪
Act
i
\
Act
o
and
Act
o
=
Act
o
∪
Act
o
.Thesetofedges
E
isdefined
bythefollowingrules:
1. If
(
q
S
,a,ϕ
S
,c
S
,q
S
)
∈
E
S
with
a
∈
Act
S
\
Act
T
thenforeach
q
T
∈
Loc
T
this
gives
((
q
S
,q
T
)
,a,ϕ
S
,c
S
,
(
q
S
,q
T
))
∈
E
2. If
(
q
T
,a,ϕ
T
,c
T
,q
T
)
∈
E
T
with
a
∈
Act
T
\
Act
S
thenforeach
q
S
∈
Loc
S
this
gives
((
q
S
,q
T
)
,a,ϕ
S
,c
S
,
(
q
S
,q
T
))
∈
E
3. If
(
q
S
,a,ϕ
S
,c
S
,q
S
)
∈
E
S
and
(
q
T
,a,ϕ
T
,c
T
,q
T
)
∈
E
T
with
a
∈
Act
S
∩
Act
T
c
T
,
(
q
S
,q
T
))
∈
thisgivesriseto
((
q
S
,q
T
)
,a,ϕ
S
∧
ϕ
T
,c
S
∪
E
.
Thefirstrulerepresentallthecaseswhere
A
S
makesanindividualmove,beit
inputoroutput,because
a
isnotinthesignatureof
A
T
.Similarlythesecondrule
handlesallindividualmovesbythesecondcomponent
A
T
.Thethirdrulehandles
allsynchronisationsbetweenthetwocomponents,nomatterthecombinationof
input and/or output. The rule is so simple because the type of the resulting
transitionisgivenbythesets
Act
i
and
Act
o
.Thenewoutputset,
Act
o
,isjusta
simpleunionoftheoutputs,whiletheinputset,
Act
i
,isalltheinputsthatare
notoutputsoftheothercomponent.
Observe that if we compose two locally-consistent specifications using the
aboveproductrules,thentheresultingproductisalsolocallyconsistent.More-
over, unlike [16], our specifications are input-enabled, and there is no way to
defineanerrorstateinwhichacomponentcanissueanoutputthatcannotbe
capturedbytheothercomponent.Theabsenceof“model-related”errorstates
allowsusto define moreelaboratederrorsspecifiedbythedesigner[12].Asan
example,atemporalpropertywritteninsomelogicsuchasTCTL
∗
canbein-
terpretedoverourspecification,whichwhenanalysedbyamodelchecker,will
resultinpartitioningofthestatesintogoodones(saysatisfyingtheproperty)
andbadones(violatingtheproperty).
Incontrasttoconjunction,parallelcompositionisusedtoreasonaboutexter-
naluseoftwo(ormore)components.Weassumeanindependentimplementation
scenario,wherethetwocomposedcomponentsareimplementedbyindependent
designers.Thedesignerofanyoftheenvironmentcomponentscanonlyassume
thatthecomposedimplementationswilladheretooriginalspecificationsbeing
composed. Consequently if an error occurs in parallel composition of the two
specifications,the
environment
istheonlyentitythatispossiblyina position
toavoidit.Thus,eachcompositionisfollowedbyapruningoperationwhereall
thestatesfromwhichtheenvironmenthasnostrategyto avoidthesetofbad
statesareremoved.
In[12],wehaveshownthefollowingimportantresultsregardingcomposition.
-
Anyimplementation ofcompositioncanbe realizedby implementationsof
composedspecifications:
[[ (
A
S
||
A
T
)]]
mod
=[
A
S
]]
mod
||
[[
A
T
]]
mod
.
-
Thecompositionoperation(alsoifcombinedwithapruning)isassociativeand
commutative,soamongothers:
[[ (
A
S
||
A
U
)]]
mod
.
-
Refinementisaprecongruencewithrespecttoparallelcomposition;forany
specifications
A
S
,
A
T
,and
A
U
suchthat
A
S
≤
A
T
)
||
A
U
]]
mod
=[
A
S
||
(
A
T
||
A
T
and
A
S
composablewith
