Information Technology Reference
In-Depth Information
UniSpec
Machine
HalfAdm1
HalfAdm2
Researcher
pub?
patent!
grant?
coin!
u<=2
Idle
y>=2
tea?
grant?
u=0
Stuck
grant?
End
Grant
A
C
Idle
u>2
Start
x>15
tea?
u<=20
grant?
cof?
grant?
coin?
tea!
u=0
patent!
y=0
coin!
grant?
patent!
pub?
x>=2
patent!
cof!
Serving
tea!
x=0
y=0
x<=15
x=0
pub!
pub!
y>=4
cof?
tea?
y<=6
patent!
B
coin!
D
coin?
x=0
x=0
pub!
x<=2
y<=2
x=0
Coffee
Tea
x>=4
pub?
pub?
x<=4
x<=8
grant?
grant?
&&
yes/no+strategy
||
≤
combinewithoperator
Fig. 10.
Illustration of thesteps performed in a concrete refinementcheck. The grey
boxrepresentsthepartcarriedoutinternallybytheverificationengine.
Finally, we illustrate the advantageof being capable to model check TCTL
propertiesonTIOAs.Wewouldliketoavoidconsideringzenobehaviours.The
idea isto combineourspecificationwith anobserverandthen makesurethat
theobservervisitsinfinitelyoftenastateinwhichtimeadvances.Thelattercan
bespecifiedwithaTCTLproperty.Theobserver
Obs
hastwostates
reset
and
advance
and a witness clock
w
. The observerissues a non shared output from
reset
to
advance
if
w
>
1
. Then it directly moves back to
reset
and resets the
clock. The observer is then composed with the specification. There will be no
synchronisationbetweentheobserverandthespecification.Nonzenobehaviours
inthecompositionarethosewhere
Obs
visitsthestate
advance
infinitelyoften.
We use the following property that checks for refinement with an additional
B¨uchiconditionconstrainingthecomposition.
refinement: (Researcher || Administration2 || Machine || Obs
: A[] A<> Obs.advance) <= UniSpec.
6 Related Work
Inthissection,wecompareourresultswithothertimedinterfacetheories.
Input/Outputautomatamodel
Therehavebeenseveralotherattempts to pro-
poseaninterfacetheoryfortimedsystems(see [14,16,13,7,6,10,35,17,27]for
some examples). Our model shall definitely be viewed as an extension of the
timedinput/outputautomatonmodelproposedbyLynchetal.[21].Themajor
differencesareinthegame-basedtreatmentofinteractionsandtheadditionof
quotientandconjunctionoperators.
Timed Interfaces by de Alfaro et al.
In [16], de Alfaro et al. proposed
timed
interfaces
,atimedextensionoftheinterfacemodeltheyintroducedin[14].Like
forspecificationautomata,thesyntaxofatimedinterfaceissimilartotheone
of a
timed input/output automaton
[22] and the semantic is given by a timed
