Information Technology Reference
In-Depth Information
Ourspecificationtheoryhasbeenimplementedasanextensionof Uppaal-
tiga [3],whichisanengineforsolvingtimedgames.Wehavemadetwomajor
modificationstotheoriginalengine.Thefirstmodificationwastoenrichtheinput
languageinordertoallowforthedescriptionofspecifications/implementations
andoperationsbetweenthem;thesecondonewastomodifythetimed-gameal-
gorithmsinordertotakethecompositionalreasoningmethodologyintoaccount.
Modelling Language.
Theinputsyntaxof
Uppaal-tiga
isidenticaltotheone
of
[4,26]-atoolforspecifying,combiningandverifyingpropertiesof
timedautomata.Theuser-friendlyinterfaceof
Uppaal
isdividedintwoparts:
1)the
specificationinterface
whereautomataarespecifiedinagraphicalmanner,
and 2)the
query interface
where one canask verificationquestions. The main
differencebetweentheinputlanguageof Uppaal-tigaandUppaal isthat,due
to the game interpretation, transitionsare typed with controlmodalities. The
specificationinterfaceofourtoolissimilartotheoneof Uppaal-tiga,except
that we decorate transitions with
input
and
output
modalities, which allows
the user to specify timed I/O automata. Like timed automata, interfaces can
communicate via broadcast channels, but global variables are not permitted.
The query interface allows the user to (a) check whether a TIOA is a proper
implementationoraspecification,(b)toapplycompositionoperationsand(c)
tocheckrefinementrelations.Moredetailscanbefoundat[36].
Each time we specify a TIOA, the tool automatically checks whether it is
deterministic and input-enabled. In case of an implementation, the tool also
checkswhether it satisfiesthe output urgencyand independent progressprop-
erties. Also, the tool automatically computes the set of states for which the
specificationisconsistent.Whenthespecificationiscombinedwithanotherone,
thisinformationisusedinordertoavoidinvolvingbadstates.
Uppaal
Timed Interface Operators.
We have implemented the composition, conjunc-
tion, and refinement operators. Quotient is being implemented. These opera-
tors are available from the query interface. We now give details regarding the
modificationswehavemadeontheoriginalversionof
.
Aswehaveseen,theoperationsof
conjunction
,
composition
,and
quotienting
mayproducespecificationswith
bad
states.Suchstatesneedtobeidentifiedand
prunedaway.For doing so,wehaveadaptedthe gamealgorithmimplemented
in
Uppaal-tiga
. The main challenge,in terms of implementation, is that the
originalalgorithmsworkonfixedinputautomata.Inourcasetheautomataare
notknowninadvancesincetheyresultfromthesuccessivepruningoperations.
Theproblemofcheckingwhether
A
S
refines
A
T
reducestotheoneofsolving
a timed game between two players on the graph-product of
A
S
and
A
T
[12].
The first player, or
attacker
, plays outputs on
A
S
and inputs on
A
T
,whereas
the second player, or
defender
, plays inputs on
A
S
and outputs on
A
T
.One
can show that Refinement does not hold if and only if the attacker can put
thedefenderinabadstate.Therearetwokindsofbadstatesinthisgame:1)
the attacker may delay and violates invariants on
A
T
, which is, the defender
cannotmatchadelay,and2)thedefenderhastoplayagivenactionandcannot
Uppaal-tiga