Der Arbeitsbereich für Programmiersprachen und Übersetzer am Institut für Computersprachen lädt zu folgendem Vortrag ein:
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 Federale 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).