Vue d'ensemble du programme

L'ensemble des présentations auront lieu dans la salle Petri/Turing. Les travaux pratiques auront lieu dans le bâtiment de travaux pratiques de l'ISTIC (BATO).

Le programme en détails

Méthodes formelles

• Thierry Jéron (Inria Rennes Bretagne Atlantique) - Model-based conformance test generation for timed systems (1h)
  The talk presents the main principles of automatic test generation for timed automata models. We consider the model of timed automata with inputs/outputs (TAIOs), an extension of timed automata, well suited for the specification of systems with both timing constraints and interaction with their environment. We review the underlying testing theory tioco which extends the classical ioco theory to the timed context. Test generation from TAIOs is then explained, with in particular the underlying problem of partial observation for a priori non-deterministic and even non-determinizable models.
• Ocan Sankur (Université Libre de Bruxelles, Belgique), Contrôle des systèmes temporisés (1h)
  On s'intéresse à la synthèse de contrôleur pour les systèmes temporisés en utilisant le formalisme d'automates temporisés. Ce formalisme permet la modélisation des systèmes qui ont une structure de contrôle discrète mais aussi des contraintes de de temps. Le but de la synthèse de contrôleur est de construire un contrôleur pour le système qui assure la spécification en présence des entrées incontrôlables fournies par l'environnement. On présentera la représentation symbolique de l'espace d'états, les algorithmes de synthèse, ainsi que des exemples.
• Frédéric Lang (Inria Grenoble Rhône Alpes) - Vérification de logique temporelle et d'équivalences par des méthodes compositionnelles (1h)
  Les systèmes modernes (matériels et logiciels) sont souvent constitués de "tâches" qui s'exécutent en parallèle et communiquent. La complexité qui en découle nécessite de disposer d'outils permettant de vérifier leur bon fonctionnement, en particulier pour les systèmes critiques. Cet exposé abordera la modélisation formelle de ces systèmes sous forme de réseaux de processus communicants, ainsi que de leurs propriétés, soit sous forme de formules de logique temporelle, soit sous forme d'automate. Nous aborderons le problème consistant à vérifier ces propriétés en tentant de repousser le problème de l'explosion combinatoire des états, notamment par des méthodes compositionnelles.
• Présentation d'outils (1h30) :
  
  • CADP, Construction and Analysis of Distributed Processes (http://cadp.inria.fr) (Frédéric Lang, Inria Grenoble Rhône Alpes)
    CADP est une boîte à outils pour la conception des systèmes concurrents asynchrones, tels que  les protocoles de communication, les systèmes distribués, les circuits asynchrones, les architecturesmulti-processeurs, les services web, etc. CADP offre un large éventail de fonctionnalités, de la simulation pas à pas au model-checking massivement parallèle. CADP prend en entrée la description d'un système écrit soit dans un langage structuré (LOTOS, LNT, FSP, etc.) soit à un plus bas niveau, dans un langage de description d'automates ou de réseaux d'automates communicants. Des compilateurs permettent la génération de code C  utilisable pour la simulation, la vérification et le test. Les propriétés peuvent être décrites sous la forme d'automates ou dans des logiques temporelles étendues avec des données. CADP implémente des algorithmes de vérification énumérative, vérification à la volée, vérification symbolique (BDD), vérification compositionnelle, ordres partiels, vérification distribuée, etc., qui peuvent parfois être combinés. En outre, CADP offre d'autres fonctionnalités variées, telles que la vérification visuelle ou l'évaluation de performances.
  • TINA, TIme Petri Net Analyze (http://www.laas.fr/tina/) (Bernard Berthomieu, LAAS-CNRS,  Silvano Dal Zilio, LAAS-CNRS, François Vernadat, LAAS-CNRS, INSA)
    TINA - TIme Petri Net Analyzer est un  environnement logiciel permettant l’édition et l’analyse de réseaux de  Petri temporels étendus avec des priorités et un traitement de données  externes synchronisé avec l’évolution du réseau. Sur ces modèles, TINA  permet la vérification de propriétés par model-checking pour, notamment, la logique temporelle à temps linéaire State/Event LTL. TINA accepte aussi en entrée des descriptions de plus haut niveau écrites  en FIACRE. Fiacre — Format Intermédiaire pour les Architectures de  Composants Répartis Embarqué http://www.laas.fr/fiacre/ — est un  langage formel pour la description de systèmes temps réel. Fiacre a été initialement développé en collaboration avec IRIT/Acadie et INRIA/Convecs
    dans le cadre de l’ACI éponyme et du projet Topcased. Le langage FIACRE décrit des composants. Les composants élémentaires sont des machines à états étendues; des composants plus complexes sont décrits hiérarchiquement, et de façon compositionnelle, par assemblage de composants plus simples dont les interactions peuvent être contraintes par des exigences temporelles et des priorités.
  • IMITATOR (http://www.imitator.fr/) (Etienne André, LIPN).
    IMITATOR est un outil pour la vérification de systèmes temps-réel, modélisés par des automates temporisés paramétrés étendus avec des chronomètres (stopwatches) et des variables. La vérification paramétrée permet de vérifier un système dont les constantes temporelles ne sont pas encore connues, ou qui présentent des incertitudes. IMITATOR permet aussi d'évaluer la robustesse d'un système temps-réel à des petites variations de temps. IMITATOR a été appliqué à de nombreuses études de cas de la littérature et de l'industrie, telles que des protocoles de communication, des circuits asynchrones, des problèmes d'ordonnancement, ou des machines à café (certainement le système le plus critique pour un chercheur). Des sorties graphiques permettent de visualiser le comportement du système ainsi que les plages de bon fonctionnement.
• Travaux pratiques sur les outils CADP (Frédéric Lang, Inria Grenoble Rhône Alpes), TINA (François Vernadat ou Bernard Berthomieu) et IMITATOR (Etienne André, LIPN) (en parallèle)

Ordonnancement et supports d’exécution

• Giuseppe Lipari (Université de Lille) - Real-Time scheduling from hard to soft real-time systems (2h)
  Real-time systems are traditionally classified into hard and soft real-time. However, the frontier between these two classes is blurred, and many systems that were considered as hard real-time in the past can now be seen under a completely different light. We shall first recall the fundamental notion of time predictability and criticality, in order to understand where the real-time deadlines that we use in our theoretical models come from. We will also summarise the most important classical results for hard real-time scheduling and discuss their robustness under varying parameters. We will then introduce the notion of soft real-time system and present the resource reservation framework. We will demonstrate its application using the novel SCHED_DEADLINE scheduling class of the Linux kernel. Finally, we will show how resource reservation techniques can be successfully applied to control systems.
• Sebastien Faucou (IRCCyN, Université de Nantes) - Systèmes d'exploitation temps réel pour l'informatique embarquée (1h)
  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 de type micro-contrôleurs. Nous illustrons notre propos à l'aide d'exemples de systèmes électriques/électroniques embarqués du domaine automobile. Nous décrivons également la façon dont ces systèmes d'exploitation peuvent, sur des architectures matérielles adaptées, co-habiter avec des systèmes généralistes grâce aux techniques de virtualisation. Nous nous intéressons en particulier aux garanties temps réel qui peuvent être apportées dans les systèmes virtualisés.
• Eric Noulard (Onera) - Real-time scheduling on multi/many-processor: from specification to real-time execution (1h30)
  The uniprocessor era is probably already over, thus real-time embedded systems have to tackle at least multi- if not many processor architectures. Multi-processor real-time scheduling is an active domain of research for some time now. Even if we have some schedulability theoretical results, the way to go from application specification down to real-time execution is not easy. Based on the ROSACE open case study we will examine some concrete proposal on how to: Specify a multi-rate real-time application using high level language like Simulink, Prelude or Lustre. Do a multi-core schedulability analysis using SchedMCore Generate code from the specification using Prelude and/or Lustre compiler tools Run the resulting application on a multi-core platform. We will show how this can apply to many-core architecture as well. We will present practical multi/many-processor schedulability analysis. We will show how resctricted multi-processor real-time execution model enables both the analysis and the execution on real hardware.
• Frank Singhoff (Université de Brest / Lab-STICC) - Real Time Scheduling Analysis Lab, an example with Cheddar (1h30)
  The objective of this tutorial is to illustrate classical real-time scheduling analysis methods and results. The tutorial will have the form of a very short lecture, with hand-outs and tools made available to participants. The short lecture will present various issues raised when implementing or using real-time scheduling tools. A focus on Cheddar will be more specifically addressed. The hand-outs will show how to use or apply a sample of classical analysis algorithms for various architecture types.

Enjeux industriels

• Jean-Baptiste Chaudron, Jacques Gatard (TTTech) - TTEthernet: Theory, Concepts and Applications (3h)
  Distributed critical systems become more and more complex and involve a lot of components communicating and interacting over a network. To meet the real-time requirements of such applications, the network itself must ensure a deterministic behavior. Design of precision and safety-critical applications usually adopts time-triggered protocols as the communication infrastructure to fulfil real-time properties. TTEthernet technology offers a new method for deterministic and time-triggered data transfer over Ethernet. It makes it possible to overcome the inherent lack of determinism of Ethernet networks by enabling a synchronization strategy and applying strict scheduling rules to data transmission. TTEthernet provides a communication infrastructure for mixed criticality systems that integrates data flow from applications with different criticality levels on a single network:
  • Time-Triggered traffic type (SAE AS6802)
  • Traffic type with fully deterministic operation, plus very low latency and jitter;
  • Rate Constrained traffic type (ARINC 664 part 7)
  • Traffic type which is certified on the Boeing 787, and Airbus A380, plus being applied to other new and retrofit aircraft applications; Best Effort traffic type (IEEE 802.3 Ethernet) Traffic type which allows standard Ethernet message to use unallocated bandwidth assigned to the other higher priority traffic types.

To summarize, this seminar will introduce TTEthernet theory and concepts:

• Communication characteristics;
• Clock synchronization principles;
• Fault tolerance properties;
• Short demo with TTEthernet Tools;
• Overview of existing TTEthernet products and applications.

Développement d’applications temps réel

• Jean-Pierre Talpin (Inria Rennes Bretagne Atlantique) - Sémantique formelle de modèles d’architecture (1h)
  Un modèle d’architecture est un artefact dans la conception d’un système critique qui se trouve au croisement des trois composantes majeures d’un système: son logiciel: contrôleur, pilote, système d’exploitation; son matériel: capteurs, bus, processeurs, mémoire, actuateurs; son environnement mécanique et physique. Le temps intervient de manière prépondérante dans la conception de ces composantes, toutes les propriétés et modèles de leurs éléments paramètrés par le temps: il est discret et logique en logiciel (“event driven”), il est discret et périodique en matériel (“time-triggered”), continu en physique. Plus encore au moment de leur intégration, et c’est la que le modèle d’architecture sert de plan, de patron de conception. Pensons par exemple à l’ordonnancement temps-réel, où l’on cherche à mitiger le temps logique (ou la causalité) du logiciel avec le temps périodique (ou multi-périodique) d’un processeur (ou d’un multi-coeurs). Nous considérons ici un standard pour la modélisation d’architectures de systèmes: AADL ("architecture analysis and design standard”) et, à l’instar de la définition de CCSL pour UML, montrons comment y associer une sémantique formelle, à la fois fidèle à la spécification du standard, et d’un pouvoir d’expression suffisant pour exprimer les différentes caractéristiques d’une architecture de système, ici essentiellement logicielle et matérielle.
• Sebastien Gerard (CEA LIST) - les contours de MARTE par l'exemple (1h)
  Le langage de modélisation UML n'est plus une option. MARTE est son compagnon indispensable dans le domaine du développement des systèmes embarqués temps-réel et distribués. L'objet de cette présentation est de fournir une introduction pratique à MARTE. Pour ce faire, on fournira d'une part une vue haut niveau de MARTE et on illustrera d'autre part son usage sur un exemple applicatif simple. A travers cette présentation, on vise à fournir les clés pour exploiter au mieux cette norme internationale de modélisation et d'analyse de systèmes embarqués et temps-réel. Pour cela, la présentation reviendra également sur une liste de cas d'utilisation standards de la norme.
• Marc Pantel (IRIT) - The UML/MARTE Verifier: A Property Driven toolchain for model checking real time systems (1h)
  The verification of real time systems is a very complex activity as these ones usually combine concurrent behavior with stringent timing constraints. Formal methods, and especially model checking, have been applied successfully on many realistic industrial systems. However, these methods usually require the end user to provide an abstract model that focuses on the appropriate aspects of the systems using a verification dedicated language. The building of these models requires both a good knowledge of the subject systems and of the verification technology. In order to ease that work, model driven engineering advocates the use of user level real time dedicated languages like UML/MARTE and model transformation from the user level to the verification level. However, a generic transformation usually produces verification models whose model checking do not scale well with the system size. This talk will present how these transformations can be dedicated to some specific properties and thus improve the scalability. It will rely on aeronautic distributed applications in that purpose.

Réseaux temps réel et qualité de service

• Luis Almeida (IT - University of Porto, Portugal) - Flexible Time-Triggered Switched Ethernet: Towards Flexible/Open Cyber-Physical Systems (45 mn)
  The Flexible Time-Triggered Switched Ethernet (FTT-SE) protocol was proposed in 2006 as a realization of the FTT paradigm specifically adapted to switched Ethernet. This paradigm is a framework to develop distributed real-time systems that are reconfigurable and adaptive. It has been successfully used for dynamic Quality-of-Service (QoS) management in control applications and video transmission, and for dynamic reconfiguration of real-time systems that are either open or include subsystems that operate occasionally. It is particularly suited to support dynamic and adaptive resource reservation in network resources through virtual channels. In the realm of real-time Ethernet protocols, FTT-SE flexibility features with real-time guarantees are unique, possibly comparable to much more costly solutions, only, such as layer 3 or 2.5 carrier- grade switches with RSVP-TE or MPLS, AVBridges or Software-Defined Networks (SDNs).
  In this talk we highlight recent FTT developments in the context of switched Ethernet technology. We start with FTT-SE protocol basics and then discuss how to improve performance and robustness with the HaRTES switch that is an FTT-enabled Ethernet switch, as well as scalability and dependability of FTT-SE/HaRTES systems. We end with several use cases that show the features of these systems.

• Jean-Luc Scharbarg (INPT/ENSEEIHT) - solutions Ethernet commuté pour réseaux embarqués temps réel (45 mn)
  Les systèmes embarqués à bord des avions, des automobiles ou des satellites sont constitués d'un ensemble de fonctions toujours plus nombreuses, distribuées sur un ensemble de calculateurs. De plus en plus de données de nature différente sont échangées entre ces fonctions. Ces données sont agrégées dans des flux. Chaque flux peut avoir une contrainte de délai à respecter, en fonction du type des données qui le composent. La solution qui se dégage aujourd'hui est fondée sur un réseau Ethernet commuté full duplex. Ce type de réseau offre un débit important et il n'y a pas de collision au niveau des liens. Cette dernière caractéristique n'est pas suffisante pour maîtriser les délais. En effet, une trame donnée est retardée dans chacun des commutateurs qu'elle traverse, en fonction des trames qui la précède dans les files d'attente. Pour borner ces délais d'attente, il est nécessaire de contraindre chaque flux. La solution la plus courante consiste à limiter le débit de chaque flux. En outre, il est possible de contrôler la bande passante offerte à chaque flux ou chaque type de flux. L'objectif de cet exposé est de présenter et comparer les solutions Ethernet commuté les plus prometteuses pour ce contexte embarqué temps réel. En particulier, on s'intéressera à l'AFDX, à Ethernet AVB et à TTEthernet

• Thomas Watteyne (Inria Paris Rocquencourt) et Pascal Thubert (Cisco) - réseaux de capteurs sans fil et déterministe (IEEE802.15.4e, OpenWSN et IETF 6TiSCH) - 1h30
  Real-time applications require deterministic networks capable of transporting data with high reliability and bounded latency. Low-power wireless technology often operates on a single frequency chennel and uses contention-based medium access techniques, preventing these networks to offer the determinism for real-time applications. This is about to change with the technology being standardized in the IETF 6TiSCH working group. The 6TiSCH architecture is based on the revolutionary Time Synchronized Channel Hopping (TSCH) technology, as the heart of the IEEE802.15.4e amendment. In a 6TiSCH network, all nodes are tightly synchronized and the communication is orchestrated by a communication schedule. Time synchronization allows node to offers a battery lifetime of over 5 years; channel hopping yields end-to-end reliability above 99,9%. 6TiSCH is the cornerstone technology for tomorrow’s Industrial Internet of Things. This talk will start by presenting real-world dense connectivity traces which highlight the different challenges a low-power wireless network is face by, justifying the use of Time Slotted Channel Hopping, the core technology of the IEEE802.15.4e standard. We will give a demonstration of OpenWSN, the de-facto open source implementation of TSCH. The second half of this presentation will focus on the standardization work happening within the IETF 6TiSCH working group. 6TiSCH allows for deterministic routing, resulting in a network which can support real-time application requirements.