Séminaire vérification de Toulouse

L'analyse formelle de programmes qui implémentent des lois de contrôle est difficile en raison d'un coeur numérique souvent complexe. Les outils mathématiques de l'automatique permettent cependant de prouver des propriétés fonctionnelles fortes sur ces lois, notamment dans leur interaction avec le système contrôlé. L'idée est alors de donner les moyens à l'automaticien de fournir à la certification logicielle, en plus de la loi de contrôle, des informations facilitant son analyse. Cette présentation décrit, d'une part, un framework complet permettant d'inclure à un diagramme Simulink des informations sur la stabilité interne d'une loi de contrôle, puis de générer automatiquement du code C annoté en ACSL avec les informations en questions, pour enfin prouver, également automatiquement, cette stabilité interne au niveau des variables du code, à l'aide d'une interface PVS. D'autre part, d'autres types de propriétés sont envisagés, tels que la stabilité de l'interaction contrôleur/système contrôlé, mais aussi des critères de performance et de robustesse concernant cette interaction. Il est démontré comment ces propriétés peuvent être exprimés comme des invariants de code.

Depuis une dizaine d'année, la généralisation des architectures multiprocesseurs a apporté un regain d'intérêt à l'étude de l'ordonnancement temps réel. Cependant l'adaptation des politiques d'ordonnancement monoprocesseur au cadre multiprocesseur n'est pas sans poser de problèmes, en particulier en ce qui concerne leur prédictibilité et leur efficacité. Le travail présenté dans ce séminaire s'inscrit dans ce cadre et se focalise sur le comportement des ordonnanceurs en tenant compte des mémoires caches.
En effet, la prise en compte des mémoires caches dans l'étude du comportement d'un ordonnanceur temps réel multiprocesseur est très complexe. Non seulement un cache peut perdre son affinité avec une tâche suite à une préemption comme dans le cas monoprocesseur, mais en plus, s'il est partagé entre plusieurs processeurs, il peut être pollué par des tâches s'exécutant simultanément.
À terme, le but de notre étude est la comparaison des nombreuses politiques d'ordonnancement existantes en considérant l'architecture matérielle. Pour cela, nous souhaitons offrir un outil facile pour prototyper un algorithme et l'évaluer.
Plusieurs approches existent pour étudier les politiques d'ordonnancement. Une première consiste à étudier analytiquement l'ordonnançabilité des systèmes, mais est limitée dans son expressivité pour prendre en considération des aspects liés à l'architecture. Une seconde vise à vérifier expérimentalement, par simulation fine ou sur un système réel, le comportement des politiques d'ordonnancement. L'inconvénient majeure de cette approche est la difficulté pour prendre en main de tels outils et pour conduire des tests de grande envergure.
L'étude que nous proposons se situe à mi-parcours entre ces deux approches en proposant un outil de simulation simple, mais suffisamment précis pour reproduire le comportement réel d'un système. Pour cela, nous nous basons sur le modèle de Liu et Layland que nous étendons afin d'intégrer des informations sur le comportement mémoire des tâches. Ces informations additionnelles nous permettent alors de faire des estimations statistiques afin d'évaluer les performances des politiques d'ordonnancement.

Building safety-critical real-time systems out of inexpensive, non-realtime, COTS components is challenging. Although COTS components generally offer high performance, they can occasionally incur significant timing delays. To prevent this, we propose two approaches: 1) a new "clean slate" real-time, memory-centric scheduling paradigm, named PRedictable Execution Model (PREM); and 2) a framework of novel application-transparent, kernel-level techniques to perform fine-grained resource reservation of cache space and memory bandwidth in multi-core real-time systems.
We have successfully implemented and tested the proposed framework on a commodity ARM-based system and on a Freescale P4080 platform; it can also be applied to a variety of other platforms currently available on the market. Finally, experimental benchmark results show that employing the proposed techniques to eliminate (last level) cache and memory bandwidth interference can lead up to a 250% improvement of the measured worst-case execution time.
Bio: Marco Caccamo received a Ph.D. in Computer Engineering from Scuola Superiore Sant'Anna, Italy in 2002. He is Associate Professor at Department of Computer Science, University of Illinois at Urbana-Champaign. His research interests include real-time operating systems, real-time scheduling and resource management, wireless real-time networks, and quality of service control in next generation digital infrastructures.

La conception des systèmes critiques s'appuie aujourd'hui largement sur l'usage de méthodes formelles afin de pouvoir certifier certaines propriétés de sûreté des systèmes, sur le modèle classique du cycle en V. Dans le même temps, les concepteurs d'interfaces hommes machines tentent d'améliorer la prise en compte des aspects humains, souvent de manière informelle, en utilisant de méthodes itératives faisant la part belle au prototypage et au test.
La conception d'interfaces hommes machines critiques est donc tiraillée entre deux approches opposées : Cycle en V ou développement itératif ? Méthodes formelles ou expérimentation empirique ? Face à ce problème relativement nouveau, nous tenterons d'apporter une réponse qui garde les aspects positifs des deux approches, tout en minimisant leurs incompatibilités.
Nous allons donc présenter un langage et une méthode de développement destinés aux interfaces hommes machines et permettant de profiter des avancées en matière de méthodes formelles. Après un tour d'horizon des solutions déjà existantes, nous présenterons le langage proposé, et son positionnement par rapport aux initiatives existantes. L'application de la méthode proposée sur un exemple permettra d'en avoir une vue plus concrète, afin d'en découvrir les limites, mais aussi les perspectives qu'elle ouvre.

Dans cet exposé, nous présenterons l'état actuel du projet Insight développé au LaBRI, qui a pour but d'analyser du code binaire.
L'analyse de code binaire est rendue difficile notamment par le fait que le graphe de flot de contrôle n'est pas disponible explicitement, et que les types des variables ne sont pas spécifiés. Il faut ajouter à cela la difficulté technique de décoder les mnémoniques de processeurs existants comme les processeurs Intel 32 bits.
Le modèle formel utilisé dans Insight sera présenté, et une application à la reconstruction d'un graphe de flot de contrôle sera détaillée. Les directions futures seront discutées.

Jury : - Mme Françoise SIMONOT-LION - Rapporteur (Professeur, Université de Nancy) - Mr Franck SINGHOFF - Rapporteur (Professeur, Université de Bretagne Occidentale, Brest) - Mr Jean-Christophe BONNET - Examinateur (DGA, Bagneux) - Mme Eva CRUCK - Examinateur (DGA/MRIS, Bagneux) - Mr Jean-Charles FABRE - Examinateur (Professeur, ENSEEIHT, Toulouse) - Mr Pierre-Emmanuel HLADIK - Examinateur (Maître de Conférence, INSA, Toulouse) - Mr Frédéric BONIOL - Directeur (ONERA) - Mr David DOOSE - Co-directeur (ONERA)
La conception des plateformes aéronautiques s’effectue en tenant compte des aspects fonctionnels et dysfonctionnels prévus dans les scénarios d’emploi des aéronefs qui les embarquent. Ces plateformes aéronautiques sont composées de systèmes informatiques temps réel qui doivent à la fois être précises dans leurs calculs, exactes dans l’instant de délivrance des résultats des calculs, et robustes à tout évènement pouvant compromettre le bon fonctionnement de la plateforme. Dans ce contexte, ces travaux de thèse abordent les ordonnancements temps réel tolérants aux fautes. Partant du fait que les systèmes informatiques embarqués sont perturbés par les ondes élec- tromagnétiques des radars, notamment dans la phase d’approche des aéronefs, ces travaux proposent une modélisation des effets des ondes, dite en rafales de fautes. Après avoir exploré le comportement de l’ordonnanceur à la détection d’erreurs au sein d’une tâche, une technique de validation, reposant sur le calcul de pire temps de réponse des tâches, est présentée. Il devient alors possible d’effectuer des analyses d’ordonnançabilité sous l’hypothèse de la présence de rafales de fautes. Ainsi, cette technique de validation permet de conclure sur la faisabilité d’un ensemble de tâches en tenant compte de la durée de la rafale de fautes et de la stratégie de gestion des erreurs détectées dans les tâches. Sur la base de ces résultats, les travaux décrits montre comment envisager l’analyse au niveau système. L’idée sous-jacente est de mettre en évidence le rôle des ordonnancements temps réel tolérants aux fautes dans la gestion des données erronées causées par des perturbations extérieures au système. Ainsi, le comportement de chaque équipement est modélisé, ainsi que les flots de données échangés et la dynamique du système. Le comportement de chaque équipement est fonction de la perturbation subie, et donne lieu à l’établissement de la perturbation résultante, véritable réponse dysfonctionnelle de l’équipement à une agression extérieure.

Ce séminaire fait suite à la présentation de Charles Lesire: "Comment savoir si mon robot va (correctement) fonctionner ? ou quelques idées autour de la validation des architectures logicielles de contrôle". Nous présenterons la méthode mise en place pour la conception d'architectures robotiques "correctes" et les techniques que nous avons développées pour l'analyse de ces systèmes. Les architectures ainsi définies sont un assemblage de composants qui communiquent par échanges de données et appels de méthodes. Les analyses consistent principalement à étudier le respect des échéances et certaines propriétés dites "comportementales" des composants de l'architectures.
Liens: Ces travaux sont en liens avec deux projets IDEAS et Quarteft. De plus, une partie de ces analyses sont réalisées grâce à la boite à outils de model-checking du LAAS (Fiacre/Tina). L'outil Otawa de l'Irit a été utilisé pour l'obtention de WCET indispensables à l'analyse.

The reachability problem for timed automata asks if there exists a path from an initial state to a target state. The standard solution to this problem involves computing the zone graph of the automaton, which in principle could be infinite. In order to make the graph finite, zones are approximated using an extrapolation operator. For reasons of efficiency in current algorithms, extrapolation of a zone is always a zone; and in particular it is convex.
We propose to solve the reachability problem without such extrapolation operators. To ensure termination, we provide an efficient algorithm to check if a zone is included in the aLU abstraction of another. Although theoretically better, aLU cannot be used in the standard algorithm since an abstraction of a zone may not be convex.
An additional benefit of the proposed approach is that it permits to calculate approximating parameters on-the-fly during exploration of the zone graph, as opposed to the current methods which do it by a static analysis of the automaton prior to the exploration. This allows for further improvements in the algorithm. Promising experimental results are presented.

Cette présentation reprend les travaux développés dans la thèse de Michaël Lauer en les étendant aux systèmes temps réel à priorités fixes communiquant via un réseau à qualité de service garantie. Cet exposé présente :

• la notion de latence de bout en bout
• puis une méthode de calcul de (latence de bout en bout) reposant sur la résolution d'un problème MILP (Mixed Integer Linear Programming problem).

L'exposé s'appuie sur une étude de cas avionique, et le passage à l'échelle de la méthode est montré sur un ensemble d'expériemntations sur cette étude de cas. S'il reste du temps, l'exposé montrera comment la méthode peut être naturellement étendue aux propriétés de "fraicheur" et de "reactivité".

With the increasing complexity of embedded networks and the expansion of exchanged data quantity, making the right design decisions to guarantee the systems requirements becomes a difficult task for designer. Hence, it becomes one of the major challenges in the design process to analyze the systems characteristics till the first steps of the development cycle. Simulations are commonly used for exploring the design space and validating the functional and timing behaviors of the embedded networks. However, these approaches are feasible for only small parts of the system and cannot cover the entire domain of the model applicability and especially rare events that represent worst-case functioning of the system. So, clearly, simulations cannot provide the deterministic guarantees required by critical embedded networks with hard certification requirements to respect like in civil and military avionics, automotive and satellites, where a failure might have a disastrous consequence on the system. With a formal specification language like StateCharts or Specification and Description Language (SDL), it is possible to verify the functional behavior of the network. However, for big networks with an important number of nodes, this approach leads to a space explosion problem inherent to the reachability analysis techniques implemented by the formal verification tools. In order to overcome these limitations, integrating an aided-decision tool till the first steps of the design process becomes necessary to choose the right systems parameters to respect the required constraints before investing too much time in detailed implementations. WOPANets (Worst Case Performance Analysis of embedded Networks) is a new tool that embodies an analytical approach based on the Network Calculus formalism to perform a system level worst-case performance evaluation and includes optimization analysis to find the optimal design solution that guarantees the system's requirements. This approach would enhance the design process time and costs. Some avionics and space networks are already implemented in WOPANets like AFDX and Spacewire and new models for applications based on multi-cluster embedded networks and wireless technologies are in progress.

A growing number of model-driven development (MDD) advocates are claiming that MDD is a "success". They point to successful applications, particularly in the embedded systems domain, and the results of surveys that show growing use of MDD technologies in industry. As an advocate I would like to concur, but there is strong evidence that this view is an overly optimistic view; there remains significant challenges that must be overcome if MDD is t realize its true potential. In this talk, I discuss some of the challenges related to model tooling and analysis that are friction points in the move towards greater acceptance of MDD in practice.

Nous proposons un domaine abstrait capable d'inférer des invariants vérifiés par des structures de données dynamiques, telles que des listes, vivant à l'intérieur de structures allouées statiquement, telles que des tableaux. Ce style de programmation se retrouve fréquemment dans les programmes embarqués critiques qui ont besoin "d'allouer" des structures dynamiques dans des régions statiques car l'allocation dynamique est interdite dans ce contexte.
Notre domaine abstrait décrit précisément cette hiérarchie de structures. Il combine plusieurs instances de domaines de forme mémoire qui capturent chacun des propriétés de forme mémoire élémentaires, et inclut également un domaine abstrait numérique. Cette modularité simplifie beaucoup la conception et la construction du domaine abstrait global. Une implémentation démontre l'efficacité de l'approche sur un problème tiré d'un code embarqué industriel.

We give an overview of second-order logics including primitive mechanisms to define data types (unary predicates) in a (co)inductive way. These data types are formalized by means of least and greatest fixed points of predicate transformers which are not necessarily monotone (syntactically positive) but are guaranteed to exist by the use of the Mendler-style, which involves a notion of monotonization of an arbitrary operator on a complete lattice. This feature of our logics allows for a direct generalization to nested or heterogeneous (co)inductive predicates useful to implement (co)data types requiring strong invariants, like perfect trees or random access lists.

Cette présentation reprend les travaux développés dans la thèse de Michaël Lauer en les étendant aux systèmes temps réel à priorités fixes communiquant via un réseau à qualité de service garantie. Cet exposé présente :

• la notion de latence de bout en bout
• puis une méthode de calcul de (latence de bout en bout) reposant sur la résolution d'un problème MILP (Mixed Integer Linear Programming problem).

L'exposé s'appuie sur une étude de cas avionique, et le passage à l'échelle de la méthode est montré sur un ensemble d'expériemntations sur cette étude de cas. S'il reste du temps, l'exposé montrera comment la méthode peut être naturellement étendue aux propriétés de "fraicheur" et de "reactivité".

Although theories of equivalence or subtyping for recursive types have been extensively investigated, sophisticated interaction between recursive types and abstract types has gained little attention. The key idea behind type theories for recursive types is to use syntactic contractiveness, meaning every mu-bound variable occurs only under a type constructor such as -> or *. This syntactic contractiveness guarantees the existence of the unique solution of recursive equations and thus has been considered necessary for designing a sound recursive type theory. However, in an advanced type system, such as OCaml, with recursion constructs, type parameters, and abstract types, we cannot easily define the syntactic contractiveness of types.
We investigate a recursive type system with type abbreviations, type parameters, and abstract types. In particular, we show that while non-contractive types may be allowed in the implementation, ones in the signature lead to unsoundness of the type system. We develop a new semantic notion of contractiveness for types and signatures using mixed induction and coinduction, and show our recursive type system is sound with respect to the standard call-by-value operational semantics which eliminates signature sealings. We have also formalized the whole system and its type soundness proof in Coq.
Joint work with Hyeonseung Im and Sungwoo Park.

Software engineering has produced a lot of theories and tools to support the development of safe large scale software. Now building a software and validating it can rely on a lot of formal methods, languages and tools. In the end, a software producer can offer guarantee on its products giving confidence to the user.
But, often, the user experience is not satisfying because the software does not fit well or exhibit bugs in its environment. This is the consequence of the failure to take into account the deployment of software when building them and validating them. Deployment is considered to be a basic task left to system administrator or end user. This was sensible when applications where small, executed in a simple environment and always managed by professionals. But, in our new world, full of new devices and user wanting more and pervasive services, installing, upgrading, removing software require to move from ad-hoc methods and tools to a formal software engineering practice.
In this context, I have been developing projects to adapt formal approaches to the domain of software deployment. In this talk, I will start by clarifying the notion of deployment and rapidly presenting current practice and their limitations. Then, I will give an overview of the work in the domain focusing on two work made at Télécom Bretagne. First, formal management of software dependencies when deploying and second, on how to replace deployment scripts by (verified) programs written on a languages taking into account all the formal contribution of software engineering.

In a context of low computing ressources available and a large variety of HW, on-board softwares for satellites have the same constraints as many other ones in critical systems : reduce costs while covering always more functions with always more mastership of the quality of the development process. After a short presentation on the context of payloads and platform developments, we will present how a spin-in of an IMA-like architecture has been developed to answer to several needs and its perspectives for the near future.

Formal techniques and tools are well established for supporting the design of critical systems. However, they are seldom used by engineers for developing more conventional software. I will present some applications of formal methods to building and verifying distributed, communicating applications. I will present first how process algebraic languages and tools have been successfully applied to the verification of cloud computing protocols. Second, I will show how they can be very helpful in supporting the construction of distributed systems by reusing and composing existing services modelled using interaction protocols or conversations. More precisely, I will present model-based techniques for compatibility checking, adaptor generation, and checking the realizability of choreography specifications.
Bio: Gwen Salaün received a PhD degree in Computer Science from the University of Nantes, France, in 2003. In 2003-2004, he held a post-doctoral position at the University of Rome ``La Sapienza'', Italy. In 2004-2006, he held a second post-doctoral position at Inria Grenoble, France. In 2006-2009, he was a research associate at the University of Malaga, Spain. Since 2009 he is an associate professor at Ensimag, one of the leading engineering schools in applied mathematics, informatics, and telecommunications in France. He was also appointed to an Inria chair in system security and safety in 2009. He is the co-author of about 50 publications in international conferences and journals. His research interests include formal techniques and tools, process algebras, concurrent and distributed systems, specification and verification, software engineering, composition of software components and services.

This talk presents an end-to-end framework for the design and the implementation of real-time systems on a many-core architecture. The framework takes as input a real-time system described in the multi-rate synchronous language Prelude, maps it to the Intel Single-chip Cloud Computer (SCC), and provides a light-weight run-time environment for the execution of real-time tasks on the SCC.
First, the talk gives an overview of the SCC and describes the bare metal framework that forms the basis of our run-time environment. Based on the characteristics of many-core processors, we argue for non-preemptive partitioned scheduling. The talk presents a scheduler implementation that takes into account the imperfect synchronization of local clocks on the SCC and the non-negligible time for communication between cores. Furthermore, the talk presents a heuristic for mapping the task set to the SCC. Apart from schedulability, the heuristic also considers the communication between tasks. The partitioning is checked by a schedulability analysis to ensure its validity. The evaluation shows that the heuristic is effective in generating valid partitionings for several case studies and that the run-time overheads introduced by the framework are reasonably low.

This talk addresses the issue of lemma generation in a k-induction based formal analysis of transition systems, in the linear real/integer arithmetic fragment. A backward analysis, powered by quantifier elimination, is used to output preimages of the negation of the proof objective, viewed as unauthorized states, or \emph{gray states}. Two heuristics are proposed to take advantage of this source of information. First, a thorough exploration of the possible partitionings of the gray state space discovers new relations between state variables, representing potential invariants. Second, an inexact exploration regroups and over approximates disjoint areas of the gray state space, also to discover new relations between state variables. $k$-induction is used to isolate the invariants and check if they strengthen the proof objective.
These heuristics can be used on the first preimage of the backward exploration, and each time a new one is output, refining the information on the gray states. In our context of critical avionics embedded systems, we show that our approach is able to outperform other academic or commercial tools on examples of interest in our application field. The method is introduced and motivated through two main examples, one of which provided by Rockwell Collins, in a collaborative formal verification framework.

Ce séminaire porte sur l'analyse temporelle d'applications organisées et structurées selon des modes. Les modes reflètent différents états du système au cours de son exécution. L'introduction de modes apporte indéniablement des avantages. Par exemple une meilleure gestion du programme ou un raffinement du problèmes d'ordonnancement en restreignant ce dernier à l'examen des tâches d'un seul mode à la fois. En revanche l'introduction des modes nécessite une étude approfondie de ce qui se passe lorsque le système change de mode au cours de son évolution. Le déroulement des changements de mode est décrit dans la littérature par plusieurs protocoles qui définissent les comportements des différentes classes de tâches pendant la période transitoire et qui expriment à quelles conditions ce changement devient réalisable. L'exposé présentera d'abord les protocoles pour schéma d'ordonnancement à priorité fixe dans un contexte monocoeur. Il abordera ensuite les méthodes dites « synchrones » qui interdisent l'exécution simultanée de tâches appartenant à des modes différents lors du changement de mode. Ces méthodes peuvent être utilisées dans un contexte multicoeur ainsi que dans des contextes faisant appel à des schémas d'ordonnancement dynamiques.

L'augmentation de la complexité des systèmes temps-réel répartis embarqués (TR2E) et leur implication dans de nombreux domaines de notre quotidien imposent de nouvelles méthodes de réalisation. Dans les domaines dîts critiques (transport, médecine...) ces systèmes doivent satisfaire des contraintes dures pour garantir leur bon fonctionnement et éviter toutes défaillances qui engendreraient des conséquences financières ou humaines dramatiques.
L'Ingénierie Dirigée par les Modèles (IDM) introduit le ``modèle'' - i.e. une description abstraite du système - et un ensemble d'outils (édition, transformation...) permettant la simplification et l'automatisation des étapes de conception, de validation et de génération du système. Ainsi, différentes abstractions du système sont élaborées dans des formalismes spécifiques de manière à couvrir un aspect du système et à permettre la réutilisation des outils d'analyse et de génération existants. Cependant, ces multiples représentations évoluent à des niveaux d'abstractions différents et il n'est pas toujours évident de mettre en corrélation système analysé et système généré.
Ce travail de thèse exploite les concepts et les mécanismes offerts par l'IDM pour améliorer la fiabilité du processus de réalisation des systèmes critiques basé sur les modèles. L'approche que nous avons définie repose sur la définition du langage de modélisation architecturale et comportementale AADL-HI Ravenscar - un sous-ensemble du langage AADL (Architecture Analysis & Design Language) et de son annexe comportementale - contraint pour permettre conjointement l'analyse et la génération de l'ensemble des composants de l'application y compris de son exécutif, avec une sémantique proche d'un langage de programmation impératif. En effet, les descriptions architecturales permettent d'exprimer l'ensemble des éléments du système à un niveau d'abstraction pertinent pour l'analyse et la génération, mais il est nécessaire de les étendre et de les enrichir avec des descriptions comportementales de manière à expliciter les composants intergiciels de l'application et à réduire les différences sémantiques entre le modèle et le langage de programmation cible.
Nous proposons un nouveau processus de réalisation qui (1) raffine la description architecturale AADL initiale de l'application vers un modèle architecturale et comportementale AADL-HI Ravenscar, (2) génère et intégre automatiquement les composants intergiciels configurés statiquement en fonction des besoins de l'application et (3) analyse et produit automatiquement le code source de l'ensemble des composants constituants l'application et sa plate-forme d'exécution personnalisée. Ce processus est implanté à l'aide de techniques et outils de transformation de modèles facilitant la sélection des raffinements et des règles de transformation en fonction de la plate-forme d'exécution et du langage cible.

The use of formal analysis tools on models or source code often requires the availability of auxiliary invariants about the studied system. Abstract interpretation is currently one of the best approaches to discover useful invariants, especially numerical ones. However, its application is limited by two orthogonal issues:
(i) Developing an abstract interpretation is often non-trivial; each transfer function of the system has to be represented at the abstract level, depending on the abstract domain used;
(ii) With precise but costly abstract domains, the information computed by the abstract interpreter can be used, only once a post fix point has been reached; something that may take a long time for very large system analysis or with delayed widening to improve precision.
This talk presents a new, completely automatic, method to build abstract interpreters. One of its nice features is that its produced interpreters can provide sound invariants of the analyzed system before reaching the end of the post fix point computation, and so act as on the fly invariant generators.

Among precise abstract interpretation methods developed during the last decade, policy iterations is one of the most promising. Despite this efficiency, it has not yet seen a broad usage in static analyzers. We believe the main explanation to this restrictive use, beside the novelty of the technique, lies in its lack of integration in the traditional abstract domain framework. This prevents an easy integration in existing static analyzers based on the classical abstract interpretation framework and collaboration with other, already implemented, abstract domains through reduced product. This work aims at providing a traditional abstract domain interface to policy iterations.
Usage of semi-definite programming to infer quadratic invariants on linear systems is one of the most appealing use of policy iteration. Combined with a template generation heuristic inspired from existing methods from control theory, this gives us a fully automatic tool to infer quadratic invariants on linear systems with guards. Those systems often constitute the core of embedded control systems and are hard, when not impossible, to analyze with traditional linear abstract domains. The method has been implemented and applied to some benchmark systems, giving good results.
On commencera par présenter sur un exemple la méthode d'itération sur les stratégies avant de donner une intuition de la façon dont on l'intègre dans un domain abstrait traditionnel. Finalement, on présentera quelques exemples de génération entièrement automatique d'invariants quadratiques pour des systèmes linéaires à garde.
keywords: abstract interpretation, policy iteration, linear systems with guards, quadratic invariants, ellipsoids, semi-definite programming

Probabilities are effective in both modeling and analyzing embedded systems by increasing the amount of information for the description of elements composing the systems; i.e. tasks and applications needing need resources, schedulers executing tasks, and resource provisioning which satisfy the resource demand. In this seminar, we present a model which condiders component-based real-time systems with component interfaces able to abstract both the functional and non-functional requirements of system components and the whole systems. The model we propose faces probabilities and probabilistic real-time systems unifying in the same framework probabilistic scheduling techniques and compositional guarantees varing from soft to hard real-time. We provide an algebra to work with the probabilistic notation developed and develop analysis in terms of sufficient probabilistic schedulability conditions for task systems with either preemptive fixed-priority or earliest deadline first scheduling paradigms.

La vérification et la validation des systèmes de commande et de guidage des avions modernes exigent la remise en cause des méthodes actuelles (fondées essentiellement sur la simulation et le test du système final), et la prise en compte non seulement des logiciels, mais aussi des modèles ayant servi à développer ces systèmes. Dans cet exposé, nous présenterons deux systèmes : d'une part, un asservissement typique d'avions de ligne et d'autre part, le prototype d'une nouvelle génération de systèmes anti-collision. Dans les deux cas, nous montrerons que l'existence de fonctions "barrières" permettant de borner le comportement de ces systèmes est essentielle à leur vérification et validation. Nous décrirons par ailleurs le prototype d'un environnement d'autocodage de systèmes de contrôle et commande qui implante automatiquement les éléments de preuve de correction qui facilitent grandement la vérification exhaustive de ces systèmes.
Eric Féron est actuellement invité par le RTRA STAE - Sciences et Technologies de l'Aéronautique et l'Espace - dans le cadre du chantier IFSE - Ingénierie Formelle des Systèmes Embarqués - en collaboration avec l'IRIT, le LAAS et l'ONERA.

Automatic memory management, also known as garbage collection, is a suitable means to increase productivity in the development of computer programs. As it helps to avoid common errors in memory management, such as memory leaks or dangling pointers, it also helps to make programs safer. Conventional garbage collection techniques are however not suited for use in hard real-time systems. In the past few years, methods for garbage collection that are suitable for use in hard real-time systems have been developed. This talk presents techniques developed in the course of my PhD thesis to enable hard real-time garbage collection also on chip multi-processor systems.
The talk starts with an overview of the Java Optimized Processor (JOP), which provides the platform for the prototype implementation of the garbage collector. Also, the talk gives a brief introduction to the basic principles of garbage collection. Challenges for real-time garbage collectors and the solutions developed in the scope of my thesis are discussed, with an emphasis on the root scanning phase of garbage collection and the treatment of heap fragmentation. Finally, an experimental evaluation is presented that confirms the theoretic results, which indicate that low release jitter can be achieved in multi-processor systems in the presence of garbage collection.
More information

The group TORRENTS (Time ORiented Reliable Embedded NeTworked Systems) is a cluster that federates the activities related to *time-oriented embedded systems* carried out in research labs in Toulouse (France). It has been set up as a response to the RTRA STAE http://www.fondation-stae.net/ call for «chantiers».
For the second year, the workshop TORRENTS, organised with the financial support of the RTRA STAE, focuses on the executive aspects
All information at http://conf.laas.fr/OPODIS2011/OPODIS/TORRENTS_talks.html.

We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL*, and the corresponding tree-based properties, in the spirit of the modal mu-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of "eventually always blueness" and mixed inductive-coinductive "almost always blueness" and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction).
We have fully formalized our development with the Coq proof assistant.
(Joint work with Marc Bezem and Tarmo Uustalu)

To meet constraints of re-use, variability, complex real-time and limited HW resources, the architecture of an engine management software is split into a static facet defining compilation units (modules, aggregates) and a dynamic (real-time) facet defining execution units (functions, tasks). The dynamic facet is characterized by sequencing and data consistency needs between strongly coupled functions, by a wide range of temporal events (from 1 millisecond to 1 second) mixed with a set of angular events (ie based on engine speed, ie with permanently variable frequency). After a short description of these constraints (which drive futher choices), we will present the means used at Continental to control the schedulability (only one aspect of dynamic architecture) of our systems: specification of the needs, implementation and configuration, verification by measurement, estimation or simulation. We will give a status on the current issues and difficulties, and an outlook on the future developments in this area.

This presentation gives an overview of the Ptides workflow, a model-based design approach for deterministic, event-driven real-time applications. Ptides stands for "Programming Temporally Integrated Distributed Event Systems" and allows for explicit, platform independent specification of functionality and timing. Ptides uses the discrete-event semantics and relates logical (or model time) to physical (or platform time) only at certain points in the model. A simulation environment that allows for execution of Ptides models together with plant models is built into the modeling and simulation tool Ptolemy II. From the specification in the model, code is generated for given target platforms. The generated code includes a lightweight operating system which performs I/O handling and scheduling as well as application specific tasks. Currently, the framework supports code generation for 3 different platforms: a Luminary Micro board, a Renesas board and an XMOS board.

This talk gives an overview of existing concepts for multi- and manycore operating systems from the viewpoint of real-time programming. Using the AUTOSAR standard as an example, it is shown which problems will arise when applying the standard to manycore processors, and how some of these problems can be solved.

In this talk I will present Clousot, an abstract interpretation-based static analyzer to be used as verifier for the CodeContracts. Clousot is routinely used every day by many .NET programmers.
In the first part of the talk I will recall what contracts are (essentially preconditions, postconditions and object invariants), why they are almost universally accepted as good software engineering practice.
Nevertheless, their adoption is very low in practice, mainly for two reasons: (i) they require a non-negligible change in the build environment which very few professional programmers are willing to pay (e.g. a new language or a new or non-standard compiler or poor IDE integration ...); (ii) the static verification tools are either absent or they require far too much help and hugely miss automation.
The CodeContracts API is an answer to (i). Clousot is an answer to (ii).
In the second part of the talk, I will dig deeper into the Clousot architecture, explaining: (i) why unlikely similar tools we decided to base it on abstract interpretation (essentially because of automation, inference power, generality, fine control of the cost/tradeoff ratio ...); and (ii) the new abstract domains (numerical, universal, existential, etc.) we designed and implemented.
The CodeContracts API is part of .NET 4.0. Clousot can be downloaded from the DevLabs: http://msdn.microsoft.com/es-AR/devlabs/dd921949.aspx

Ces travaux portent sur la certification de programmes impératifs. Les certificats établissent la validité des propriétés sémantiques des programmes et sont fournis sous forme depreuves déductives vérifiables par machine (http://en.wikipedia.org/wiki/Computer-assisted_proof). Le défi relevé est d'automatiser la construction des preuves de correction de programmes. Nous avons suivie l'approche de Floyd-Hoare pour prouver que les propriétés sémantiques sont des invariants du programme et nous avons utilisé le système Coq pour vérifier la validité des preuves.
On considère le cas où les propriétés sémantiques sont calculées par des analyseurs statiques (http://fr.wikipedia.org/wiki/Analyse_statique_de_programmes) de programmes qui s'appuient sur la théorie de l'Interprétation abstraite (http://www.di.ens.fr/%7Ecousot/publications.www/Cousot-TSI-00-Hermes-p155-164-2000.pdf). Nous proposons une méthode d'instrumentation des analyseurs statiques de programmes afin de leur faire générer automatiquement un certificat pour chaque propriété sémantique calculée. L'instrumentation consiste à associer à certaines fonctions d'un analyseur statique des patrons de preuve qui à l'exécution généreront les certificats. De tels analyseurs instrumentés ne sont pas pour autant certifiés puisque leur correction pour toutes leurs entrées possibles n'est pas garantie, néanmoins ils sont capables de justifier par une preuve formelle la correction du résultat de chacun de leurs calculs. Bien sûr, si pour une entrée possible l'exécution de l'analyseur est boguée le résultat sera erroné et la justification produite ne sera pas une preuve valide; elle sera rejettée par le vérificateur de preuves (Coq dans notre cas).
Cette approche permet de certifier avec un très haut-niveau de confiance (celui du vérificateur de preuves) les résultats d'outils existants, même à l'état de prototypes. Pour que l'instrumentation soit applicable en pratique, nous avons cherché à limiter le nombre de fonctions à instrumenter. Nous avons dégagé un ensemble restreint de fonctions, commun à tout analyseur, à instrumenter pour qu'un analyseur existant devienne un outil de certification automatique.
Nous avons appliqué cette technique d'instrumentation à un analyseur de programmes manipulant des tableaux (http://mathias.xn--pron-bpa.eu/index.php?menu=2,0,10#pldi08) qui s'appuie sur des domaines abstraits non triviaux. Cet analyseur calcule des propriétés sur le contenu des tableaux manipulés par les programmes et, grâce à notre instrumentation, génère désormais des certificats vérifiables par Coq attestant de la validité des propriétés découvertes par l'analyse statique.

Establishing adequacy of implementations of software transactional memory (STM) is notoriously non-trivial. Above all, it is difficult to determine the desirable notion of correctness and to define it mathematically. But describing an implementation of STM in a form amenable to mathematical scrutiny and proving it correct with respect to the chosen notion of correctness are also subtle and error-prone tasks. In this talk, I describe an experiment in this direction. We defined a particular STM implementation for the While language with parallelism and nested transactions in terms of a transactional small-step semantics, stated Guerraoui and Kapalka's opacity for this implementation in terms of simulability of runs in the transactional semantics by runs in a sequential semantics and vice versa for a suitable notion of agreement between configurations in the two semantics, and proved that it holds. We formalized the whole development in the dependently typed programming language Agda. (Joint work with Andri Saar.)

Avec le projet PROSEU, contrat DGE faisant en principe collaborer laboratoires et industriels français et québécois, nous avons été amenés à nous intéresser à quelque chose qui nous préoccupait moyennement jusqu'à présent (mais un vrai problème, identifié à la fin des années 70): les erreurs transitoires [alias erreurs « soft », alias SEU (Single Event Upsets)], leurs causes, leurs effets, particulièrement dans les systèmes embarqués, et comment s'en protéger avec le meilleur rapport qualité/prix.
C'est à un résumé de notre activité sur ce sujet que sera consacré l'exposé: ce qu'on sait faire actuellement et les idées que nous nous proposons de mettre en oeuvre

Le lambda calcul non typé, créé en 1936 par Alonzo Church, est une théorie très largement utilisée en logique, théorie des types, programmation fonctionnelle, linguistique, etc...
Le théorème de Church-Rosser en particulier fait partie de ses résultats les plus importants et les plus utilisés. Son énoncé est le suivant :
Theorem 1.32 (Church-Rosser theorem for ▹ß)
If P ▹ß M and P ▹ß N, then there exists a term T such that M ▹ß T and N ▹ß T
La plupart des preuves du théorème de Church-Rosser ne prennent pas vraiment en compte les problèmes liés à l'⍺-conversion, le renommage de variables liées au sein d'un terme. Elles définissent en général des classes d'équivalence pour la relation d'⍺-conversion ce qui leur permet de s'affranchir des difficultés naissant du renommage et de la substitution des variables liées. Certains trouvent cela dommage car l'⍺-conversion est une relation extrêmement importante en lambda calcul.
J. Roger Hindley et Jonathan P. Seldin proposent dans leur livre Lambda Calculus and Combinators, an Introduction une preuve gardant l'⍺-conversion du début à la fin. L'idée est de définir une conversion alternative appelée ⍺0-conversion, équivalente à l'⍺-conversion, mais qui leur permet de traiter la substitution plus simplement.
Cependant, lors de sa rencontre avec Makoto Tatsuta le 24 Mai 2010, Hindley lui avoua qu'il n'etait pas certain de l'exactitude de sa preuve. C'est la raison pour laquelle nous nous sommes lancés dans une verification sous Coq, un assistant de preuve développé en collaboration entre l'INRIA, école Polytechnique, Université Paris-Sud 11 et le CNRS, de la preuve de son livre. Notre but était d'avancer le plus possible dans la verification, la durée de mon séjour au NII étant limité.
Avec l'aide de Makoto Tatsuta et de Xavier Thirioux, j'ai tout d'abord défini la structure de notre lambda calcul et prouvé quelques résultats basi- ques sur celle-ci, puis implémenté la substitution de variables accompagnée de quelques autres résultats, pour finir par l'⍺-conversion et ses lemmes nécessaires à la preuve elle-même.

Parmi les outils de vérification utilisés aujourd'hui, les interprètes abstraits jouent un rôle de plus en plus important. Ils reposent sur un représentation abstraite des propriétés des logiciels, les domaines abstraits. Que ce soit dans les cadres industriels critiques où l'on veut avoir confiance dans ces outils, ou dans l'enseignement où l'on veut pouvoir synthétiser totalement ou partiellement des analyseurs pour faire intervenir les élèves, la génération automatique de domaines abstraits finis prend tout son sens. Nous présentons ici notre approche qui génère un domaine abstrait et ses fonctions de transfert sémantique à partir d'une description de la structure de son treillis et d'une fonction de concrétisation. Cette méthode repose sur Camlp4 pour construire un module Caml de type "domaine abstrait" et sur des solveurs SMT pour calculer au mieux les opérations de transfert du domaine.

Data flow languages are high level programming languages commonly used in industry to model and implement reactive embedded systems controlling a vast variety of devices.
We present a general approach for proving automatically safety properties of data flow programs. The approach extends and combines Model Checking with Satisfiability Modulo Theories (SMT) techniques. In it, a given program and property are first translated into formulas belonging to a decidable fragment of first-order logic that includes the combined theory of the program's data types--such as integers, reals, Booleans and so on. Then the property is proved by induction over the length of program executions using as reasoning engine an SMT solver specialized on that theory.
This talk will provide a high level description of the basic approach and its main enhancements as applied to the data flow language Lustre. Among the enhancements, it will then focus on a novel invariant discovery mechanism used by the model checker to strengthen its inductive reasoning steps and increase its success rate in proving safety properties.

Dr. Cesare Tinelli is an associate professor of Computer Science at the University of Iowa. He received a PhD in Computer Science from the University of Illinois at Urbana-Champaign in 1999. His research interests include automated reasoning, formal methods, foundations of programming languages, and applications of logic in computer science.
He is a founder and leader of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for Satisfiability Modulo Theories solvers. He received an NSF CAREER award in 2003 for a project on improving extended static checking of software by means of advanced automated reasoning techniques, and a Haifa Verification Conference award in 2010 his role in building and promoting the SMT community. He has given invited talks at such conferences as CAV, HVC, TABLEAUX, VERIFY, and WoLLIC.
His research has been funded by the US National Science Foundation, the US Air Force Office of Scientific Research and Intel Corp., and has appeared in more than 40 refereed publications, including articles in such journal as Artificial Intelligence, Information and Computation, the Journal of the ACM, Logical Methods in Computer Science, and Theoretical Computer Science.
He is a founder of the SMT workshop and has served in the program committee of numerous automated reasoning conferences and workshops, and in the steering committee of CADE, IJCAR, FTP, FroCoS and SMT. He will be the PC chair of FroCoS'11. He is also an associate editor of the Journal of Automated Reasoning.

Les systèmes réactifs deviennent extrêmement complexes avec l’essor des hautes technologies. Malgré les progrès techniques, la grande taille de ces systèmes facilite l’introduction d’une plus grande gamme d’erreurs. Parmi ces systèmes, les systèmes asynchrones, composés de sous-systèmes communiquant par échange de messages via des files d’attentes (par exemples des protocoles, des systèmes de communication bord/sol. . . ), apportent une complexité encore supérieure.
Actuellement, les industries engagent tous leurs efforts dans le processus de tests et de simulations à des fins de certification. Néanmoins, ces techniques deviennent rapidement inexploitables pour débusquer des erreurs pouvant conduire à des situations catastrophiques. La couverture des jeux de tests s’amincit au fur et à mesure de la complexification des systèmes, et il devient nécessaire d’utiliser de nouvelles méthodes. Parmi celles-ci, les méthodes formelles ont contribué, depuis plusieurs années, à l’apport de solutions rigoureuses et puissantes pour aider les concepteurs à produire des systèmes non défaillants. Dans ce domaine, les techniques de model-checking ont été fortement popularisées grâce à leur faculté d’exécuter, plus ou moins automatiquement, des preuves de propriétés sur des modèles logiciels.
Néanmoins, cette méthode souffre du problème de l’explosion combinatoire. Pour contrer ce phénomène, les méthodes de réduction par ordres-partiels se sont révélées particulièrement efficaces pour éliminer à la volée des séquences de transitions équivalentes de l’automaten global, là où le model checking classique effectuait un parcours exhaustif.
Toutefois, les travaux sur les ordres-partiels issus de la littérature appliquent les méthodes de réduction, lors de la construction de l’automate global composé du système, de son environnement complet ainsi que de la propriété à vérifier. Or, dans la majorité des cas, les propriétés à vérifier correspondent à des cas d’utilisation bien spécifiques et par conséquent la prise en compte de l’environnement complet du système n’est pas nécessaire.
L’approche dans laquelle s’insère ce travail, prend un point de vue complémentaire en considérant la réduction, non plus du système global, mais plutôt de son environnement. En effet, l’idée est d’abord de réduire les comportements du système en décrivant un cas d’utilisation particulier de l’environnement avec lequel le système interagit. L’objectif est de guider le model-checker à concentrer ses efforts, non plus sur l’exploration de l’automate global, mais sur une restriction pertinente de ce dernier pour la vérification. Pour cela, l’environnement (appelé contexte) est déplié et partitionné pour générer un ensemble de scénarios. La vérification effective s’effectue ainsi en composant chaque scénario avec le système et la propriété à vérifier. Sur cette idée, une méthode de description de l’environnement appelée contexte a été développée, pour permettre à l’utilisateur de spécifier, dans un langage simple, le comportement souhaité de son environnement. La description de l’environnement et la décomposition de la vérification, en vérification élémentaire sur chaque scénario, apporte une réduction importante de l’explosion combinatoire en espace.
Néanmoins, dès lors que le nombre d’acteurs (c’est à dire des éléments parallèles ou acteurs de l’environnement) devient important, le nombre de scénarios dépliés peut devenir prohibitif (par exemple, un environnement composé de P acteurs concurrents chacun émettant un message au système, générera P ! scénarios), et par conséquent une explosion combinatoire en temps et non plus en espace. La complexité du processus de vérification n’a pas disparue mais a seulement changé de nature. L’explosion combinatoire qui était de nature spatiale devient, par cette méthode, de nature temporelle.
Pour contrer cette explosion temporelle, nous proposons d’étendre les méthodes de réduction d’ordres partiels et la théorie des traces de Mazurkiewicz de manière à déterminer une équivalence entre les scénarios du contexte afin de supprimer ceux qui ont le même impact sur le système. Nous appliquons la méthode sur des modèles SDL, tout d’abord dans le cas mono processus puis dans le cas multi-processus sur deux cas d’études avioniques industriels. Nous comparons les résultats avec un model-checker performant : SPIN.

Dans cette présentation, nous examinerons les fondements d'une théorie de la conception d'un système embarqué par contrats, à partir d'un ensemble de considérations méthodologiques. Après avoir passé en revue différentes tentatives pour satisfaire ces fondements, nous étudierons les contrats modaux, unification des automates d'interface de de Alfaro/Henzinger et des spécification modales de Larsen, qui offrent toute la flexibilité espérée et supportent, en particulier, le raisonnement compositionnel avec une complexité algorithmique satisfaisante.

Shared decision diagram representations of a state-space have been shown to provide efficient solutions for model-checking of large systems. However, decision diagram manipulation is tricky, as the construction procedure is liable to produce intractable intermediate structures (a.k.a peak effect). The definition of the so-called saturation method has empirically been shown to mostly avoid this peak effect, and allows verification of much larger systems. However, applying this algorithm currently requires deep knowledge of the decision diagram data-structures, of the model or formalism manipulated, and a level of interaction that is not offered by the API of public DD packages.
Hierarchical Set Decision Diagrams (SDD) are decision diagrams in which arcs of the structure are labeled with sets, themselves stored as SDD. This data structure offers an elegant and very efficient way of encoding structured specifications using decision diagram technology. It also offers, through the concept of inductive homomorphisms, unprecedented freedom to the user when defining the transition relation. Finally, with very limited user input, the SDD library is able to optimize evaluation of a transition relation to produce a saturation effect at runtime. We further show that using recursive folding, SDD are able to offer solutions in logarithmic complexity with respect to other DD. We conclude with some performances on well known examples.

Les technologies omniprésentes dans notre environnement intègrent désormais des éléments logiciels facilitant leur utilisation. Ces technologies offrent un vaste laboratoire d’expérimentation pour la recherche et en particulier pour l’informatique appliquée; elles sont un support évident pour rendre des services aux personnes dans leur vie quotidienne. Ces services concernent divers champs d’applications, chacun servant des objectifs spécifiques : confort, sécurité, accès à l’information ou encore assistance à la personne. Puisque les applications offrant ces services sont intimement liées aux besoins des utilisateurs, il est indispensable qu’elles s’adaptent facilement à leurs besoins. Une manière de répondre à ce défi est de proposer à l’utilisateur des outils pour programmer lui-même ses applications. Notre contribution consiste non seulement à définir un tel outil, sous la forme d’un langage visuel paramétré par un champ d’applications, mais aussi à proposer une méthodologie dont l’objectif est de guider un utilisateur dans la programmation d’applications à l’aide de ce langage. Cette méthodologie est dédiée à l’orchestration d’entités communicantes : elles représentent les technologies déployées dans nos environnements. Notre approche, associant une méthodologie à un langage, est accessible à un programmeur novice et suffisamment expressive pour traiter divers champs d’applications. Afin d’augmenter la confiance de l’utilisateur dans le développement de ses applications, nous étendons la méthodologie en proposant une approche de développement dirigée par la vérification de quelques propriétés. Cette vérification est permise par la sémantique du langage, formellement définie.
Mots clés : méthodologie, langages visuels, langages dédiés, accessibilité, assistance à la personne

One of the primary purposes of embedded software and systems is to implement control algorithms aimed at harnessing the dynamics of complex dynamical systems, such as aircraft, automobiles, fast trains and automated transit systems. The necessity to certify these systems makes it a requirement to extract the semantics of the software as it interacts with the physical world. Several tools exist to achieve that goal, and they have displayed excellent performance when applied to large safety-critical software such as that present in avionics systems.
This presentation will be devoted to the contributions that control theory may bring to the extraction of useful control software semantics. It will be shown by means of examples that the process by which such semantics is obtained may be greatly simplified when working with control system specifications first. Numerical issues that arise when moving from the ideal world of system specifications to the concrete software environment will also be discussed. i

First working day on time-oriented embedded systems will be held on November 2, 2010, at ENSEEIHT, Toulouse. Expected invited speakers are Edward A. Lee (U. of California at Berkeley, USA), Wolfgang Pree (U. of Salzburg, Austria) and Jean-Pierre Talpin (IRISA, Rennes, France). All information at http://www.irit.fr/torrents/activities.php.

The Development Assurance Level (DAL) indicates the level of rigor of the development of a software or hardware function of an aircraft. The DAL (ranging from E to A) guides the assurance activities that should be applied at each stage of development. These activities aims at eliminating design and coding errors that would have a safety effect on the aircraft.
The new standard ARP4754a has established rules to allocate the DAL to functions. The allocation is primarly based on the severity of the effects of a function implementation error. But new rules introduce the possibility to downgrade the DAL levels based on various notions of independence (requirement, implementation, execution independence). In the context of the MISSA project we investigate means to assist the safety specialists when checking an existing DAL allocation or generating an allocation.
In this talk we will present our work on the formalization of the DAL allocation rules and its implementation using a pseudo-boolean solver. We will illustrate the talk with various critical aircraft systems including the Electrical Generation and Distribution System.

Model-checking consists in building a formal model of a program, and prove its correctness by checking that the state-space of the model does not contain any bad state. Most programs have infinite state-spaces that must be entirely explored by model-checking algorithms to ensure correctness. This is particularly the case for real-time systems, due to the continuous nature of time.This entails two main problems: the finite representation and the effective computation of infinite sets of states. We present a technique based on Real Vector Automata (RVA) for the representation of state-sets and on acceleration to help the termination of state-space exploration. RVA are weak Büchi automata that we use to encode sets of values definable in Presburger arithmetic over reals and integers. They can particularly represent infinite periodic unions of sets, that we use in turn to capture loop invariants in the model. We show that we can express the iteration of any loop in a timed automaton as a Presburger formula. Following a result of Comon & Jurski on the flatness of timed automata, this yields an algorithm for the computation of the reachability space of timed automata. For linear hybrid automata, we present a technique to compute invariants for ultimately periodic loops. Despite model-checking linear hybrid automata is undecidable, our approach succeeded on many examples found in the literature.

We describe an algebra of Edge-Valued Decision Diagrams (EVMDDs) to encode arithmetic functions and its implementation in a model checking library.
We provide efficient algorithms for manipulating EVMDDs and review the theoretical time complexity of these algorithms for all basic arithmetic and relational operators. We also demonstrate that the time complexity of the generic recursive algorithm for applying a binary operator on EVMDDs is no worse than that of Multi-Terminal Decision Diagrams.
We have implemented a new symbolic model checker with the intention to represent in one formalism the best techniques available at the moment across a spectrum of existing tools.
Compared to the CUDD package, our tool is several orders of magnitude faster.

L'exposé présente une méthode de vérification d'algorithmes manipulant des graphes à l'aide de leur représentation sous la forme d'arbres couvrants décorés de pointeurs additionnels. Nous illustrons ce concept par la vérification d'une version (pseudo-)impérative de l'algorithme de Schorr-Waite, par raffinement d'une version fonctionnelle manipulant des arbres. Ce développement se compose de deux étapes indépendantes:

• le raffinement de l'algorithme fonctionnel en une version impérative, démontré par simulation
• la correction de la version fonctionnelle lors de l'ajout de pointeurs aux arbres qui sont finalement fusionnées pour obtenir le résultat.

De plus, les spécifications impératives utilisent des monades et du sucre syntaxique les rendant très proches d'un programme impératif classique
L'ensemble du travail a été réalisé dans l'assistant de preuve Isabelle/HOL.

Cet exposé présentera les principes de génération de code à partir de modèles AADL, et les fonctionnalités couvertes par Ocarina notre générateur de code. Ocarina est un projet joint entre Télécom ParisTech, l'ISAE et l'ENIS.
AADL est un langage de description d'architectures normalisé par la SAE. La version 2 du langage a été publiée en Janvier 2009. La conception de ce langage vise à fournir les briques de base pour exprimer les éléments fondamentaux de l'architecture en vue de l'analyser. Parallèlement à ces activités, AADL permet aussi de générer de nombreux éléments (tâches, tampons et canaux de communications, tables de routages ..). Tirant partie des informations architecturales, il est possible de générer un code compact, optimisé et conforme aux exigences strictes de qualité de code (Profil Ravenscar et Haute-Intégrité de Ada, ECSS-40 de l'ESA et recommandations liées au langage C). Afin de supporter cette génération de code, Nous avons étendu AADLv2 et dirigé la direction de trois documents annexes clarifiant les patrons de modélisation à utiliser pour garantir que l'on est en mesure de générer du code.
Ocarina est un outil de génération de code basé sur AADL. Il génère du code Ada, C ou Real-Time Java. Le code généré peut s'exécuter aussi bien sur des plates-formes natives qu'embarquées (RTEMS, bare-board, RT-Linux). De plus, il couvre aussi bien des systèmes basés sur RT-POSIX, que des systèmes partitionnés se fondant sur les concept de ARINC653. Il a été validé au travers de plusieurs cas d'étude avec l'ESA, Thales et leurs partenaires.

Un graphe attribué est constitué d'une partie structurelle, et d'attributs qui sont associés aux éléments de la structure. Pour réaliser des transformations de graphes attribués, il faut donc transformer la structure, et réaliser des calculs sur les attributs.
En ce qui concerne la transformation structurelle, il existe deux approches principales: le double pushout et le simple pushout.
Au niveau du calcul sur les attributs, Ehrig a enrichi l'approche double pushout à l'aide d'attributs définis dans le cadre de la théorie des types algébriques. L'approche développée par Ehrig, nécessite de créer des sommets en fonction du nombre de valeurs possibles pour un calcul, ce qui fait que l'implémentation du calcul sur les attributs pose problème et se fait en dehors du cadre formel développé dans sa théorie.
L'approche DPoPb (Double Pushout, Pullback), développée dans la thèse de Maxime Rebout offre un cadre théorique unique qui contient la réécriture de la partie structurelle des graphes et les calculs sur les attributs du graphe. Les espaces des attributs sont des types inductifs, et le calcul sur les attributs se fait à l'aide de moyens qui sont assurés par la théorie des types inductifs. En plus d'avoir un formalisme unique pour la transformation de la structure et des attributs, la puissance de calcul des types inductifs est supérieure à celle des types algébriques car on peut avoir des fonctions comme arguments.
Nos travaux actuels se concentrent sur le calcul sur les attributs: nous étudions comment traiter le calcul des attributs à l'aide des types inductifs, également dans l'approche simple pushout pour comparer avec l'autre approche (Double Pushout) que nous avons déjà étudiée.
De plus, les types inductifs permettent de représenter l'infini d'une certaine manière (par exemple des arbres aux branchements infinis). Il est également possible de faire passer de l'information des attributs, à la structure du graphe. Ce qui nous donne une piste pour représenter un graphe dont la structure a une taille infinie.
La dernière partie de l'exposé est consacrée au côté algorithmique et aux questions d'implémentation de réécriture de graphes par l'approche DPoPb.

L'exposé passe en revue les différentes méthodes de vérification modèle checking borné et non borné basées SAT/SMT ayant diffusé avec succès dans l'industrie dans les années récentes (induction, interpolation), et introduit quelques unes des tendances futures.

Le model checking utilise l'équivalence entre la définissabilité d'un langage de mots par une formule de la logique monadique du deuxième ordre (MSOL) et sa reconnaissabilité par un automate fini ("Théorème de Buchi").
Cette logique permet d'exprimer la plupart des logiques temporelles usuelles. Les applications d'aujourd'hui étant principalement distribuées, on voit l'utilité de caractériser MSOL pour des langages d'ordres partiels étiquetés (LPO), qui sont un modèle plus expressif et fidèle de leurs comportements. Des propriétés analogues au theorème de Buchi ont été prouvées pour des classes restreintes de LPO, telles que les traces de Mazurkiewicz ou les MSC (qui sont la version formelle des diagrammes de séquences d'UML).
Dans cette présentation, nous considérons les systèmes de transition par pas avec autoconcurrence (Step Transition Systems), et définissons une sémantique par langages de LPO qui constitue une extention des sémantiques concurrentes usuelles des Réseaux de Petri. Nous mettons en évidence plusieurs caractérisations de la définissabilité par MSOL de ces langages en termes de régularité, caractérisations qui étendent nombre des résultats mentionnés ci-dessus.
Nous montrons comment ces résultats s'appliquent en particuliers aux langages concurrents des réseaux de Petri.
(travail commun avec Rémi Morin du Lif, en partie publié à PN 2009)

This talk, to be held in english, will get into the g(l)ory details of MLF: introducing MLF new types, their interpretation, the type instance relation, typing rules, type-inference algorithm, unification algorithm, and so on, as long as the audience can bear it.

Les logiques de description (LD) forment une famille de langages adaptés pour la représentation et le raisonnement sur des connaissances d'un domaine d'application d'une façon structurée et formelle. Les outils de représentation et de raisonnement sur des connaissances est actuellement l'un des champs d'application des méthodes formelles, dont l'objectif est d'assurer leur fiabilité. Un point essentiel de l'application de ces méthodes formelles est la preuve de validité des raisonnements dans des LDs, comme celle de la terminaison, l'adéquation (soundness) et la complétude d'un raisonneur. Dans cet exposé , on présente une spécification formelle de la syntaxe et de la sémantique de ALC, qui est considérée comme un représentant typique d'une large gamme de LDs. On prouve pour cette logique les propriétés d'adéquation, de complétude et de terminaison dans l'assistant de preuve Coq.

The talk generalises a famous result from game theory. It presents one proof and sketches three alternative ones.
In a game from game theory, a Nash equilibrium (NE) is a combination of one strategy per agent such that no agent can increase his payoff by unilaterally changing his strategy. Kuhn proved that all (tree-like) sequential games have NE. Osborne and Rubinstein abstracted over these games and Kuhn's result: they proved a *sufficient* condition on agent *preferences* for all games to have NE. I will present a *necessary and sufficient* condition, thus accounting for the game-theoretic frameworks that were left aside. The proof is *formalised* using Coq, and contrary to usual game theory it adopts an inductive approach to trees for definitions and proofs. By rephrasing a few game-theoretic concepts, by ignoring useless ones, and by characterising the proof-theoretic strength of Kuhn's/Osborne and Rubinstein's development, the talk also intends to clarifies sequential game theory.
Then I will sketch an alternative proof. Both proofs so far pre-process the preferences by topological sorting, which is surprising since it decreases the number of NE. Finally I will sketch two other proofs that pre-process the preferences only by transitive closure. The four proofs are all constructive and by induction, and I will compare them when seen as algorithms. The four proofs also constitute diverse viewpoints on the same concepts, the trial of diverse techniques against the same problem, and reusable techniques for similar structures.

For the call-by-name restriction of Curien and Herbelin's lambda-bar-mu-mu-tilde calculus - a calculus for the study of the computational behaviour of classical proofs, an alternative proof of termination of all computations is given in a very syntactic (and hence elementary) way, namely by simulation of all steps in simply-typed lambda calculus. First, the calculus is embedded into a new monadic extension of Parigot's lambda-mu calculus by way of a monadic translation. The new calculus is in turn embedded into simply-typed lambda calculus by a CPS (continuation-passing style) translation. This is joint work with Espírito Santo and Pinto in Braga (Portugal).

Type systems are designed to guarantee that typable programs are safely executed. Therefore it is expected that we can automatically check whether a program is typable or not, and such a problem is called type-inference problem (or typability problem) of type systems. The type-checking problem is another type-related problem: does a program have a given type or not? The type inference is known to be decidable in both the simply-typed lambda calculus and the type system of ML, and the problems in the impredicative polymorphic lambda calculi have been studied. On the other hand, the problems for existential types have not been studied enough. In this talk, some recent results on type-related problems for polymorphic and existential types are presented. In particular, the undecidability for the domain-free lambda calculus with existential types, which was proved by the speaker, is presented. The proof gives a new theoretical application of the continuation-passing-style (CPS) translations.

This presentation comes as a positive reaction inspired by Ralph Matthes' presentation of May, 19. This notably dealt with termination proofs for the simply-typed lambda-calculus augmented with new reduction rules. My presentation will sum up results published in Mathematical Structures in Computer Science, Volume 18, Special Issue 04, August 2008.
A common way to show the termination of the union of two abstract reduction systems, provided both systems terminate, is to prove they enjoy a specific property (some sort of “commutation” for instance). This specific property is actually used to show that, for the union not to terminate, one out of both systems must itself be non-terminating, which leads to a contradiction. One nice feature of such a proof technique is that it often relies on simple diagram chasing.
Sometimes, however, these proofs will not work because there are some cases where the objects (whatever they may be: terms, trees, graphs, or so) are too complex for the diagrams to be closed. On the other hand, there are situations such that if the object at the root of the diagram satisfied some condition, the diagram in question could be closed.
Thus, I will define an operator transforming an infinite reduction sequence into another one by inserting a given reduction step at the beginning of the sequence. Then I will give an example of how it may be used to derive a new lemma ensuring that the union of two reduction systems is terminating. Finally, I will apply this lemma to two case studies.

Les langages de programmation comme OCaml et Haskell reposent sur des règles de typage garantissant la bonne exécution des programmes. En pratique, le typage permet de détecter maintes erreurs de programmation à la compilation. Depuis vingt ans, de nombreux travaux visent à enrichir ces sytèmes de types avec le polymorphisme de première classe (i.e. en ajoutant le quantificateur universel "pour tout"). Le référentiel pour le polymorphisme a été défini en 1972 dans le domaine de la logique : c'est le Système F (Girard). Mais en pratique, le Système F est inutilisable comme langage de programmation, à la différence de OCaml ou Haskell. De plus, l'adaptation naïve du Système F à ces langages rend le typage indécidable.
Dans cet exposé, nous détaillons intuitivement le problème en expliquant pourquoi les solutions proposées jusqu'à présent ne sont pas satisfaisantes. Nous présentons ensuite MLF, un système de types qui répond aux exigences posées, puis nous illustrons avec des graphes l'algorithme d'unification de MLF.

Nous présentons tout d'abord le projet CAVALE (Combinaison d'Analyses pour la VALidation de Logiciels Embarqués). Cette composition doit permettre d'obtenir une meilleure connaissance du système que chacune des analyses prises séparément.
Ce projet a pour objectif:
1) de proposer un cadre permettant la composition d'analyses statiques, (interprétation abstraite, méthode déductive, ...) et de techniques de test dynamique (méthode de construction, critère de couverture, ...) pour un programme C embarqué, découpé en lots fonctionnels ;
2) de réaliser un prototype s'intégrant dans la plateforme Frama-C.
Puis nous présentons un état de l'art des travaux récents dans le domaine, ainsi que nos propres pistes de réflexion, permettant la composition d'analyses avant ou arrière, symboliques (exactes) ou approchées, par plus petits ou plus grands points fixes le cas échéant.

Cet exposé rappelle la traduction CPS pour le lambda-calcul simplement typé et son intérêt, la comparaison avec la variante "colon translation" de Plotkin et sa généralisation aux monades par Wadler. Une variante "continuation-and-garbage-passing style" par Ikeda et Nakazawa est étudiée pour le cas d'un lambda-calcul avec application généralisée qui illustre les problèmes de calculs pour la recherche de preuves. La troisième partie montre une extension vers un calcul de la logique classique de Curien et Herbelin pour lequel une simulation dans le lambda-calcul simplement typé est obtenu par une traduction monadique vers une nouvelle extension monadique du lambda-mu-calcul de Parigot, suivi par une traduction CPS. Tous les résultats qui ne sont pas "classiques" ont été obtenus en collaboration avec Espírito Santo et Pinto à Braga en Portugal depuis octobre 2006.

Coccinelle est un outil qui permet de faire de la reconnaissance de motifs et de la transformation sur du code C. Développé à l'origine pour pallier le problème de l'évolution collatérale dans les pilotes du noyau linux, il est aussi utilisé pour détecter et corriger des bugs. Les motifs à reconnaître sont traduits en formules de logique temporelle, et interprétés sur le graphe de flot de contrôle du programme C. La reconnaissance de motifs correspond alors à la détection des noeuds du graphe de flot de contrôle qui satisfont la formule correspondante (par un algorithme de model checking).
Nous présenterons le langage qui permet de spécifier les motifs et les transformations de code, ainsi que la logique temporelle sous-jacente.

Nous décrivons la formalisation d'un langage synchrone (du style de Signal) dans l'assistant de preuve Isabelle. Dans cet exposé, nous nous intéressons au calcul d'horloge et à la question de "type soundness" de ce langage. Les langages synchrones sont basés sur l'hypothèse que les calculs d'un programme synchrone sont exécutés à des instants spécifiques, comme déterminé par les horloges des signaux manipulés par le programme. Un système de type d'horloge doit assurer que le programme ne traite pas de données invalides. Dans l'exposé,

• nous décrivons un système de types, qui est essentiellement un système d'équations ensemblistes
• nous montrons un résultat de "type soundness" qui assure que, si le système d'équations dérivé d'un programme est valide, alors "tout va bien" dans l'exécution du programme
• nous nous intéressons à la question de solvabilité d'un tel système d'équations (donc à une notion algorithmique, contrairement à la notion sémantique de validité).