Séminaire vérification de Toulouse

We present a component algebra and an associated logic for heterogenous timed systems that can be interconnected at run time. The components of the algebra are asynchronous networks of processes, where processes are sets of traces that model the behaviour of the software applications or devices that are interconnected and execute according to the clock granularity of the network node in which they are placed. The advantage of a trace-based model is that it abstracts from the specificities of the different classes of automata that can be chosen as models of implementations and characterises at a higher level the topological properties of the languages generated by such automata that support several compositionality results; in the paper, such properties are supported by a new time refinement relation and its related closure operator. The main novelty and contribution of our theory lies in the fact that we do not assume that all network nodes have the same clock granularity and that interconnections can be established, at runtime, among nodes with different clock granularities. We investigate conditions under which the interconnected processes can communicate and make progress, generating a collective non-empty behaviour, i.e., conditions that ensure that the interconnection is consistent. Those conditions can be verified at design time, thus allowing that systems can be interconnected at runtime without further checking for compatibility; to the best of our knowledge, no other component algebra has been put forward for timed heterogeneous systems that does not require a-priory knowledge of their structure. Finally, we propose a logic that can support specifications for this component algebra and prove associated compositionality results.

Contracts are an effective way to establish boundaries between components and can be used efficiently to verify global properties by using compositional reasoning techniques. A contract specifies the assumptions a component makes on its context and the guarantees it provides. Requirements in the specification of a component are often case-based, with each case describing what the component should do depending on a specific situation (or mode) the component is in. This talk introduces CoCoSpec, a mode-aware assume-guarantee-based contract language for embedded systems built as an extension of the Lustre language. CoCoSpec lets users specify mode behavior directly, instead of encoding it as conditional guarantees, thus preventing a loss of mode-specific information. Mode-aware model checkers supporting CoCoSpec can increase the effectiveness of the compositional analysis techniques found in assume-guarantee frameworks and improve scalability. Such tools can also produce much better feedback during the verification process, as well as valuable qualitative information on the contract itself. I will presents the CoCoSpec language and illustrate the benefits of mode-aware model-checking on a case study involving a flight-critical avionics system. The evaluation uses Kind 2, a collaborative, parallel, SMT-based model checker developed at the University of Iowa that provides full support for CoCospec.

The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in safety critical roles. There is a considerable body of mathematical proofs on on-line optimization programs which can be leveraged to assist in the development and verification of their implementation. To demonstrate this we built an autocoder which generates a C implementation of an interior point algorithm solving a specific linear problem given as input to the autocoder. This autocoder will not only generate C code but also the proof of its correctness as ACSL annotation that can be checked by Frama-C, SMT solver and PVS.

State-of-the-art (semi-)decision procedures for non-linear arithmetic address polynomial inequalities by mean of symbolic methods, such as quantifier elimination. Although (some of) these methods offer nice completeness properties, their high complexity remains a limit, despite the impressive efficiency of modern implementations. This appears, for instance, to be an obstacle to the use of SMT solvers for the verification of functional properties of control-command programs.
We offer an alternative method that uses off-the-shelf numerical optimization solvers. These solvers only deliver approximate solutions and cannot be trusted due to the algorithms they implement. Nonetheless, while this prevents the completeness of our approach, its soundness is guaranteed by an efficient a-posteriori validation method. Our early prototype implemented in the Alt-Ergo SMT solver already gives some impressive results, particularly on control-command programs.

The verification of floating-point mathematical libraries requires computing numerical bounds on approximation errors. Due to the tightness of these bounds and the peculiar structure of approximation errors, such a verification is out of the reach of generic tools such as computer algebra systems. In fact, the inherent difficulty of computing such bounds often mandates a formal proof of them.
In this talk I will present the CoqInterval library [1], which offers tactics to automatically and formally prove bounds on univariate expressions involving elementary functions in the Coq proof environment. These tactics build upon a formalization of floating-point arithmetic, interval arithmetic, and Taylor models. All the computations are performed inside Coq's logic, relying on the reflection paradigm.
I will also present some experimental results for comparing the performance of our tactic with various existing tools dedicated to the proof of inequalities over the reals.
[1] http://coq-interval.gforge.inria.fr/

We present a novel modeling and programming language which aims at more simplicity, more intuitive programming, quicker turnaround time and real-time predictability by leveraging the use of model-interpretation and providing the language abstractions needed to argue about the timing correctness on a high-level. A MDD flow is built around this language called the Cyber-Physical Action Language (CPAL). In this presentation, we report on the lessons learned during the design and implementation of the CPAL language and the associated run-time environment. We then explain and illustrate the concept of timing correctness that is implemented in CPAL with respect to synchronous approaches. Finally, we discuss the envisioned programming model where the developer states the permissible timing behavior, and a system synthesis step involving both analysis and optimization generates a scheduling solution which at run-time is enforced by the execution environment. CPAL and associated tools are jointly developed by our research group at the University of Luxembourg and the company RTaW since 2012. The CPAL documentation, graphical editor and execution engine for several platforms are freely available at http://www.designcps.com

Probability distributions bring flexibility as well as accuracy in modeling and analyzing real-time systems. On the other end, the adding of probabilities increases the complexity of the scheduling problem, especially in case of mixed-criticalities where tasks of different criticalities have to be taken into account on the same computing platform. In this work we explore the flexibility of probabilistic distributions applied to mixed-critical task sets for defining the probabilistic space of Worst Case Execution Time and evaluating the effects of changes on the task execution conditions. Finally, we start formalizing and making use of probabilistic sensitivity analysis for evaluating mixed-critical scheduling performance.

Floating-point arithmetic is a very efficient solution to perform computations in the real field. However, it induces rounding errors making results computed in floating-point differ from what would be computed with reals. This can be an issue, particularly if one wants to use it to perform proofs. Although numerical analysis gives tools to bound such differences, the proofs involved can be painful, hence error prone. We thus investigate the ability of a proof assistant like Coq to mechanically check such proofs.
In this talk, a brief introduction to floating point roundings and to the proof assistant Coq will be given followed by an overview of the results. No prior knowledge of neither Coq nor floating-point arithmetic is expected.
Eventually, a last part of the talk will present a potential application to the validation of approximate results of polynomial sum of squares optimization problems. This can be used in static analysis to validate polynomial loop invariants for programs with polynomial assignments.

Most software verification tools can be classified into one of a number of established families, each of which has their own focus and strengths. For example, concrete counterexample generation in model checking, invariant inference in abstract interpretation and completeness via annotation for deductive verification. This creates a significant and fundamental usability problem as users may have to learn and use one technique to find potential problems but then need an entirely different one to show that they have been fixed. We present a single, unified algorithm kIkI, which subsumes abstract interpretation, bounded model checking and k-induction. This not only combines the strengths of these techniques but allows them to interact and reinforce each other, giving a `single-tool' approach to verification. We have implemented the algorithm in an analysis tool for C programs, 2LS, exploiting synthesis-based program analysis techniques.

Modeling languages for hybrid systems are cornerstones of embedded systems development in which software interacts with a physical environment. Sequential code generation from such languages is important for simulation efficiency and for producing code for embedded targets. Despite being routinely used in industrial compilers, code generation is rarely, if ever, described in full detail, much less formalized. Yet formalization is an essential step in building trustable compilers for critical embedded software development.
This talk will present a novel approach for generating code for a hybrid systems modeling language that combine synchronous SCADE-like programming constructs and ordinary differential equations (ODEs). By building on top of an existing synchronous language and compiler, it reuses almost all the existing infrastructure with only a few modifications. The versatility of the approach is exhibited by treating two classical simulation targets: code that complies with the FMI standard and code directly linked with an off-the-shelf numerical solver (Sundials CVODE).
The presented material has been implemented in the Zélus compiler and the industrial KCG code generator of SCADE 6.

Nous nous intéressons à des problèmes abordés dans la gestion du trafic aérien, en particulier l'évitement de conflits d'aéronefs, qui surviennent lorsque deux aéronefs sont trop proches l'un de l'autre, à savoir, lorsque leurs distances horizontales et verticales sont inférieures aux distances de sécurité. L'optimisation non-linéaire mixte en nombres entiers (MINLP) se pose naturellement dans la formulation de ce type de problèmes, où la nécessité de modéliser des choix logiques suggère la présence simultanée des variables discrètes ainsi que continues, et les contraintes non-linéaires résultent de la modélisation de la condition de séparation des aéronefs. Nous présentons un aperçu de quelques contributions récentes en termes de modélisation et approches de résolution, issues de MINLP, obtenues dans le contexte du projet ANR "ATOMIC".

We consider First-Order Linear Temporal Logic (FO-LTL) over linear time. We focus on finding models with finite first-order domains for FO-LTL formulas. More precisely, we investigate the complexity of the following problem: given a formula phi and an integer n, is there a model of phi with domain of cardinality at most n? We show that depending on the logic considered (FO or FO-LTL) and on the precise encoding of the problem, the problem is either NP-complete, NEXPTIME-complete, PSPACE-complete or NEXPSPACE-complete. In a second part, we exhibit cases where the Finite Model Property can be lifted from fragments of FO to their FO-LTL extension.

Safety critical systems or applications must satisfy safety requirements ensuring that catastrophic consequences of combined component failures are avoided or kept below a satisfying probability threshold. Therefore, designers must define a hardened architecture (or implementation) of each application, which fulfills the required level of safety by integrating redundancy and safety mechanisms. We propose a methodology which, given the nominal functional architecture, uses constraint solving to select automatically a subset of system components to update and appropriate safety patterns to apply to meet safety requirements. The proposed ideas are illustrated on an avionics flight contoller case study.

Floating-point arithmetic is a very efficient solution to perform computations in the real field. However, it induces rounding errors making results computed in floating-point differ from what would be computed with reals. Although numerical analysis gives tools to bound such differences, the proofs involved can be painful, hence error prone. We thus investigate the ability of a proof assistant like Coq to mechanically check such proofs. We demonstrate two different results involving matrices, which are pervasive among numerical algorithms, and show that a large part of the development effort can be shared between them. In this talk, a brief introduction to floating point roundings and to the proof assistant Coq will be given followed by an overview of the results.

Dans cet exposé, je vais étudier les automates probabilistes sur mots finis. C'est une extension des automates classiques, où les transitions sont déterminées par une loi probabiliste. Ce modèle est très expressif, et le prix à payer pour cette expressivité est que beaucoup de questions naturelles sont indécidables. L'objectif de cet exposé est de montrer que néanmoins, on peut construire des algorithmes algébriques, manipulant des ensembles de matrices, pour résoudre partiellement certains problèmes naturels (équivalence, vide, approximation de la valeur). Je présenterai à la fois des résultats théoriques et des compte-rendus d'expérimentations.

Dans cette présentation, nous décrirons comment nous pouvons approcher de manière sûre l'ensemble des valeurs atteignables d'un système dynamique à temps discret et affine par morceaux en exhibant une fonction de Lyapunov quadratique par morceaux. La technique développée est une adaptation des travaux de Rantzer et Johansson sur l'étude de la stabilité des systèmes dynamiques affines par morceaux aux problèmes d'invariance. Nous appliquerons cette méthode à l'approximation des valeurs prises par les variables d'un programme numérique de type contrôle/commande composé d'une boucle "while" dont le corps contient des branchements conditionnels imbriqués.

Integrating robotic systems into our everyday life needs that we prove that they will not endanger people, i.e. that they will behave correctly with respect to some safety rules. In this paper, we propose a validation toolchain based on a Domain Specific Language. This DSL allows to model the software architecture of a robot using a component-based approach. From these models, we provide tools to generate deployable components, as well as a two-step validation phase. This validation first performs a real-time analysis of the component architecture, leading to an evaluation of the software architecture schedulability. Then we can check the validity of some behavioral property on the components.

Model finders are very useful to tackle many software engineering problems. Kodkod is one of the most popular, due to its support for relational logic (a combination of first order logic with relational operators and transitive closure) and partial instances (allowing the specification of a priori exact, but potentially partial, knowledge about a problem's solution). The most well-known application of Kodkod is the automated analysis of specifications written in Alloy. However, in some software engineering problems, such as model repair, knowledge about the solution is not exact, but instead there is a known target (for example, the current faulty model that must be repaired) that the solver should approximate. In this talk I will first present an extension to Kodkod's partial instances to allow the specification of such targets, and show how its model finding procedure can be adapted to support them.
I will then present two applications of this target oriented relational model finder: Echo (http://haslab.github.io/echo/), an EMF compliant tool for model repair and bidirectional model transformations (with support for OCL, QVT-R, and ATL), that is able to both check and recover, through minimal updates, both intra- and inter-model consistency; and an extension to the Alloy Analyzer with support for sophisticated scenario exploration operations, namely to allow the user to quickly explore very similar (or different) satisfiable instances, by attaching preferences to model elements.

In this talk, I will present Cubicle, a new model checker for verifying safety properties of parameterized systems.
Cubicle is an implementation of the MCMT (Model Checking Modulo Theories) framework for array-based systems, a syntactically restricted class of parameterized transition systems with states represented as arrays indexed by an arbitrary number of processes.
While rudimentary at the moment, Cubicle's input language is sufficiently expressive for describing typical parameterized systems such as cache coherence protocols, fault-tolerant protocols and mutual exclusion algorithms.
Cubicle's implementation is based on a parallel symbolic backward reachability procedure using Satisfiabilty Modulo Theories. Its SMT solver is a tightly integrated, lightweight and enhanced version of Alt-Ergo and its parallel implementation relies on the Functory library.

Les systèmes informatiques embarqués agissent sur leur environnement en calculant des ordres de commandes à partir de données d'entrée produites par des capteurs. C'est le cas notamment des systèmes de contrôle commande. Les ordres calculés et les entrées reçues sont calculés dans des unités physiques données. Ces unités font partie de la spécification du système : par exemple des mêtres, des secondes, ou des mêtres par seconde... Or curieusement ces unités n'apparaissent pas dans les modèles Simulink ou SCADE, et encore moins dans le code généré à partir de ces modèles. L'information de dimension est en quelque sorte perdue lors de la modélisation. La question est alors de savoir pourquoi ? Y a t-il une difficulté technique à annoter les modèles par les unités physiques ? Le but de l'exposé et de répondre à cette question, et prenant comme langage de modélisation le langage Lustre. La réponse est que l'enrichissement apporté au langage pour supporter les unités physique est très simple, et que l'exploitation de ces unités repose sur un système d'inférence de type également très simple. Bref, aucune difficulté. Remarque : exposé déjà donné à AFADL 2014 en juin dernier au CNAM à Paris.

La classe des langages réguliers présente un bon compromis entre expressivité et complexité: elle est close par de nombreuses opérations, et la plupart des problèmes naturels que l'on peut poser sont décidables. Ces avantages proviennent du fait que les langages réguliers sont définissables par plusieurs formalismes équivalents: automates (déterministes ou pas), expressions régulières, logiques, algèbre... Je détaillerai notamment l'avantage de l'approche algébrique pour les questions de décidabilité. Finalement, je présenterai certains problèmes de décidabilité qui sont difficiles à appréhender par les méthodes traditionnelles (la hauteur d'étoile est l'exemple le plus célèbre) et un aperçu des techniques qui ont permis de les résoudre.

In this talk, I will give an overview of the safety verification of the Transport Class Model (TCM). The TCM is a Simulink model of a modern transport-class aircraft simulation for controls and health management system. The simulator is meant to model a mid-size, twin-engine, commercial transport class aircraft. The verification effort involved several stages: formalizing and disambiguating requirements in collaboration with domain experts; processing models for their use by verification tools; applying compositional techniques at the architectural and component level to scale verification; and combining the results of these efforts to construct a safety case.
Among the lessons that we learned is that close collaboration between verification and domain experts is crucial in formalizing requirements and in particular assumptions about the physical system, without which verification cannot be completed. Compositional verification is also key to constructing scalable and meaningful proofs for this complex system and domain. Finally, safety cases are very useful in organizing the system requirements, driving verification efforts, and documenting verification results in a systematic fashion for certification.

La norme IEEE 754-2008 pour l'arithmétique en virgule flottante (VF) recommande d'implanter les fonctions élémentaires (exp, sin, arctan, etc) avec arrondi correct. Mais pour que ces implantations soient efficaces et fiables, il faut résoudre ce qu'on appelle le dilemme du fabricant de tables (Table Maker's Dilemma en anglais) pour chaque fonction considérée. Les algorithmes Lefèvre et Stehlé-Lefèvre-Zimmermann (SLZ) ont été conçus pour résoudre ce problème. Mais les calculs correspondants sont très longs (plusieurs années de temps CPU) et sont effectuées en utilisant des implantations fortement optimisées d'algorithmes complexes : cela jette inévitablement le doute sur l'exactitude des résultats de ces algorithmes. D'où la nécessité d'utiliser des outils formels tels que l'assistant de preuve Coq, pour fournir des garanties fortes sur les résultats obtenus. Je présenterai les travaux réalisés dans cadre du projet TaMaDi, avec un accent particulier sur la certification de l'algorithme SLZ. Je présenterai la méthodologie utilisée et les bibliothèques CoqHensel et CoqApprox qui ont ét é développés dans ce but.

Nous étudions le formalisme des Message Sequence Charts enrichi par des compteurs. Nous rappelons commen t ces spécifications peuvent être décrites et vérifiées formellement à l'aide de réseaux de Petri. Nous montrons qu'effectivement l'ajout de compteurs conduits plusieurs problèmes élémentaires de vérifications d e la classe NP-difficile à la classe EXPSPACE-difficile.

We formalize a unified framework for verified decision procedures for regular expression equivalence. Five recently published formalizations of such decision procedures (three based on derivatives, two on marked regular expressions) can be obtained as instances of the framework. We discover that the two approaches based on marked regular expressions, which were previously thought to be the same, are different, and we prove a quotient relation between the automata produced by them. The common framework makes it possible to compare the performance of the different decision procedures in a meaningful way.

The on-going transformation from the current US Air Traffic System (ATS) to the Next Generation Air Traffic System (NextGen) will force the introduction of new automated systems and most likely will cause automation to migrate from ground to air. This will yield new function allocations between humans and automation and therefore change the roles and responsibilities in the ATS. Yet, safety in NextGen is required to be at least as good as in the current system. We therefore need techniques to evaluate the safety of the interactions between humans and automation. Current human factor studies and simulation-based techniques fall short in front of the ATS complexity, and we need to add more automated techniques to simulations, such as model checking, which offers exhaustive coverage of the non-deterministic behaviors in nominal and off-nominal scenarios.
At NASA we have developed a verification approach based both on simulations and on model checking for evaluating the roles and responsibilities of humans and automation. Models are created using Brahms (a multi-agent framework) and we show that the traditional Brahms simulations can be integrated with automated exploration techniques based on model checking, thus offering a complete exploration of the behavioral space of the scenario. Our framework takes as input a Brahms model along with a Java implementation of its semantics. We then use Java PathFinder developed at NASA Ames to explore all possible behaviors of the model and, also, produce a generalized intermediate representation that encodes these behaviors. The intermediate representation is automatically transformed to the input language of mainstream model checkers, including PRISM, SPIN, and NuSMV allowing us to check different types of properties. We validate our approach on a model that contains key elements from the Air France Flight 447 accident and the Uberlingen accident.
Bio : Dr. Neha Rungta is a Research Scientist at the NASA Ames Research Center located in California. Dr. Rungta’s research interests are in software model checking, verification of multi-agent systems for aviation safety, requirements analysis, and automated program analysis. In the past 10 years, Dr. Rungta’s work has been geared toward developing verification techniques for automated test case generation, detection of subtle concurrency errors, incremental program analysis, and verification of multi-agent systems. Dr. Rungta has published in several leading software engineering peer-reviewed conferences such as ICSE (International Conference on Software Engineering), ISSTA (International Symposium on Software Testing and Analysis), and ASE (International Conference on Automated Software Engineering), multi-agent system conferences such as AAMAS (International Conference on Autonomous Agents and Multi-agent Systems), as well as leading CS journals. She has chaired conferences such as the NASA Formal Methods (NFM) and the SPIN symposium on software model checking.

Le problème auquel nous nous intéressons est l'aide à la localisation d'erreurs dans un programme impératif avec des instructions numériques lorsqu'on dispose d'un contre-exemple qui viole une assertion. L'objectif étant d'identifier des instructions du programme qui sont susceptibles d'être à l'origine de l'erreur. Pour cela nous présenterons d'abord les principaux algorithmes pour le calcul de MUS /IIS (Minimal Unsatisfiable Subset / Irreducible infeasible subset), MSS (Maximal Satisfiable Subset) et MCS (Minimal Correction Set) dans un système de contraintes. Nous présenterons aussi des résultats expérimentaux préliminaires sur un ensemble de benchmarks académiques.

In this talk, we present an alternative method to Kleene iteration to compute fixed point in abstract interpretation. Indeed, the fixed point equations which appear in asbtract interpretation can be understood as value computation in dynamic programming operators. The latter fact allows us to use fixed point computation method from game theory such as Policy iteration. First we illustrate Policy Iteration with intervals domains and then show its generalisation in finite templates domain thanks to constrained optimisation.

This talk presents a formalization in higher-order logic of a generic algorithm that is used in automated strategies for solving global optimization problems. It is a generalization of numerical branch and bound algorithms that compute the minimum of a function on a given domain by recursively dividing the domain and computing estimates for the range of the function on each sub-domain. The correctness statement of the algorithm has been proved in the Prototype Verification System (PVS) theorem prover. This algorithm can be instantiated with specific functions for performing particular global optimization methods. The correctness of the instantiated algorithms is guaranteed by simple properties that need to be verified on the specific input functions. The use of the generic algorithm is illustrated with an instantiation that yields an automated strategy in PVS for estimating the maximum and minimum values of real-valued functions. The generic branch-and-bound algorithm has been implemented in C++ as part of the Kodiak library and applied to bifurcation analysis of dynamical systems.
Dr. Cesar Munoz is a research computer scientist at NASA Langley Research Center. His primary research interest is the development of formal methods technology for the design, verification, and implementation of safety-critical aerospace systems. Prior to joining NASA in 2009, Dr. Munoz was a Research Fellow at the National Institute of Aerospace. Dr. Munoz currently works on the development of formal methods technology for NASA's Next Generation of Air Traffic Systems (NextGen), Assurance of Flight Critical Systems (AFCS), and Unmanned Aircraft Systems Integration in the National Airspace System (UAS in the NAS) projects. Dr. Munoz has a bachelor degree and master's degree in Computer Engineering from the University of the Andes, Colombia. He also holds a master's degree and a Ph.D. degree in Computer Science from University of Paris 7, France.

Safety assurance cases have been in use for some time in the defense, rail, and oil & gas sectors. Increasingly, they are being adopted for safety assurance in other safety-critical domains, such as aviation, automotive systems, and medical devices. Effectively, safety cases reflect an evidence-driven, argument-based approach to safety assurance, and have become a key element in safety regulation.
Although safety cases marshal heterogeneous evidence, of which a significant portion can include formal engineering artifacts, safety cases themselves remain, largely, informal. Furthermore, in the current practice, their creation, evolution and evaluation continues to be a manually-driven process, with the available set of tools providing little to no support for automation.
In this talk, we present some of the issues involved in moving towards a more formal, automated approach for safety case development, and how some of these have been addressed in our toolset for assurance case automation, AdvoCATE. For example, AdvoCATE (i) can leverage the output of formal methods to auto-generate argument structure fragments, (ii) can automatically assemble such auto-generated fragments with manually created safety cases (iii) provides a mechanism for well-formed hierarchical abstraction, and (iv) supports the specification of well-formed, typed, argument structure patterns that can, further, be automatically instantiated into (provably) well-formed instance arguments
We illustrate our vision for formalism and automation in safety cases by describing how we are applying it to the ongoing creation of a safety case for the Swift Unmanned Aircraft System (UAS) being developed at NASA Ames.

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é).