Séminaire vérification de Toulouse
Programme
Cette page rassemble les différents évènements toulousains publics ayant
trait au thème spécification et vérification formelle. Elle rassemble
principalement les séminaires réguliers des laboratoires ONERA-DTIM, IRIT et
LAAS ainsi que les séminaires des chantiers RTRA STAE TORRENTS et IFSE, ou
encore les rendez-vous annuels comme les journées FAC.
Le lieu varie suivant les présentations. Attention, pour l'Onera, l'accès aux ressortissants hors-CEE est soumis à autorisation préalable.
Le lieu varie suivant les présentations. Attention, pour l'Onera, l'accès aux ressortissants hors-CEE est soumis à autorisation préalable.
Séminaires à venir
Séminaires passés (cliquez sur le sujet pour afficher le résumé)
15 octobre 2018 à 9h30 -
Towards a ROS static analysis framework -
Alcino Cunha - Salle Bardeen du LAAS[IFSE]
In this talk I will start by presenting the context that lead us to
embark on this new research project on robotic software quality, namely
present the robotics research groups and projects of INESC TEC, our
research lab. Following a brief presentation of the Robot Operating
System (ROS), one of the most popular middlewares for robotic software
development, including a high-level meta-model of its concepts and
computation graph, I will then present HAROS, a generic, plug-in-driven,
framework for static analysis and quality monitoring of ROS code,
capable of extracting and visualising models conforming to such
meta-model. One of the first usages of HAROS was to conduct a couple of
large studies, by mining many publicly available ROS repositories, to
evaluate the typical internal quality of ROS code and the usage patterns
of ROS primitives in practice, with the goal of helping us (and the
community) establish a roadmap for the development of ROS static
analysis techniques and tools. In the talk I will present and discuss
the results of these studies. Finally, I will present two small
applications we are currently developing based on HAROS: the first is a
pluggin that allows developers to specify rules to validate and impose
coding standards on the ROS computation graph; and the second is a small
tool for property-based testing of a sub-component of a ROS system, that
automatically generates test scripts, including random message
generators for open topics.
02 octobre 2018 à 9h30 -
Target oriented relational model finding -
Alcino Cunha - Salle des thèses de l'IRIT-UPS[IFSE]
In this talk I will present another extension of the popular Kodkod
relational model finder, this one allowing the addition of a desired
target to a problem, as a simple way to indirectly specify the order
preference in which the different instances should be returned. After
presenting how the Kodkod analysis engine was adapted to support such
targets, I will describe two applications we developed that make use of
this extension: the first is Echo, an Eclipse based bidirectional model
transformation tool, that allows the specification of a consistency
relation between two models using the QVT-R language, and that, once one
of the models is updated, tries to recover consistency by performing
minimal repairs in the other; the second is an add-on for the Alloy
Analyzer for improved scenario exploration of software design models, by
allowing the user to choose different strategies to enumerate instances.
17 septembre 2018 à 10h -
Pardinus: a temporal relational model finder -
Alcino Cunha - Salle du DTIM de l'Onera[Séminaire DTIS]
In this talk I will present Pardinus, an extension of the popular Kodkod
relational model finder with mutable relations and temporal logic (to
simplify the analysis of dynamic systems) and with symbolic bounds (to
allow a more precise specification of prior partial knowledge about the
problem). Pardinus currently includes a SAT based bounded-model checking
engine, being developed at INESC TEC - HASLab, and an SMV based
unbounded model checking engine, being developed at ONERA - DTIS. I will
detail the former after briefly presenting Kodkod and the extensions
included in Pardinus. Then I will present the technique currently being
developed to support scenario exploration in Pardinus, namely to allow
iteration through the different instances (or counter-examples) of a
problem. Finally, I will present a decomposed analysis strategy that
aims to improve the efficiency of both analysis engines. This strategy
decomposes a Pardinus problem into two parts, the first containing only
immutable relations and being used to enumerate different configurations
of the system, which are then are then incorporated in the mutable part
and analysed in parallel. Preliminary experimental results showing the
effectiveness of this technique will also be presented.
19 janvier 2017 à 14h -
Heterogeneous and Asynchronous Networks of Timed Systems -
José Fiadeiro, Antónia Lopes - Salle du Boulon de l'Onera[Séminaire DTIM]
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.
11 juillet 2016 à 10h -
Kind 2: Contract-based Compositional Reasoning Contract-based
software development is a leading methodology for the construction of
safety- and mission-critical embedded systems -
Adrien Champion - Salle du Boulon de l'Onera[Séminaire DTIM]
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.
02 mars 2016 à 10h30 -
Credible autocoding of an interior point method algorithm -
Guillaume Davy - Salle des thèses de l'IRIT-UPS[Séminaire Acadie]
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.
15 février 2016 à 10h -
Solving Non-Linear Arithmetic: a Numerical Alternative -
Pierre Roux - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
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.
27 janvier 2016 à 11h -
CoqInterval: A Toolbox for Proving Non-linear Univariate
Inequalities in Coq -
Erik Martin-Dorel - Salle des thèses de l'IRIT-N7 (C0001)[Séminaire ACADIE]
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/
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/
14 décembre 2015 à 10h -
Write Once Run Anywhere with timing-equivalent execution : the CPAL approach -
Nicolas Navet (univ. Luxembourg) - Salle du DTIM de l'Onera[Séminaire DTIM]
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
07 décembre 2015 à 10h -
Presentation of the Electrum framework -
Julien Brunel - David Chemouil - Salle du DTIM de l'Onera[Séminaire DTIM]
Model-checking is increasingly popular in the early phases of the
software development process. To establish the correctness of a
software design one must usually verify both structural and
behavioral (or temporal) properties. Unfortunately, most
specification languages, and accompanying model-checkers, excel
only in analyzing either one or the other kind. This limits their
ability to verify dynamic systems with rich configurations:
systems whose state space is characterized by rich structural
properties, but whose evolution is also expected to satisfy
certain temporal properties. To address this problem, we first
propose a specification language where both rich configurations
and expressive temporal properties can easily be defined. Two
alternative model- checking techniques are then proposed, one
bounded and the other unbounded, to verify systems expressed in
such language, namely to verify that every desirable temporal
property holds for every possible configuration.
30 novembre 2015 à 10h -
Probabilities and Mixed-Criticalities: the Probabilistic C-Space -
Luca Santinelli - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
26 novembre 2015 à 10h30 -
Efficient and sound numerical proofs: floats and Coq -
Pierre Roux - Salle 001 de l'IRIT-UPS[Séminaire ACADIE]
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.
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.
23 novembre 2015 à 10h -
Safety Verification and Refutation by k-invariants and k-induction -
Peter Schrammel - Salle du Boulon de l'Onera[Séminaire IFSE]
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.
12 novembre 2015 à 10h -
A Synchronous-based Code Generator For Explicit Hybrid Systems Languages -
Marc Pouzet - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
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.
08 juin 2015 à 10h -
Optimisation non-linéaire mixte en nombres entiers pour des problèmes d'évitement des conflits d'aéronefs -
Sonia Cafieri (Prof. ENAC) - Salle du DTIM de l'Onera[Séminaire DTIM]
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".
11 mai 2015 à 10h -
Résultats théoriques autour d'Electrum (ou Temporal Alloy, ou encore TLAlloy) -
Denis Kuperberg, Julien Brunel, David Chemouil - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
30 mars 2015 à 10h -
Automatic Architecture Hardening Using Safety Patterns -
Kevin Delmas - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
15 mars 2015 à 10h -
Formal Proofs of Rounding Error Bounds -
Pierre Roux - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
27 janvier 2015 à 10h -
Algorithmes algébriques pour les automates probabilistes -
Nathanaël Fijalkow (Institute of Informatics, Warsaw University and LIAFA, Université Paris 7 - Denis Diderot) - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
01 décembre 2014 à 10h -
Piecewise quadratic Lyapunov functions -
Assalé Adjé, Pierre-Loïc Garoche - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
17 novembre 2014 à 10h -
A modeling framework for software architecture specification and validation -
Nicolas Gobillot - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
13 novembre 2014 à 9h30 -
Target Oriented Relational Model Finding -
Alcino Cunha - Salle du Boulon de l'Onera[Séminaire IFSE]
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.
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.
3 novembre 2014 à 10h30 -
Cubicle : an SMT based model checker for parameterized systems -
Sylvain Conchon - Salle du Boulon de l'Onera[Séminaire DTIM]
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.
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.
20 octobre 2014 à 10h -
Une proposition pour l'ajout de dimensions dans la programmation de logiciels embarqués -
Frederic Boniol - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
06 octobre 2014 à 10h -
Problèmes de décidabilité en théorie des automates -
Denis Kuperberg - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
29 septembre 2014 à 10h -
Verifying the safety of the Transport Class Model (TCM) -
Temesghen Kahsai - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
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.
25 septembre 2014 à 14h -
Preuves formelles et calcul certifié en Coq pour la vérification de bibliothèques mathématiques -
Érik Martin-Dorel - Salle des thèses de l'IRIT-UPS[Séminaire ACADIE]
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.
22 septembre 2014 à 14h30 -
Vérification de langages de scenarios avec des réseaux de Petri -
Rémi Morin - Salle Europe du LAAS[Séminaire LAAS]
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.
02 septembre 2014 à 11h -
Verified Decision Procedures for Regular Expression Equivalence -
Tobias NIPKOW - Salle des thèses de l'IRIT-UPS[Séminaire IRIT]
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.
15 mai 2014 à 15h30 -
Ensuring Aviation Safety : Verification of Interactions between Automated Systems and Humans -
Neha Rungta - salle de l'Auditorium de l'IRIT-UPS[Séminaire IRIT]
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.
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.
21 février 2014 à 14h -
Aide à la localisation d'erreurs dans des systèmes de
contraintes numériques -
Michel Rueher, Prof. à l'Université de Nice Sofia Antipolis - Salle de conférences du LAAS[Séminaire IFSE]
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.
10 février 2014 à 10h -
Policy iterations with templates domain -
Assalé Adjé - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
17 décembre 2013 à 11h -
A Formally Verified Generic Branching Algorithm at Applications to Global
Optimization -
Cesar Muñoz - Salle des thèses de l'ENSEEIHT C002[Séminaire IFSE]
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.
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.
23 septembre 2013 à 14h -
Towards Automation in Assurance Cases: Theory, Tool Support, and Application -
Ewen Denney - NASA Ames - Salle du DTIM de l'Onera[Séminaire IFSE]
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.
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.
22 avril 2013 à 10h -
Analyse formelle d'implémentations de loi de contrôle à l'aide d'outils issus de l'automatique -
Romain Jobredeaux - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
08 avril 2013 à 10h -
Problématique du comportement du cache dans l'ordonnancement -
Maxime Cheramy et Pierre-Emmanuel Hladik - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
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.
27 mars 2013 à 10h -
Predictable Integration of Safety-Critical Software on COTS-based
Embedded Systems -
Marco Caccamo (University of Illinois) - Salle des thèses de l'IRIT-N7 (C0001)[Séminaire TORRENTS]
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.
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.
25 mars 2013 à 10h -
Un langage formel pour les interfaces hommes-machines critiques -
Vincent Lecrubier - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
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.
11 mars 2013 à 10h -
Le framework d'analyse de code binaire Insight -
Aymeric Vincent (Labri) - Salle du Boulon de
l'Onera[Séminaire chantier TORRENTS]
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.
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.
18 février 2013 à 14h30 -
Combinaison des aspects temps réel et sûreté de fonctionnement pour la conception des plateformes avioniques -
Florian Many - Salle des thèses de l'ISAE[Soutenance de thèse]
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.
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.
04 février 2013 à 10h -
Mauve (Modeling Autonomous Vehicules) : une ébauche de modélisation et d'analyse
d'architectures robotiques. -
David Doose et Charles Lesire-Cabaniols, ONERA - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
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.
28 janvier 2013 à 10h -
Using non-convex approximations for efficient analysis of timed automata -
Frédéric Herbreteau, LABRI - Salle du DTIM de l'Onera[Séminaire Torrents]
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.
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.
21 janvier 2013 à 10h -
Analyse de latences de bout en bout dans un système temps réel distribué -
Fred Boniol - Salle du DTIM de l'Onera[Séminaire DTIM]
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).
14 janvier 2013 à 10h -
System level worst-case performance evaluation of embedded Networks -
Ahlem Midfaoui - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
19 décembre 2012 à 14h30 -
MDD in Practice: Where's the friction? -
Robert France, Colorado State University - Auditorium de l'IRIT-UPS[Séminaire IRIT]
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.
17 décembre 2012 à 10h -
Vérification statique de programmes embarqués critiques : structures de données dynamiques -
Pascal Sotin - Onera, salle du DTIM[Séminaire DTIM]
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.
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.
07 décembre 2012 à 10h -
On second-order logics with native mechanisms of (co)inductive data type definition -
Favio Miranda-Perea, professeur à l'Universidad National Autónoma de México (UNAM - Facultad de Ciencias) - Salle 001 de l'IRIT-UPS[Séminaire IRIT]
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.
26 novembre 2012 à 10h -
Analyse de latences de bout en bout dans un système temps réel distribué -
Fred Boniol - Onera, salle du DTIM[Séminaire DTIM]
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).
22 novembre 2012 à 10h -
A Recursive Type System with Type Abbreviations and Abstract Types -
Keiko Nakata - Salle des thèses de l'ENSEEIHT[Séminaire IRIT]
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.
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.
21 novembre 2012 à 9h30 -
Towards formal software deployment -
Fabien Dagnat - Onera[Séminaire IFSE]
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.
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.
20 novembre 2012 à 10h -
Embedded software architectures for satellites at CNES -
Julien Galizzi, CNES - Salle du Boulon de
l'Onera[Séminaire chantier TORRENTS]
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.
19 novembre 2012 à 10h -
Design and Verification of Communicating Systems -
Gwen Salaün - salle C002 (salle des thèses) de l'N7[Séminaire IFSE]
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.
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.
12 novembre 2012 à 10h -
Prelude on SCC with Interlude -
Wolfgang Puffitsch - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
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.
29 octobre 2012 à 10h -
Generating Property Directed Potential Invariants By Backward Analysis. -
Adrien Champion - Salle du DTIM de l'Onera[Seminaire DTIM]
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.
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.
22 octobre 2012 à 10h -
Changements de mode dans les systèmes temps réel -
Thomasz Kloda - Salle du DTIM de l'Onera[Séminaire DTIM]
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.
16 octobre 2012 -
Une Approche Intégrée pour la Validation et la
Génération de Systèmes Critiques par Raffinement Incrémental de
Modèles Architecturaux
-
Gilles Lasnier
- ISAE
[Séminaire TORRENTS]
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.
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.
8 octobre 2012 -
Kind-AI: When abstract interpretation and
SMT-based model-checking meet
-
Pierre-Loïc Garoche
- Salle du DTIM de
l'Onera
[Séminaire DTIM]
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.
(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.
1er octobre 2012 -
Policy iteration as Traditional Abstract
Domains
-
Pierre Roux
- Salle du DTIM de
l'Onera
[Séminaire DTIM]
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
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
10 septembre 2012 -
Probabilistic WCET Challenges within the
real-time research community are mostly in terms of modeling and
analyzing the complexity of actual real-time embedded systems.
-
Luca Santinelli
- Salle du DTIM de
l'Onera
[Séminaire DTIM]
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.
9 juillet 2012 -
Vérification et Validation des systèmes de
commande et guidage des systèmes aéronautiques
-
Eric Feron
- Salle des theses de
l'IRIT N7
[Séminaire DTIM]
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.
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.
28 juin 2012 -
Hard Real-Time Garbage Collection on Chip
Multi-Processors
-
Wolfgang Puffitsch
- Salle du Boulon de
l'Onera
[Séminaire DTIM]
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 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
12 décembre 2011 -
2nd TORRENTS workshop
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.
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.
22 novembre 2011 -
A Proof Pearl with the Fan Theorem and Bar
Induction: Walking through infinite trees with mixed induction and
coinduction
-
Keiko Nakata, senior researcher à l'Institut de
Cybernétique de l'Université Technique de Tallinn -
- Salle des thèses de
l'IRIT-UPS
[Séminaire chantier IFSE]
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)
We have fully formalized our development with the Coq proof assistant.
(Joint work with Marc Bezem and Tarmo Uustalu)
22 novembre 2011 -
Handling of Engine Management real-time
architecture at Continental Automotive -
Denis Claraz, Continental Automotive France SAS
Powertrain Engine Systems -
- Salle du boulon de
l'ONERA
[Séminaire chantier TORRENTS]
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.
21 novembre 2011 -
Ptides: A Model-based Design Approach for
Deterministic, Event-driven Real-time Applications
-
Patricia Derler - Univ of Berkeley
- Salle de Boulon de
l'Onera
[Séminaire chantier TORRENTS]
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.
27 septembre 2011 -
Real-Time Operating Systems for ManyCore
Processors
-
Florian Kluge (Univ. of Augsburg,
Germany) -
- Auditorium de
l'IRIT
[Séminaire chantier TORRENTS]
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.
23 juin 2011 -
Practical program verification for the working
programmer with CodeContracts and Abstract Interpretation -
Francesco Logozzo
- Salle C0002 de
l'ENSEEIHT
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
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
3 mai 2011 -
Preuve automatique de Programmes par
Instrumentation d'Interprètes abstraits
-
Manuel Garnacho
- Salle du Boulon de
l'Onera
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.
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.
14 avril 2011 -
Reasoning about correctness of software
transactional memory
-
Tarmo Uustalu
- Salle des thèses de
l'ENSEEIHT (C002)
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.)
14 février 2011 -
Modélisation/traitement des erreurs
transitoires.
-
Guy Durrieu
- Salle du DTIM de
l'ONERA
[Séminaire DTIM]
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
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
24 janvier 2011 -
Vérifier la démonstration du théorême de Church
Rosser en Coq sans s'abstraire des difficultes liées à
l'alpha-conversion
-
Adrien Champion
- Salle du DTIM à
l'Onera
[Séminaire DTIM]
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.
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.
17 janvier 2011 -
Dessine moi un domaine abstrait fini - une
recette à base de Camlp4 et de solveurs SMT
-
Pierre
Roux
et Pierre-Loïc
Garoche
- Salle du DTIM à
l'Onera
[Séminaire DTIM]
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.
3 janvier 2011 -
SMT-based model checking and invariant
generation for data flow programs
-
Cesare Tinelli
- Salle du Boulon à
l'Onera
[Séminaire DTIM]
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.
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.
13 décembre 2010 -
Application des méthodes par ordres-partiels à
la vérification formelle de systèmes asynchrones clos par un contexte
:application à SDL
-
Xavier Dumas
- Salle du boulon à
l'Onera
[Séminaire DTIM]
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.
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.
29 novembre 2010 -
Théorie des contrats modaux pour les systèmes
embarqués
-
Jean-Baptiste Raclet (IRIT)
- Salle du DTIM à
l'Onera
[Séminaire DTIM]
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.
23 novembre 2010 -
Hierarchical Set Decision Diagrams and Automatic
Saturation -
Alexandre Hamez
- Salle Feynman au
LAAS
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.
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.
18 novembre 2010 -
Vers une méthodologie dédiée à l’orchestration
d’entités communicantes -
Zoé Drey
- IRIT site ENSEEIHT
-- Salle des thèses C002
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
Mots clés : méthodologie, langages visuels, langages dédiés, accessibilité, assistance à la personne
3 novembre 2010 -
Applications of control to formal software
semantics -
Eric
Feron, Dutton-Ducoffe Professor of Aerospace Engineering,
Georgia Institute of Technology
- Salle
A202
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.
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.
2 novembre 2010 -
First TORRENTS working day
-
Paul
Caspi, Edward
Lee, Wolfgang
Pree
and Jean-Pierre
Talpin
-
[TORRENTS workshop]
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.
11 octobre 2010 -
Calcul de pires temps fonctionnels
-
Michaël Lauer
- Salle du DTIM à
l'Onera
[Séminaire DTIM]
27 septembre 2010 -
Dalculus - Theory and Tool for DAL allocation
-
Pierre Bieber et Rémi Delmas
- Salle du DTIM à
l'Onera
[Séminaire DTIM]
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.
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.
31 mai 2010 -
Accelerated model-checking for real-time
systems -
Frédéric
Herbreteau (LaBRI)
- Salle de réunion du
DTIM (1e étage de la 4e dent) à l'Onera
[Séminaire DTIM]
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.
20 avril 2010 -
Model Checking with Edge-valued Decision
Diagrams -
Pierre Roux
- Salle du Boulon de
l'Onera
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.
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.
31 mars au 1er avril 2010 -
17e
édition des journées "Formalisation des Activités Concurrentes"
FAC'2010 -
- Salle du Boulon de
l'Onera
[Journées FAC'2010]
30 mars 2010 -
Théorie des catégories appliquée à
l'architecture des logiciels et systèmes -
José
Luiz Fiadeiro
- Salle du Boulon de
l'Onera
[Journées FAC'2010]
2 mars 2010 -
Verification of the Schorr-Waite algorithm -
from trees to graphs
-
Mathieu
Giorgino
- Salle 157 de
l'IRIT-UPS
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:
L'ensemble du travail a été réalisé dans l'assistant de preuve Isabelle/HOL.
- 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.
L'ensemble du travail a été réalisé dans l'assistant de preuve Isabelle/HOL.
1 mars 2010 -
AADL, de l'analyse à la génération de
code -
Jérôme
Hugues (ISAE)
- Salle de réunion du
DTIM (1e étage de la 4e dent) à l'Onera
[Séminaire DTIM]
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.
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.
16 février 2010 -
Réécriture de graphes attribués (théorie des
catégories et théorie des types) -
Louis Féraud, Sergei Soloviev, Hanh-Nhi Tran et
Bertrand Boisvert, avec des contributions de Lionel
Marie-Magdeleine, Christian Percebois, Maxime Rebout
- Salle 157 de
l'IRIT-UPS
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.
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.
2 février 2010 -
Panorama des méthodes basées SAT dans l'industrie
-
Rémi Delmas
- Salle de réunion du
DTIM (2e étage) à l'Onera
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.
12 janvier 2010 -
Logique monadique du deuxième ordre et
sémantiques concurrentes des réseaux de Petri
-
Jean
Fanchon
- Salle Europe du
LAAS
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)
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.
17 novembre 2009 -
Formalisation de la logique de description ALC
dans l'assistant de preuve Coq
-
Mohamed Chaabani
- Salle 157 de
l'IRIT-UPS
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.
12 novembre 2009 -
Sequential game theory: a formal and abstract approach.
-
Stéphane
Le Roux (École Polytechnique)
- Salle 175 de
l'IRIT2-UPS
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.
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.
3 novembre 2009 -
Strict Simulation of a Lambda Calculus for
Classical Logic in Simply-Typed Lambda Calculus (Second Part of:
Traductions par passage de continuations, ses variantes, et ses
généralisations aux monades - séminaire du 19
mai) -
Ralph
Matthes
- Salle 175 de
l'IRIT-UPS
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).
29 octobre 2009 -
Type-checking and type-inference problems for polymorphic and
existential types
-
Koji
NAKAZAWA, University of Kyoto
- Salle des thèses
de l'IRIT-UPS
[Séminaire IRIT]
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.
30 juin 2009 -
A modular technique for termination proofs in
abstract rewriting systems -
David Chemouil
- Salle du Boulon à
l'Onera
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.
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.
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.
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.
19 mai 2009 -
Traductions par passage de continuations, ses
variantes, et ses généralisations aux monades
-
Ralph
Matthes
- Salle des thèses
de l'IRIT-UPS
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 présenterons le langage qui permet de spécifier les motifs et les transformations de code, ainsi que la logique temporelle sous-jacente.
21 avril 2009 -
Modélisation d'un langage synchrone dans un
assistant de preuve -
Martin
Strecker
- Salle des thèses
de l'IRIT-UPS
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é).