École d’Été Temps Réel - Sciencesconf.org

Semaine Lun. 28 Mar. 29 Mer. 30 Jeu. 31 Ven. 01 Liste

	Lun. 28	Mar. 29	Mer. 30	Jeu. 31	Ven. 01
09:00 10:00 11:00 12:00 13:00 14:00 15:00 16:00 17:00 18:00 19:00 20:00 21:00 22:00 23:00	Accueil et inscriptions 13:00 - 14:00 (1h) Accueil et inscriptions Récupération du badge et des éléments associés Mot d'accueil des organisateurs 14:00 - 14:30 (30min) Mot d'accueil des organisateurs Présentation de la semaine ETR https://etr2017.sciencesconf.org/data/program/ETR_2017_bienvenue.pdf Vérification de systèmes temporisés et de systèmes temporisés paramétrés - Etienne André (LIPN / Université Paris 13) 14:30 - 15:30 (1h) Vérification de systèmes temporisés et de systèmes temporisés paramétrés - Etienne André (LIPN / Université Paris 13) Les automates temporisés représentent un formalisme puissant, permettant de spécifier et vérifier des systèmes concurrents soumis à des contraintes temporelles. Situés à la frontière de la décidabilité et de l'indécidabilité, ils peuvent être utilisés comme formalisme de spécification pour effectuer du model checking à l'aide de logiques temporelles temporisées, et ainsi déterminer si un système satisfait une propriété donnée. Les automates temporisés paramétrés permettent d'augmenter l'expressivité des automates temporisés en s'attaquant à un problème plus complexe : déterminer pour quelles valeurs des constantes temporelles (dans le modèle et/ou la propriété) le système satisfait une propriété donnée. Cette forte expressivité s'obtient au détriment de la décidabilité, mais les automates temporisés paramétrés ont néanmoins pu récemment résoudre des problèmes concrets dans le domaine de l'ordonnancement temps-réel. https://etr2017.sciencesconf.org/data/program/2017_08_28_ETR_final.pdf Pause café 15:30 - 16:00 (30min) Pause café Session doctorants - présentations / posters 16:00 - 18:00 (2h) Session doctorants - présentations / posters Cocktail de bienvenue 18:00 - 19:30 (1h30) Cocktail de bienvenue	Vérification et imposition de propriétés temporisées à l’exécution - Yliès Falcone (LIG, Université de Grenoble) 10:00 - 11:00 (1h) Vérification et imposition de propriétés temporisées à l’exécution - Yliès Falcone (LIG, Université de Grenoble) La vérification à l'exécution désigne les théories, techniques et outils pour déterminer si un système respecte l'ensemble de ses propriétés attendues à partir d'informations collectées durant son exécution. La vérification à l'exécution peut être appliquée lors du développement du système à des fins de débogage ou lorsque le système est en service pour détecter des comportements erratiques qui n'ont pu être évités durant sa conception. L'imposition à l'exécution complète la vérification à l'exécution et concerne plus particulièrement la prévention des erreurs et l'automatisation des réactions aux comportements erratiques. Dans cet exposé, nous présenterons les travaux menés en vérification et imposition de propriétés temporisées sur les systèmes temps réels. Les propriétés temporisées régissent non seulement le séquencement des actions dans les systèmes mais aussi le temps physique qui s'écoule entre ces actions. https://etr2017.sciencesconf.org/data/program/Falcone_ETR_2020.pdf Pause café 11:00 - 11:30 (30min) Pause café Vérification classique et statistique pour les systèmes probabilistes - Benoît Delahaye (LS2N, Université de Nantes) 11:30 - 12:30 (1h) Vérification classique et statistique pour les systèmes probabilistes - Benoît Delahaye (LS2N, Université de Nantes) La modélisation et l'abstraction des systèmes est aujourd'hui un point de passage nécéssaire à l'étude et à la compréhension de ceux-ci. Que ce soit dans le cadre de l'étude de systèmes physiques (sciences du vivant, automatique, ...) ou du développement de systèmes logiciels, il est souvent nécéssaire d'avoir recours aux probabilités pour abstraire des aspects trop complexes, prendre en compte l'incertitude due aux observations ou introduire artificiellement de l'aléatoire. Dans cet exposé, nous passerons en revue les différents formalismes de modélisation pour systèmes probabilistes (discrets, continus, avec ou sans non-déterminisme) ainsi que les principales méthodes de vérification applicables à ces modèles. Nous mettrons particulièrement l'accent sur la vérification de modèles probabiliste (exacte) et sur la vérification de modèles statistique (approchée). https://etr2017.sciencesconf.org/data/program/slides_delahaye.pdf Déjeuner 12:30 - 14:00 (1h30) Déjeuner Présentation de l'outil Cosmos - Benoît Barbot (LACL / Université Paris-Est Créteil) 14:00 - 14:30 (30min) Présentation de l'outil Cosmos - Benoît Barbot (LACL / Université Paris-Est Créteil) https://etr2017.sciencesconf.org/data/program/slides.pdf Présentation de l'outil Imitator - Etienne André (LIPN / Université Paris 13) 14:30 - 15:00 (30min) Présentation de l'outil Imitator - Etienne André (LIPN / Université Paris 13) https://etr2017.sciencesconf.org/data/program/2017_08_29_ETR_IMITATOR_final.pdf Présentation de l'outil Roméo - Didier Lime (LS2N / École Centrale de Nantes) 15:00 - 15:30 (30min) Présentation de l'outil Roméo - Didier Lime (LS2N / École Centrale de Nantes) https://etr2017.sciencesconf.org/data/program/DL_ETR_2017.pdf Pause café 15:30 - 16:00 (30min) Pause café Travaux pratiques au choix - Cosmos, Imitator, Roméo 16:00 - 17:30 (1h30) Travaux pratiques au choix - Cosmos, Imitator, Roméo https://etr2017.sciencesconf.org/data/program/TPetr.pdf	Uniprocessor Real-Time Scheduling - Julien Forget (Université de Lille) 9:00 - 10:30 (1h30) Uniprocessor Real-Time Scheduling - Julien Forget (Université de Lille) https://etr2017.sciencesconf.org/data/program/forget_etr2017.pdf Pause café 10:30 - 11:00 (30min) Pause café Systèmes d'exploitation temps réel pour l’embarqué - Mikaël Briday (IRCCyN, Université de Nantes) 11:00 - 12:00 (1h) Systèmes d'exploitation temps réel pour l’embarqué - Mikaël Briday (IRCCyN, Université de Nantes) Nous décrivons les principes d'architecture et de réalisation des systèmes d'exploitation temps réel pour l'informatique embarquée. Plus précisément, nous nous intéressons aux systèmes d'exploitation qui sont adaptés à l'exécution d'applications réactives de type contrôle-commande sur des cibles matérielles à base de microcontrôleurs. Nous nous intéressons en particulier aux fonctions de bas niveau utilisées par l'ordonnanceur (gestion de la liste des tâches prêtes, changement de contexte en mono- et multi-cœur). Cette présentation s'appuie en grande partie sur l'architecture de Trampoline, un exécutif temps réel disponible sous licence libre, aligné sur les standards industriels issus de l'automobile OSEK/VDX OS et AUTOSAR OS. https://etr2017.sciencesconf.org/data/program/pres_etr_2017.pdf Analyse de WCET - Hugues Cassé (UPS / IRIT) 12:00 - 13:00 (1h) Analyse de WCET - Hugues Cassé (UPS / IRIT) https://etr2017.sciencesconf.org/data/program/presentation_WCET.pdf Déjeuner 13:00 - 14:30 (1h30) Déjeuner Ordonnancement multiprocesseurs : théorie et pratique - Mathieu Jan (CEA LIST) 14:30 - 16:00 (1h30) Ordonnancement multiprocesseurs : théorie et pratique - Mathieu Jan (CEA LIST) https://etr2017.sciencesconf.org/data/program/ETR_2017_ordo_multi.pdf Pause café 16:00 - 16:30 (30min) Pause café TP ordonnancement avec l'outil Cheddar - Frank Singhoff (Lab-STICC-Université de Bretagne Occidentale) TP sur le système d'exploitation Trampoline/OSEK - Mikaël Briday (IRCCyN, Université de Nantes) TP sur l'estimation des WCET avec Heptane - Damien Hardy (IRISA / Université de Rennes 1) 16:30 - 17:30 (1h) TP ordonnancement avec l'outil Cheddar - Frank Singhoff (Lab-STICC-Université de Bretagne Occidentale) 16:30 - 17:30 (1h) TP sur le système d'exploitation Trampoline/OSEK - Mikaël Briday (IRCCyN, Université de Nantes) 16:30 - 17:30 (1h) TP sur l'estimation des WCET avec Heptane - Damien Hardy (IRISA / Université de Rennes 1)	Normes pour la Sûreté de fonctionnement Logiciel et système - Groupe de travail NSL Embedded France 9:00 - 10:00 (1h) Normes pour la Sûreté de fonctionnement Logiciel et système - Groupe de travail NSL Embedded France Cette présentation introduira succinctement les normes de sûreté de fonctionnement concernant les aspects systèmes et logiciels dans différents domaines d'application : aéronautique, automatismes industriels, automobile, espace, nucléaire, transport ferroviaire. Puis certaines similitudes et différences entre les différents domaines seront expliquées. Cette présentation est basée sur le travail réalisé au sein d'Embedded France avec pour objectif d'identifier les principales similitudes et différences de ces normes en vue d'une potentielle harmonisation entre domaines. https://etr2017.sciencesconf.org/data/program/ETR2017_2017_08_30_v1.2.pdf Pause café 10:00 - 10:30 (30min) Pause café Asterios : d'un modèle de calcul parallèle déterministe à la réalisation d'un système Temps-Réel Critique - Emmanuel Ohayon (Krono-Safe) 10:30 - 12:30 (2h) Asterios : d'un modèle de calcul parallèle déterministe à la réalisation d'un système Temps-Réel Critique - Emmanuel Ohayon (Krono-Safe) https://etr2017.sciencesconf.org/data/program/AsteriosInNutshell_pub.pdf Déjeuner 12:30 - 14:00 (1h30) Déjeuner TP conception d'applicatifs temps réel avec Astérios (Krono-Safe) 14:00 - 15:30 (1h30) TP conception d'applicatifs temps réel avec Astérios (Krono-Safe) Pause café 15:30 - 16:00 (30min) Pause café Transformations de modèles pour l'analyse et l'optimisation d'architectures de systèmes temps-réels critiques - Etienne Borde (Telecom ParisTech) 16:00 - 17:00 (1h) Transformations de modèles pour l'analyse et l'optimisation d'architectures de systèmes temps-réels critiques - Etienne Borde (Telecom ParisTech) https://etr2017.sciencesconf.org/data/program/ETR_2017_IDM_Borde.pdf Social event 18:00 - 23:30 (5h30) Social event	Network-on-Chip service guarantees - Benoît De Dinechin (Kalray) 9:00 - 10:00 (1h) Network-on-Chip service guarantees - Benoît De Dinechin (Kalray) https://etr2017.sciencesconf.org/data/program/Kalray_ETR_2018.pdf SMT-based Schedule Synthesis for Time-Sensitive Networks - Silviu S. Craciunas (TTTech Computertechnik AG) 10:00 - 11:00 (1h) SMT-based Schedule Synthesis for Time-Sensitive Networks - Silviu S. Craciunas (TTTech Computertechnik AG) We will introduce and discuss the TSN sub-standards currently being defined by the Time-Sensitive Networking Task Group and present methods for computing fully deterministic schedules for 802.1Qbv-compliant multi-hop switched networks using Satisfiability Modulo Theories (SMT) and, alternatively, Optimization Modulo Theories (OMT) solvers. We identify and analyze key functional parameters affecting the deterministic behaviour of real-time communication under 802.1Qbv and, based on a generalized configuration of these parameters, derive the required constraints for computing offline schedules guaranteeing low and bounded jitter and deterministic end-to-end latency for critical communication flows. Furthermore, we discuss several optimization directions and concrete configurations exposing trade-offs against the required computation time. We also show the performance of our approach via synthetic network workloads on top of different network configurations. https://etr2017.sciencesconf.org/data/program/craciunas_etr2017_talk.pdf Pause café 11:00 - 11:30 (30min) Pause café Evolutions de l'architecture réseau à bord des avions: interconnexion NoC-AFDX - Jean-Luc Scharbarg ( IRIT/INPT/ENSEEIHT) 11:30 - 12:30 (1h) Evolutions de l'architecture réseau à bord des avions: interconnexion NoC-AFDX - Jean-Luc Scharbarg ( IRIT/INPT/ENSEEIHT) https://etr2017.sciencesconf.org/data/program/TalkEtr2017.pdf