Journées FAC 2012

Mercredi 4 avril (matin)

Accueil Café à partir de 9h00
9h15 Ouverture des journées

Conférencier invité

9h30-10h30 • Hume: a functionally-based Domain Specific Language Targeting real-time Embedded Systems
Kevin Hammond The University of St Andrews

10h30-11h00 Pause

Techniques de verification

11h00-11h30 • A Generic Ellipsoid Abstract Domain for Linear Time Invariant Systems
P. Roux, R. Jobredeaux, P.-L. Garoche, E. Feron ONERA GEORGIA [papier]

11h30-12h00 • Formal compatibility of experimental frame concept and finite and deterministic devs model
D. Foures, V. Albert, A. Nkesta LAAS [papier]

12h00-12h30 • Parallel Model Checking With Lazy Cycle Detection - MCLCD
R. T. Saad, S. Dal Zilio, B. Berthomieu LAAS [papier]

13h00 Repas à l’UPSIDUM

Mercredi 4 avril (après-midi)

Logique et Vérification

14h30-15h00 • Non preemptive static priority in network calculus: accuracy and integration with P-GPS
William Mangoua Sofack, Marc Boyer ONERA [papier]

15h00-15h30 • A Lemma Generator Powered by Quantifier Elimination and Hull Computation
A. Champion, R.Delmas, M. Dierkes ONERA ROCKWELL [papier]

15h30-16H00 • Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
A. Schimpf, S. Merz, J.-G. Smaus U. Freiburg, LORIA, IRIT [papier]

16h00-16h30 Pause

Architecture

16h30-17h00 • Nets-within-nets to model innovative space system architectures
F. Cristini, C. Tessier ONERA [papier]

17h00-17h30 • Un Point de Vue Sûreté de Fonctionnement pour la Vérification d’Architectures Abstraites
M. Piriquito, P. Bieber, J. Brunel, D. Chemouil ONERA [papier]

17h30-18h00 • Use of modelling methods and tools in an industrial embedded system project: works and feedback
A. Fernandes Pires, S. Duprat, T. Faure, C. Besseyre, J. Beringuier, J.-F. Rolland ATOS AIRBUS [papier]

Jeudi 5 avril (matin)

Conférencier invité

9h-10h • Sémantique non-standard de systemes hybrides et applications à la compilation d’un langage hybride
Benoît Caillaud IRISA

10h00-10h30 Pause

Compilation

10h30-11h00 • Model-Driven Engineering Approach For SysML Activity Diagram Simulation
D. Foures, V. Albert, J.-C. Pascal, A. Nketsa LAAS [papier]

11h00-11h30 • Specification and Validation of Model Transformations for Certified Systems Development
A. Toom, A. Dieumegard, M. Pantel IRIT Tallinn University [papier]

11h30-12h00 • Formally verified optimizing compilation in ACG-based flight control software
R. Bedin Franca, S. Blazy, D. Favre-Felix, X. Leroy, M. Pantel, J. Souyris AIRBUS, INRIA, IRISA, IRIT [papier]

12h00-12h30 • Resource Sharing Conflicts Checking in Multithreaded Java Programs
N. Baklanova, L. Féraud, M. Strecker IRIT [papier]

13h00 Repas à l’UPSIDUM

Jeudi 5 avril (après-midi)

Langages

14h30-15h00 • Vers une sémantique des jeux pour un langage d’ingénierie des exigences par buts et agents
C. Chareton, J. Brunel, D. Chemouil ONERA [papier]

15h00-15h30 • Calcul de latences dans un programme Prelude
Rémy Wyss, Frédéric Boniol, Julien Forget, Claire Pagetti ONERA LIFL IRIT [papier]

15h45-16h15 Pause

Spécifications temps réel

16h15-16h45 • Model-Checking Observers for a Real-Time Pattern Language
N. Abid , S. Dal Zilio , D. Le Botlan LAAS [papier]

16h45-17h15 • Time Properties Dedicated Semantics for UML-MARTE Safety Critical Real-Time System Verification
N. Ge, M. Pantel IRIT [papier]

This document was translated from L^AT_EX by H^EV^EA.