JSLC 2001

Plan

Présentation

Buts et moyens

JSLC 2000

JSLC 2001

Projets-pilote

Club des Partenaires

Nous contacter

Liens

Mardi 6 : Sécurité des systèmes - Tuesday 6^th : System security

Journée animée par Yassine Lakhnech, Professeur, Université de Joseph Fourier

09 h 30 - 10 h 45    Daniel Le Metayer (Trusted Logic) :  "TL-FIT, un environnement d'aide à la conception et à l'évaluation de produits dans le cadre des Critères Communs de Sécurité"

10 h 45 - 11 h 15     Pause

11 h 15 - 12 h 30     Gilles Barthe (INRIA Sophia Antipolis) : "Tool-Assisted Reasoning about JavaCard"

12 h 30 - 14 h 00     Déjeuner

14 h 00 - 15 h 15     Michaël Rusinowitch (INRIA Lorraine) : "Vérification automatique de protocoles cryptographiques avec CASRUL"

15 h 15 - 16 h 30     Silvano Dal-Zilio (CNRS Marseille) : "Calcul de Processus Mobiles"

16 h 30 - 17 h 00     Pause

17 h 00 - 18 h 15     Didier Begay (France Telecom R&D) : "Les méthodes formelles à France Télélecom R&D"

Mercredi 7 : Perspectives in System Development - Wednesday 7^th

Journée animée par Joseph Sifakis, Directeur de Recherche, CNRS

09 h 00 - 10 h 15     John Rushby (SRI International) : "Formal verification for the Time Triggered Architecture"

10 h 15 - 10 h 45     Pause

10 h 45 - 12 h 00     David Harel (Weizmann Institute) : "Capturing and Executing Behavioral Requirements: The Play-In/Play-Out Approach"
                                 contact: David Harel <harel@wisdom.weizmann.ac.il>
 

12 h 00 - 13 h 30     Déjeuner

13 h 30 - 14 h 45     Steve Vestal (Honeywell) : "Formalizing Avionics Software Architectures"

14 h 45 - 16 h 00     Yaron Wolfsthal (IBM Haifa Research Labs) : "A Journey to the Center of the State Space: Formal (and Semi-Formal) Verification Methods at IBM"

16 h 00 - 16 h 30     Pause

16 h 30 - 17 h 45     Gérard Berry (Esterel Technologies) : "Control Dominated Critical Systems : Synthesis and Verification"

Jeudi 8 : Systèmes embarqués - Thursday 8^th : Embedded systems

Journée animée par Nicolas Halbwachs, Directeur de Recherche, CNRS

09 h 00 - 09 h 40     David Lesens (EADS lanceurs) : "Conception des logiciels critiques dans le domaine spatial"

09 h 40 - 10 h 20     Antoine Rauzy (LaBRI - Bordeaux) : "Compilation of data-flow AltaRica into fault trees"

10 h 20 - 11 h 00    François-Xavier Dormoy (Telelogic) : "SCADE: a Toolbox for the Development of Safety Critical Control Systems"

11 h 00 - 11 h 30     Pause

11 h 30 - 12 h 10     Mary Sheeran (Chalmer University / Prover Technology) : "SAT-based verification applied to SCADE: underlying methods"

12 h 10 - 12 h 50     Marten Saflund (Prover Technology) : "Taking Formal Verification of SCADE Designs to the Commercial Level"
                                 Replaced by:
                                 Nicolas Breton (Prover Technology) : "Proof Engines : The Next Big Software Advancement in Software Development"

12 h 50 - 14 h 30     Déjeuner

14 h 30 - 15 h 10     Odile Laurent (EADS Airbus) : "Les techniques de preuves formelles ouvrent-elles de nouvelles voies dans la stratégie de validation des systèmes avions ? Retour d'expérience sur le système de commandes de vols secondaires de l'A340/600"

15 h 10 - 15 h 50     Daniel Weil (France Telecom R&D) : " TAXYS : A tool for the development and verification of real-time embedded systems"

15 h 50 - 16 h 20     Pause

16 h 20 - 17 h 00     Paul Caspi (VERIMAG) : "Contrôle/commande : de l'asynchrone au synchrone et inversement"

 17 h 00 - 17 h 40     Samuel Boutin (Renault) : "Quelques éléments de réflexion sur l'évolution du processus de conception des logiciels embarqués de l'automobile"