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
Search WWH ::




Custom Search