Information Technology Reference
In-Depth Information
8. Theremustexistaspecificationlanguagetospecifypropertiesofinterfaces
aswellasaproceduretodecidewhethertheinterfacesatisfiestheproperties.
9. All the above operations and properties should be performed and checked
withe
cientalgorithms.
10. User-friendlytools providing comprehensiblefeedback to the user must be
available.Forexample,ifanimplementationviolatesaspecification,auseful
feedbackinspiresthedesigneronhowtocorrectit.
In [16], a timed extension of the theory of interface automata has been intro-
duced,motivatedbythefactthattimecanbeacrucialparameterinpractice,
forexampleinembeddedsystems.Theresultsof[16]focusmostlyonstructural
composition.Recently[12]wehaveproposedwhatseemstobethefirstcomplete
interfacetheoryfortimedsystems(withrespecttotheaboverequirements).Our
specifications are
timed
input/output automata [21]—timed automata whose
setsofdiscretetransitionsaresplitinto
input
and
output
transitions.Contrary
to [16] and [21]our theorydistinguishes between implementations and specifi-
cations.Thisisdonebyassumingthattheformerhavefixedtimingbehaviour
and they can always advance either by producing an output or delaying. The
theoryalsoprovidesagame-basedalgorithmtodecidewhetheraspecificationis
consistent,i.e.whetherithasatleastoneimplementation.Thelatterreducesto
deciding existenceofastrategythat despitethebehaviourofthe environment
willavoidstatesthatcannotpossiblysatisfytheimplementationrequirements.
A
pruning
facilityremovesallthe statesnot coveredbythe strategy.It can
drasticallyreducethestate-spaceofthesystem.Followingasimilarprinciple,it
ispossibletoconstrainaninterfacewithatimedtemporallogicformula[1].For
example,likein[16],onecanuseaB¨uchiobjectivetoremovestatesallowingZeno
behaviours.Ourtheoryisrichinthesensethatitcapturesallthegoodoperations
foracompositionaldesigntheorypresentedabove.Alsoallthealgorithmshave
beenimplemented.Thisimplementation(availableat[36])comesasanextension
oftheUppaal-tiga tool-set[3].Uppaal-tiga isatoolthatimplementsaseries
ofalgorithmsforsolvingtimedgames[9]aswellascheckingtimedtemporallogic
properties.Workingwithin
Uppaal-tiga
allowsustoproposeastate-of-the-art
userinterfaceforverificationtools.
In this paper ourobjectivesare(1) to givemore insightinto design choices
madein [12],(2)toreportonchallengesoftheimplementation,(3)todiscuss
designmethodologiescompatiblewithourtheory,(4)toevaluatetheimplemen-
tation,and(5)tocompareourresultswithotherresultsinthesamefield.
2 Specifications and Implementations
Weshallnowintroduceourcomponentmodel.
Definition 1.
A Timed I/O Transition System (TIOTS) is a quadruple
S
=
(
St
S
,s
0
,Σ
S
,
→
S
)
,whereSt
S
is an infinite set of states,
s
0
∈
St is the initial
state,
Σ
S
=
Σ
i
⊕
Σ
o
isafinitesetofactionspartitionedintoinputs(
Σ
i
)and
outputs (
Σ
o
)and
→
S
:
St
S
×
(
Σ
S
∪
R
≥
0
)
×
St
S
is a transition relation. We
