Layered Composition of Data-Enriched Real-Time Systems

  We investigate techniques that aim at easier verification
of data-enriched real-time systems, modelled as networks of extended
timed automata (ETA). To this end, we first introduce a syntactic
notion of independence and an operator for layered composition of ETA.
Under certain independence conditions, the Communication Closed Layer
(CCL) laws are shown to hold.

Next, we introduce input/output (i/o) and partial-order (po) equiva-
lences, and show that they are preserved when the layered composition operator is replaced by sequential composition within the CCL laws.
We then introduce time precedence as a semantic condition that
preserves the validity of the CCL laws even under violation of the
syntactic independence conditions, but with the ETA now restricted
to acyclic models.

Finally, we show that both the independence and the time precedence
conditions may be exploited for easier verification of networks of
ETA, and illustrate a realistic example for each approach. For the former (independence), we consider a collision avoidance protocol
developed for an audio/video system of Bang and Olufsen, while the
usage of time precedence is illustrated by considering Fischer's
protocol for mutual exclusion.

(This is joint work with Ernst-Rüdiger Olderog).