Information Technology Reference
In-Depth Information
game. However, unlike specification automata, timed interfaces are not forced
to be deterministic or input-enabled. The absence of input-enabledness allows
for defined error states in the composition where one component can issue an
outputthatcannotbecapturedbytheothercomponent.Twotimedinterfaces
are said to be compatible if there exists an environment in which they can
worktogetherwhileavoidingsucherrorstates.Thisdefinitionofcompatibility
allowstocapturethetimingbetweeninterfaces:“whatarethetemporalordering
constraintsoncommunicationeventsbetweencomponents?”.Unfortunately,the
work in [16] is incomplete. Indeed there is no notion of implementation and
refinement.Moreover,conjunctionandquotientarenotstudied.Also,deAlfaro
et al. did not consider more elaborated error states specified by the user with
some timed temporal logic. Finally, the theory has only been implemented in
a prototype tool called TICC[13], which does not handle continuous time. A
main drawbackof TICC is its textual input languagethat is far from modern
graphicalspecificationlanguagesusedbyengineers.
TimedModal Specifications
In[23]Larsenproposes
modal automata
,whichare
deterministicautomataequippedwithtransitionsofthefollowingtwotypes:
may
and
must
.Thecomponentsthat implement suchinterfacesaresimple labelled
transitionsystems.Roughly,a musttransitionisavailableineverycomponent
that implements the modal specification, while a may transition need not be.
Recently[7,6] a timed extension of
modal
automata was proposed, which em-
bedsalltheoperationspresentedinthepresentpaper.However,modalitiesare
orthogonal to inputs and outputs, and it is well-known [24] that, contrary to
the game-semantic approach, they cannot be used to distinguish between the
behavioursofthecomponentandthoseoftheenvironment.Asidefromtheor-
thogonality between input/output and may/must modalities. Our model does
notallowtocombine/compareautomatathatsharecommonclocknames,while
in[7,6]theyrestrictthemselvestoeven-clockautomata[2]fordoingso.Weare
convincedthatourtheorydirectlyextendsto anevent-clockautomataversion
ofTIOAwith sharedclocks.Finally, ourworkisimplemented, while thework
in [7,6]isnotimplemented.
7Con lu on
Wehaveproposedacompletegame-basedspecificationtheoryforrealtimesys-
tems, in which we distinguish between a component and the environment in
which it is used. To the best of our knowledge, our contribution is the first
game-basedapproachtosupportbothrefinement,consistencychecking,logical
and structural composition, and quotient. Our results have been implemented
inthe
toolfamily[3].
In the future one could extend our model with global variables. This was
alreadysuggestedbyBerendsenand Vaandragerin [5],but onlyforstructural
compositionandrefinementandwithoutthegame-basedsemantic.
One could also investigate whether our approach can be used to perform
scheduling of timed systems (see [13,19,17] for examples). For example, the
Uppaal
