lundi 28 août 2017

Heures événement  
13:00 - 14:00 Accueil et inscriptions - Récupération du badge et des éléments associés  
14:00 - 14:30 Mot d'accueil des organisateurs - Présentation de la semaine ETR
 
14:30 - 15:30 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.
 
15:30 - 16:00 Pause café  
16:00 - 18:00 Session doctorants - présentations / posters  
18:00 - 19:30 Cocktail de bienvenue  

mardi 29 août 2017

Heures événement  
10:00 - 11:00 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.
 
11:00 - 11:30 Pause café  
11:30 - 12:30 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).
 
12:30 - 14:00 Déjeuner  
14:00 - 14:30 Présentation de l'outil Cosmos - Benoît Barbot (LACL / Université Paris-Est Créteil)
 
14:30 - 15:00 Présentation de l'outil Imitator - Etienne André (LIPN / Université Paris 13)
 
15:00 - 15:30 Présentation de l'outil Roméo - Didier Lime (LS2N / École Centrale de Nantes)
 
15:30 - 16:00 Pause café  
16:00 - 17:30 Travaux pratiques au choix - Cosmos, Imitator, Roméo
 

mercredi 30 août 2017

Heures événement  
09:00 - 10:30 Uniprocessor Real-Time Scheduling - Julien Forget (Université de Lille)
 
10:30 - 11:00 Pause café  
11:00 - 12:00 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.
 
12:00 - 13:00 Analyse de WCET - Hugues Cassé (UPS / IRIT)
 
13:00 - 14:30 Déjeuner  
14:30 - 16:00 Ordonnancement multiprocesseurs : théorie et pratique - Mathieu Jan (CEA LIST)
 
16:00 - 16:30 Pause café  
16:30 - 17:30 TP ordonnancement avec l'outil Cheddar - Frank Singhoff (Lab-STICC-Université de Bretagne Occidentale)  
16:30 - 17:30 TP sur le système d'exploitation Trampoline/OSEK - Mikaël Briday (IRCCyN, Université de Nantes)  
16:30 - 17:30 TP sur l'estimation des WCET avec Heptane - Damien Hardy (IRISA / Université de Rennes 1)  

jeudi 31 août 2017

Heures événement  
09:00 - 10:00 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.
 
10:00 - 10:30 Pause café  
10:30 - 12:30 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)
 
12:30 - 14:00 Déjeuner  
14:00 - 15:30 TP conception d'applicatifs temps réel avec Astérios (Krono-Safe)  
15:30 - 16:00 Pause café  
16:00 - 17:00 Transformations de modèles pour l'analyse et l'optimisation d'architectures de systèmes temps-réels critiques - Etienne Borde (Telecom ParisTech)
 
18:00 - 23:30 Social event - Surprise !  

vendredi 1 septembre 2017

Heures événement  
09:00 - 10:00 Network-on-Chip service guarantees - Benoît De Dinechin (Kalray)
 
10:00 - 11:00 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.
 
11:00 - 11:30 Pause café  
11:30 - 12:30 Evolutions de l'architecture réseau à bord des avions: interconnexion NoC-AFDX - Jean-Luc Scharbarg ( IRIT/INPT/ENSEEIHT)