T4: Timed models
  This tutorial consists of two parts:
Timed Models: From Theory to Implementation
Patricia Bouyer
(LSV-CNRS and ENS of Cachan, France)
Duration: 90 minutes
Many critical applications have explicit timing constraints. For example, behaviours of systems interacting with an environment (e.g. embedded systems) depend on quantitative timing constraints like response times, transmission delays, etc. For representing such timed systems, several timed models have been proposed. Since their introduction by Alur and Dill in the 90s, timed automata are one of the most-studied and most-established models for real-time systems. Numerous works have been devoted to the comprehension of timed automata and the major property of timed automata is probably that reachability is decidable, which implies in particular that it can be used for verification purposes. Based on this nice theoretical result, several model-checkers have been developed (for instance CMC, HyTech, Kronos and Uppaal) and a lot of case studies have been treated. Decidability properties for timed automata are proved based on the construction of the so-called region automaton: it abstracts finitely and in a correct way the behaviours of timed automata. However, in practice, such a construction is not implemented, because it suffers from an enormous combinatorics explosion, but algorithms searching on-the-fly through the automaton are preferred. These algorithms are based on the notion of zones and can be efficiently implemented using data structures like DBMs. Among these algorithms are the forward analysis algorithms that compute all the reachable configurations from the initial configurations. However, the exact forward computation does not always terminate. Abstractions have to be used to avoid this termination problem but one has to be careful when using such abstractions. In this tutorial, we will present basic results on timed automata as well as abstractions and algorithms that are used in practice.
Time in Process Algebra: A Conceptual Overview
Mario Bravetti
(Univ. of Bologna, Italy)
Duration: 90 minutes
It is widely recognized that dealing with time related aspects in process algebra is often crucial for the specification and analysis of complex real systems. Research work in this field has led to a rather huge literature, where several kinds of time have been taken into account: time may be either based on a discrete or continuous domain, time elapsing may be either probabilistically (so-called stochastic-time) or deterministically (so-called real-time) bounded, analysis may be based on model checking, model solving etc. In this tutorial we perform a conceptual dissertation about the treatment of the various kinds of time in transition systems where notions of composition are defined (as e.g. by defining a process algebra). Moreover we show the conceptual relationship between the notion of time considered and the kind of semantics (in the sense of classical process algebra literature) which must be adopted for representing such a notion of time in the composition operators. The presentation of the different kinds of time extensions is formally supported by making use of simple process algebras which extend a common core timed calculus. All together such extensions form a unifying theory for the representation of different kinds of time in process algebras.
Web Maintenance Person.