June 10th, 2010      Amsterdam, Netherlands (satellite of DisCoTec 2010) organised with Artist partners 


ICE 2010 programme

Slot Duration Talk
09:00 – 09:05 (00:05) Opening
09:05 – 10:05 (01:00) From Boolean to Quantitative Theories of Reactive Systems.
Thomas A. Henzinger (invited talk)
10:05 – 10:30 (00:25) Port Protocols for Deadlock-Freedom of Component-Based Systems.
Christian Lambertz and Mila Majster-Cederbaum
10:30 – 11:00 (00:30) Coffee break
11:00 – 11:30 (00:30) A Graphical Approach to Progress for Structured Communication in Web Services.
Marco Carbone and Søren Debois
11:30 – 12:00 (00:30) History-sensitive versus future-sensitive approaches to security in distributed systems.
Alejandro Hernandez and Flemming Nielson
12:00 – 12:25 (00:25) Safer in the Clouds.
Chiara Bodei, Gian Luigi Ferrari and Viet Dung Dinh
12:25 – 14:00 (01:35) Lunch
14:00 – 15:00 (01:00) Concurrency, Interaction, Abstraction and Randomness.
Joost-Pieter Katoen (invited talk)
15:00 – 15:30 (00:30) Static vs dynamic SAGAs.
Ivan Lanese
15:30 – 16:00 (00:30) Coffee break
16:00 – 16:30 (00:30) Primitives for Contract-based Synchronization.
Massimo Bartoletti and Roberto Zunino
16:30 – 17:00 (00:30) An Introduction to Time-Constrained Automata.
Matthieu Lemerre, Vincent David, Christophe Aussaguès and Guy Vidal-Naquet
17:00 – 17:30 (00:30) A theory of desynchronisable closed loop systems.
Harsh Beohar and Pieter Cuijpers
17:30 – 17:55 (00:25) A linear programming approach to general dataflow process network verification and dimensioning.
Renaud Sirdey and Pascal Aubry
17:55 – 18:10 (00:15) Closing
20:00 Social Event

Invited talks

  • Thomas A. Henzinger (IST, Austria) "From Boolean to Quantitative Theories of Reactive Systems"
    Abstract: The traditional view holds that there is a boolean satisfaction or refinement relation between system implementations and system specifications. Reactive models have been extended to accommodate certain numerical quantities, such as transition times and probabilities. However, the boolean view is still prevalent, for example, in checking whether a timed automaton satisfies a formula of a real-time logic, or whether a stochastic process satisfies a formula of a probabilistic logic. We advocate the fully quantitative view, where a specification can be satisfied to different degrees, that is, the value of a given specification over a given implementation is a real number rather than a boolean. We survey some results in this direction and present some potential applications, not only in the timed and probabilistic domains, but also for specifying and analyzing the resource use, cost, performance, robustness, and reliability of a system.
  • Joost-Pieter Katoen (RWTH Aachen University, Germany) "Concurrency, Interaction, Abstraction and Randomness"
    Abstract: We consider a stochastic model which allows interaction and concurrency in a CSP-like fashion. We discuss notions of (bi)simulation, congruence results, and compositional abstraction. Analysis is carried out using a model-checking procedure. Finally, we sketch how the model can be used as semantical backbone for higher-level formalisms such as generalized stochastic Petri nets or the architecture description language AADL.

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet