Scientific Program 
Scientific Program Scientific Program
Scientific Program Scientific Program
Wednesday December 12
11h – 12h Registration
12h Lunch
13h45 – 14h Welcome
14h – 15h Invited talk "Avionic Software Verification by Abstract Interpretation".
By Patrick COUSOT. LIENS - Ecole Normale Supérieure de Paris- Paris, France.
15h – 15h30 Break
15h30 – 17h30 Session 1. Scheduling
“New worst-case analysis technique for real-time transactions”
By Ahmed Rahni, Emmanuel Grolleau and Michaël Richard - LISI/ENSMA, Futuroscope , France .
“A C-space sensitivity analysis of Earliest Deadline First scheduling”
By Jean-François Hermant - ECE, LACSC, Paris, France - and Laurent George - University of Paris 12, France.
“Functionally Deterministic Scheduling”
By Frédéric Boniol - IRIT-ENSEEIHT, Toulouse , France -, Claire Pagetti, and François Revest - ONERA-CERT, Toulouse , France .
“Reliable and Precise WCET and Stack Size Determination for a Real-life Embedded Application”
By Philippe Baufreton - Hispano-Suiza, Etablissement de Réau, Moissy-Cramayel, France - and Reinhold Heckmann – AbsInt Angewandte Informatik GmbH, Saarbrücken, Germany.
17h30 Social event
Thursday December 13
8h30 – 9h30 Invited talk. “ Model-based development of embedded control systems: historical perspective and recent advances”
By Paul CASPI. Former researcher Verimag-Grenoble , France .
9h30 – 10h30 Session 2. Performance Analysis
“Formal models of Fractal Component Based Systems for performance analysis”
By Nabila Salmi, Patrice Moreaux - Université de Savoie, France -, and Malika Ioualalen - USTHB, Algiers, Algeria.
“Fault-Tolerance Analysis of Mixed CAN/Switched Ethernet Architecture”
By Claudia Betous-Almeida, Jean-Luc Scharbarg, and Christian Fraboul - IRIT-ENSEEIHT- University of Toulouse, France.
10h30 – 11h BREAK
11h – 12h30 Session 3. Model Checking
“Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more”
By Michael Leuschel and Daniel Plagge - Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, Germany .
“Verification, Diagnosis and Adaptation: Tool supported enhancement of the model-driven verification process”
By Marco Bakera, Tiziana Margaria, Clemens D. Renner - University of Potsdam , Germany -, and Bernhard Steffen - University of Dortmund , Germany .
“Verification of embbeded systems with preemption: a negative result”
By Jérôme Ermont and Frédéric Boniol - IRIT-ENSEEIHT - University of Toulouse , France .
12h30 – 14h Lunch
14h – 15h Invited talk “ The aeronautical systems development challenges for Airbus”
By Odile LAURENT . Airbus France – Toulouse, France.
15h – 16h Session 4. Formal Modelling
“Using Analogy to Promote Conceptual Modeling Reuse”
By Karin K. Breitman, Simone D.J. Barbosa, Marco A. Casanova, Antonio L. Furtado - Pontifícia Universidade Católica do Rio de Janeiro, Brazil -, Michael G. Hinchey - Loyola College, Baltimore, USA.
“Formal Modeling of Data. A Case Study for Space Applications”
By Jean-Paul BLANQUART – Astrium Satellites, Toulouse, France - Gérard Bulsa – ESTEC Keperlaan, Noordwijk, Netherlands -, David Lesens – Astrium Space Transportation, Les mureaux, France -, George Mamais – Semantix Information Technologies, Athens, Greece - and Maxime Perrotin – ESTEC Keperlaan, Noordwijk, Netherlands.
16h – 16h30 Break
16h30 – 18h Session 5. Refinement / Abstraction Methods
“Don't care in SMT-Building flexible yet efficient abstraction/refinement solvers”
By Andreas Bauer - Canberra Research Laboratory, Australia - , Martin Leucker, Christian Schallhart, and Michael Tautschnig - Technische Universität München, Germany.
“Qualitative Abstraction based Verification for Analog Circuits”
By Mohamed H. Zaki, Sofiène Tahar - Concordia University, Montréal Canada - and Guy Bois - Ecole Polytechnique de Montreal, Canada.
“Preservation of timed properties during an incremental development by components”
By Jacques Julliand, Hassan Mountassir, and Emilie Oudot - Université de Franche-Comté, France.
19h30 Social event
Friday December 14
8h30 – 9h30 Invited talk “ Development of Transportation Systems”
By Dines BJORNER. Technical University of Denmark - Lingby , DENMARK .
9h30 – 10h30 Session 6. Real Time
“OASIS formal approach for distributed safety-critical real-time system design”
By Jean-Sylvain Camier, Damien Chabrol, Vincent David, and Christophe Aussaguès – CEA, GIF SUR YVETTE, France.
“Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method”
By Joris Rehm - Université Henri Poincaré Nancy 1, France - and Dominique Cansell - LORIA, France.
10h30 – 11h Break
11h – 12h30 Session 7. Testing
“A Simplified Approach for Testing Real-Time Systems Based on Action Refinement”
By Saddek Bensalem, Moez Krichen - Verimag Laboratory, Gières, France -, Lotfi Majdoub, Riadh Robbana - LIP2 Laboratory and Polytechnic School of Tunisia, Tunisia - and Stavros Tripakis - Verimag Laboratory and Cadence Berkeley Labs, USA.
“Using Formal Methods to increase confidence in one Home Network System implementation. Case study”
By Lydie du Bousquet - Universités de Grenoble, France -, Masahide Nakamura - Kobe University, Japan -, Ben Yan - Nara Institute of Science and Technology, Japan - and Hiroshi Igaki - Kobe University, Japan.
“Using Invariant Detection Mechanism in Black Box Inference”
By Muzammil Shahbaz - France Telecom R&D, Meylan , France - and Roland Groz - Grenoble Universités , France .
Closing.
12h30 Lunch