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.
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.
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).
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.
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.
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/ETR_2017_bienvenue.pdf
