Bonjour,
J'ai le plaisir du vous inviter à ma soutenance de thèse
Simulation abstraite : une analyse statique de modèles Simulink
qui se déroulera le
lundi 8 décembre 2008 à 14h30
à l'École Polytechnique, amphithéâtre Monge; ainsi qu'au pot qui suivra.
Pour vous rendre à l'École Polytechnique, Cf:
http://www.polytechnique.fr/campus/campus_plans.php
L'amphithéâtre Monge est à côté du numéro 20 du plan:
http://www.polytechnique.fr/images/campus/plan_ecole.pdf
----------------------------------------------------------------------
J'ai le plaisir du vous inviter à ma soutenance de thèse
Simulation abstraite : une analyse statique de modèles Simulink
qui se déroulera le
lundi 8 décembre 2008 à 14h30
à l'École Polytechnique, amphithéâtre Monge; ainsi qu'au pot qui suivra.
Pour vous rendre à l'École Polytechnique, Cf:
http://www.polytechnique.fr/campus/campus_plans.php
L'amphithéâtre Monge est à côté du numéro 20 du plan:
http://www.polytechnique.fr/images/campus/plan_ecole.pdf
----------------------------------------------------------------------
Le jury est composé de :
Jean-Marie Chesneaux, Université Pierre et Marie Curie (Rapporteur)
Nicolas Halbwachs, Vérimag (Rapporteur)
Daniel Krob, Ecole Polytechnique (Examinateur)
Bruno Pagano, Esterel Technologies (Examinateur)
Marc Pouzet, Université Paris-Sud (Examinateur)
Matthieu Martel, Université de Perpignan Via Domitia (Directeur)
---------------------------------------------------------------------------------
Résumé de la thèse :
Résumé de la thèse :
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.
Aucun commentaire:
Enregistrer un commentaire