Institute of Computer Languages
Compilers and Languages Group
über
| Datum: | Dienstag, 7. September 2010 |
|---|---|
| Zeit: | 10:00 s.t. |
| Ort: | TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte) |
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) equivalences, 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.
(joint work with Ernst-Rüdiger Olderog)
Mani Swaminathan holds a Master's degree in Telecommunications from
the Indian Institute of Technology, Delhi. From 2000 to 2005 he has
held positions in industry and academia in India and Switzerland,
including General Electric Global Research and the Ecole Polytechniqe
Fédérale de Lausanne. Later on he was a PhD student in the
Graduiertenkolleg Trustsoft at the University of Oldenburg, and a
consultant in avionics and aerospace at Altran Deutschland. Since 2008,
Mani is a research assistant within DFG funded
Sonderforschungsbereich AVACS (Automatic Verification and Analysis of
Complex Systems).
(http://csd.informatik.uni-oldenburg.de/persons/mani.swaminathan/)
Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.