


LieuLIP6: comment y aller Programme14h0015h00: Giuseppe Lipari, Scuola Superiore Sant'Anna, Pisa, Italy "Componentbased analysis of realtime systems"Abstract: The complexity of modern embedded realtime systems is constantly increasing, as new and more complex functionality is added to existing software. At the same time, due to the increasing computational power of the hardware platforms and to the pressure to reduce the costs, software that in the past was run on different computational nodes, is now being integrated onto a single node. An appealing way to reduce complexity is to apply a componentbased realtime design methodology. A realtime system can be seen as a set of interacting components, each one providing a welldefined subset of functionalities, whose integration produces the final system behavior. A componentbased methodology is successful only if it can effectively reduce the complexity. To achieve this goal, the system designer must be able to 1) analyze and validate each component in isolation from the rest of the system, 2) summarize its properties and requirements into simpler interfaces, 3) perform the final integration analysis and validation on the component interfaces. In this talk, the author will give an overview of current techniques for componentbased analysis of realtime systems, with a look at their possible use in avionics and automotive systems. Then, a possible research agenda will be discussed, highlighting the shortcomings of current analysis and how to improve on it. 15h0015h30 : Ala Eddine Ben Salem, LIP6/LRDE "Model Checking using Generalized Testing Automata"Abstract: Geldenhuys and Hansen showed that a kind of omegaautomata known as Testing Automata (TA) can, in the case of stutteringinsensitive properties, out perform the Büchi automata traditionally used in the automatatheoretic approach to model checking. In previous work, we compared TA against Transitionbased Generalized Büchi Automata (TGBA), and concluded that TA were more interesting when counterexamples were expected, otherwise TGBA were more efficient. In this work we introduce a new kind of automata, dubbed Transitionbased Gen eralized Testing Automata (TGTA), that combine ideas from TA and TGBA. Implementation and experimentation of TGTA show that they outperform other ap proaches in most of the cases.. 15h3016h00: pause café16h0016h30: vie du groupe 
