2008
Simulation abstraite : une analyse statique de modèles Simulink
Par Chapoutot Alexandre (Université Paris 6 - LIP6) le 2008-12-04
- La conception de systèmes embarqués nécessite de plus en plus l'utilisation d'outils logiciels afin de contenir la complexité croissante de ceux-ci. Les deux principaux outils industriels dans ce domaine sont Simulink et Lustre/Scade. Ces deux outils possèdent de nombreuses fonctionnalités comme un moteur de simulations, des générateurs de tests ou de code. Cependant, Simulink est, dans la majorité des cas, utilisé pour la conception de systèmes embarqués et ceci parce qu'il a une expressivité plus importante. Il est capable de modéliser et de simuler des systèmes à temps continu, à temps discret et un mélange des deux, c'est-à-dire des systèmes hybrides. Pour la conception des systèmes embarqués, Simulink permet de modéliser l'environnement physique et le logiciel embarqué dans un même formalisme. L'application des méthodes formelles sur de telles spécifications est un défi industriel et scientifique important pour la validation des logiciels embarqués. De plus, l'utilisation de méthodes formelles, au plus tôt dans le cycle de développement, est un challenge essentiel dans l'industrie afin de réduire les coûts liés à la correction de bogues. Dans cette thèse, nous définissons une analyse statique par interprétation abstraite de modèles Simulink. Nous appelons cette analyse simulation abstraite. L'objectif de la simulation abstraite est de fournir un critère de correction des comportements numériques des exécutions des modèles Simulink. Ces simulations sont souvent utilisées pour valider les systèmes modélisés, mais elles sont plus proches de l'activité de tests que celle de la preuve. En conséquence, elles ne permettent pas de valider vis-à-vis des spécifications un système modélisé avec Simulink. La simulation abstraite fournit un critère de correction dans le sens que les comportements des modèles Simulink représentent au mieux les comportements du monde réel. Nous supposons que le modèle mathématique, représenté par un modèle Simulink, est correcte vis-à-vis du monde réel. Notre objectif est de calculer automatiquement et conjointement une sur-approximation des comportements mathématiques et des comportements issus de la simulation numérique pour une plage d'entrées possibles. Nous sommes ainsi capable d'estimer l'ensemble des imprécisions introduit par la simulation numérique, c'est-à-dire les erreurs d'arrondi ou les erreurs de troncature liées, par exemple, aux capteurs. Le critère de correction des modèles à temps continu est obtenu en évaluant la distance séparant les résultats des méthodes d'intégration numérique, utilisées par le moteur de simulations, des résultats obtenus par un méthode d'intégration numérique garantie. Le critère de correction des modèles à temps discret est donné par l'utilisation le domaine numérique abstrait des nombres flottants avec erreurs différentiées. Ce nouveau domaine numérique est issu de la combinaison du domaine des flottants avec erreurs et la méthode de différentiation automatique permettant d'avoir une meilleure abstraction des erreurs. Nous définissons également une abstraction d'un domaine des séquences utilisant les partitions d'un ensemble. Nous sommes ainsi en mesure de représenter des simulations infinies d'une manière finie. L'ensemble de ces domaines permet alors d'estimer les erreurs introduites par les traitements numériques présents lors des simulations. Nous obtenons alors une méthode de validation des comportements numériques des systèmes embarqués modélisés en Simulink.
Vers des supports exécutifs capables d'exploiter les machines multicœurs hétérogènes
Par Augonnet Cédric (INRIA Bordeaux - Runtime) le 2008-11-27
- Si de nombreux efforts ont été portés sur la programmation d'architectures multicœurs, et plus récemment sur l'utilisation d'accélérateurs (GPGPUs, Cell, FPGA, ...), il reste bien difficile d'exploiter l'ensemble de ces ressources de calcul simultanément. Nous présentons donc un support exécutif qui s'articule autour d'un modèle d'exécution unifié et d'une bibliothèque pour automatiser les mouvements de données. Nous montrons que notre approche permet d'exploiter efficacement ces machines, tout en cachant une partie de leur complexité. Alors que l'hétérogénéité est a priori le principal frein à l'utilisation de telles plate-formes, nous mettons en évidence que l'utilisation de stratégies d'ordonnancement permet en fait de tirer parti de cette même hétérogénéité.
Méthodologie de Prototypage rapide des MPSoC sur des plateformes reconfigurables
Par Senouci Benaoumeur (Université de Perpignan - DALI) le 2008-11-20
- Multiprocessor Systems on-Chip (MPSoCs) are considered as the generation of architectures able to deal with the ever increasing performances and scalability applications demands. On the other hand Multi-CPU/FPGA platforms based prototyping approach is an attractive solution for fast validation of MPSoCs embedded software. My thesis investigates to understand the complexities of the Hardware/Software interface design process in MPSoC. We propose a new generic MPSoC prototyping flow based on these reconfigurable hardware platforms, which allows fast prototyping of POSIX threads based applications, taking into the count homogeneous and heterogeneous multiprocessor systems. Applications running on those platforms use a centralized/distributed POSIX compliant operating system. Actually, combining heterogeneous processors in the same architecture allows drawing on strength from each kind of processor, increasing overall system performance and efficiency. However, such a design introduces new challenges, especially for embedded software designers. I address also in my thesis, the difficulty of ensuring an efficient bridging between processors in heterogeneous MPSoC. We propose a common FPGA based middleware structure to manage communication and synchronisation between the processors. Then, we describe a semi-systematic design space exploration framework for automatic inter-processor communication and synchronization refinement.
Résoudre et Certifier la solution d'un système linéaire
Par Nguyen Hong Diep (ENS-Lyon - LIP) le 2008-11-13
- Je présenterais une approche pour résoudre un système linéaire et simultanément certifier la solution calculée. Par certifier, on entend calculer un encadrement garanti de l'erreur. Pour cela, nous passons de l'arithmétique flottante à l'arithmétique par intervalles et nous résolvons le système linéaire satisfait par le résidu. Cela nous donne une borne garantie de l'erreur sur le résultat exact. Nous avons adapté une méthode de raffinement itératif pour le calcul de la borne d'erreur. La combinaison de deux composantes de base, à savoir la résolution en arithmétique flottante d'un système linéaire et le raffinement itératif de la borne d'erreur en utilisant l'arithmétique par intervalles, produit une solution plus précise dotée d'une borne d'erreur. Cette borne d'erreur nous permet d'estimer en outre le nombre de chiffres corrects de la solution approchée. Notre approche est implantée en utilisant les bibliothèques MPFR et MPFI. Ces deux bibliothèques nous permettent d'adapter la précision utilisée à chaque étape. Cela nous a permis d'étudier aussi l'effet de la précision utilisée pour le calcul du résidu sur la qualité du résultat calculé. Les résultats expérimentaux illustrent le gain au niveau de la qualité de la solution et de la borne d'erreur lié à la précision utilisée pour les calculs.
Accélération de temps de simulation
Par Bouache Mourad (Université de Perpignan - DALI et Université de Boumerdès, Algérie) le 2008-10-23
La complexité croissante des processeurs, due en particulier à la multiplication des ressources (multi-coeurs), rend la compréhension de leur comportement et l'estimation de leur performance extrêmement difficile. Les architectes ont jusqu'ici mis en oeuvre les nouveaux mécanismes qu'ils ont proposé au moyen de simulateurs monolithiques tels que SimpleScalar . Au sein de ces simulateurs, constitués d'un programme unique regroupant toutes les unités du processeur, y compris sa hiérarchie mémoire, il est malaisé de focaliser son attention sur une unité, soit pour en étudier le rendement, soit pour le comparer à celui d'une unité de remplacement basée sur un algorithme qu'on conjecture plus performant. Le développement d'un nouveau simulateur est un investissement conséquent en temps à cause d'un long processus de modélisation, de débogage et de validation. Les simulateurs monolithiques sont des solutions de moins en moins adaptées au développement d'architectures de plus en plus complexes. L'adoption d'environnements de simulation modulaires devient donc une nécessité, mais de tels environnements ne peuvent être exploités correctement sans y a jouter une méthodologie de conception basée sur un protocole de communication intermodules. Le passage aux environnements de simulation modulaires induit un ralentissement de la simulation par rapport aux simulateurs monolithiques. La vitesse de simulation est un facteur critique car elle bride l'étendue des solutions qui peuvent être évaluées par les architectes de processeur. Dans un premier temps, nous présenterons l'environnement de simulation UNISIM et son mécanisme de communication inter-module. Nous présenterons aussi un simulateur générique de processeur à exécution dans le désordre que nous avons développé à partir d'UNISIM. Nous présenterons ensuite notre proposition d'extension du protocole de communication permettant le développement de modules vectorisés, orientés vers la duplication des ressources. Des résultats préléminaires montrent que la simulation d'un vecteur de n unités est nettement plus rapide que celle de n modules représentant autant d'unités individuelles.
Formal methods for rare failures of long processes
Par Daumas Marc (Université de Perpignan - DALI) le 2008-09-30
It is widely admitted that industrial processes contain flaws and they are allowed to fail. We describe a theory suitable for extremely rare failures of very long processes. This theory can be applied to hybrid systems modeling, for example an aircraft or a nuclear power plant on one side and its software on the other side. We are using PVS and a previously published formal theory on random variables as such formal developments force explicit statement of all hypotheses and prevent incorrect uses of theorems. Under the hypothesis that first order errors dominate, accumulated errors are sums of independent discrete and continuous variables. We derive a simple formula based on Lévy's and Markov's inequalities that can be applied to any sequence of independent and symmetric random variables that admit second and fourth order moments, such as variables uniformly distributed over [-ulp/2,ulp/2]. We bound the probability that the accumulated errors were never above a given threshold. Quick highest order instantiation after almost a billion operations in single precision with a probability of failure below one against almost a billion shows about a fourth of the bits are significant where worst case analysis considers that no significant bit remains. Future developments will use Doob's original inequality that follows a proof path very different form Doob-Kolmogorov inequality used in former developments.
Analyse statique de systèmes hybrides discrets-continus
Par Bouissou Olivier (CEA-LIST) le 2008-09-18
- Je présenterai le résultat de mes travaux sur l'analyse statique des logiciels embarqués, et notamment une théorie qui permet de prendre en considération, en plus du code embarqué, l'environnement physique dans lequel il est exécuté. On abordera principalement les points suivants : - La construction d'un nouveau modèle pour les logiciels embarqués qui prend en compte l'environnement physique avec lequel le logiciel interagit. - La construction d'une sémantique dénotationnelle pour ce nouveau modèle qui est définit comme une extension de la sémantique dénotationnelle classique des langages de programmation. - Une méthode d'analyse statique par interprétation abstraites des logiciels embarqués par une analyse disjointe de la partie discrète (le code) et de la partie continue (l'environnement physique). - Une méthode d'analyse de la partie continue nommée GRKLib et qui permet de calculer des bornes garanties sur la solution d'une équation différentielle à partir d'une méthode de résolution numérique à la Runge-Kutta.