Information Technology Reference
In-Depth Information
HalfAdm1
HalfAdm2
grant?
coin!
pub?
patent!
a)
b)
C
A
patent!
pub?
coin!
grant?
y=0
x=0
coin!
D
patent!
B
x<=2
y<=2
pub?
pub?
grant?
grant?
grant
patent
pub
coin
grant
patent
pub
coin
Fig. 7.
Exampleoftwoconjuncts,eachhandlingoneaspect,thatmakeupadifferent
modeloftheAdministrationcomponent
ofthe
Administration
component.Figure7adescribesanalternationbetweenthe
coin!
and
grant?
whileFigure7bdescribesthealternationbetween
patent!
and
pub?
.Togethertheseformanalternativeandslightlymoreloosespecificationof
theadministration.It is thecasethatboth
Administration
and
Administration2
refinetheconjunction
HalfAdm1
∧
HalfAdm2
,whiletheoppositeisnotthecase.
Finally the tool is able to verify TCTL
∗
[1] propertieson the specifications.
This feature is made possible thanks to the modified underlying verification
engine.Thiswillbeexemplifiedinsection5.
4 Combining Specification Automata
In this section, we discuss the three main operations defined on specification
automata, namely: conjunction, composition, and quotient. All of these were
usedtosupportdifferentdesignprocessesdescribedintheprevioussection.
Intherestofthesection,wewillconsidertwospecificationautomata
A
S
=
(
Loc
1
,q
0
,
Clk
1
,E
1
,Act
1
,
Inv
1
)
and
A
T
=(
Loc
2
,q
0
,
Clk
2
,E
2
,Act
2
,
Inv
2
)
.Fortech-
nicalreasons,wealsoassumethat
Clk
1
∩
Clk
2
=
∅
.
4.1 Conjunction
Conjunctionallowstotestwhetherseveralspecificationscanbesimultaneously
metbythesamecomponent.Inourframework,conjunctioncanonlybedefined
if
Act
i
=
Act
i
and
Act
o
=
Act
o
. The operation reduces to check whether
the twospecifications can progressin the same way. Formallythe conjunction
of
A
S
and
A
T
, denoted
A
S
∧
A
T
,istheTIOA
A
=(
Loc
,q
0
,
Clk
,E,Act
S
,
Inv
)
Loc
T
,
q
0
=(
q
0
,q
0
)
,
Clk
=
Clk
S
givenby:
Loc
=
Loc
S
×
Clk
T
,
Inv
((
q
S
,q
T
)) =
Inv
(
q
S
)
∧
Inv
(
q
T
)
.Thesetofedges
E
isdefinedbythefollowingrule:
