Méthodologie de conception d'architectures numériques complexes : du formalisme à l’implémentation en passant par l'analyse, préservation de la conformité. Application aux neuroprothèses

Hélène Leroux 1
1 DEMAR - Artificial movement and gait restoration
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier, CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : Dans ce mémoire, la conception de systèmes numériques complexes, et notamment de systèmes embarqués critiques, est abordée au travers d'une méthodologie allant de la modélisation formelle à l'implantation sur FPGA : la méthodologie HILECOP. Celle-ci offre au concepteur la possibilité de représenter dans un modèle formel d'une part l'architecture du système selon un assemblage de composants, et d'autre part le comportement de ces composants et leur composition par réseaux de Petri temporels. Le modèle décrit est ensuite transformé automatiquement en un modèle implémentable (en langage VHDL) pour son exécution sur la cible matérielle, mais également en un modèle analysable pour permettre l'analyse formelle des propriétés du système. Les deux objectifs principaux des travaux présentés sont l'étude de la conformité d'un point de vue comportemental entre les différents modèles utilisés dans la méthodologie (modèle conçu, modèle implémentable et modèle analysable), ainsi que l'intégration d'un mécanisme de gestion efficace des exceptions. Ces travaux ont permis de fiabiliser l'implémentation du modèle et d'obtenir un modèle analysable plus pertinent par rapport au modèle conçu, dans le sens où il garantit l'inclusion du comportement du modèle conçu dans celui du modèle analysé et réduit, dans une certaine mesure, le risque d'explosion combinatoire. Les limites de la pertinence des résultats obtenus par analyse formelle sont de plus désormais connues. En ce qui concerne la gestion des exceptions, principalement étudiée au niveau comportemental, le mécanisme de la macro-place a été retenu et adapté aux contraintes fonctionnelles et non-fonctionnelles des systèmes embarqués critiques. L'apport de la macro-place et la conservation de la conformité ont pu être validés sur des modèles industriels relatifs à l'architecture numérique de neuroprothèses.
Type de document :
Thèse
Automatique / Robotique. Université Montpellier II - Sciences et Techniques du Languedoc, 2014. Français. 〈NNT : 2014MON20163〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://tel.archives-ouvertes.fr/tel-01766458
Contributeur : Abes Star <>
Soumis le : vendredi 13 avril 2018 - 16:05:08
Dernière modification le : mercredi 18 juillet 2018 - 11:54:45

Fichier

41557_LEROUX_2014_archivage_co...
Version validée par le jury (STAR)

Identifiants

  • HAL Id : tel-01766458, version 1

Collections

Citation

Hélène Leroux. Méthodologie de conception d'architectures numériques complexes : du formalisme à l’implémentation en passant par l'analyse, préservation de la conformité. Application aux neuroprothèses. Automatique / Robotique. Université Montpellier II - Sciences et Techniques du Languedoc, 2014. Français. 〈NNT : 2014MON20163〉. 〈tel-01766458〉

Partager

Métriques

Consultations de la notice

128

Téléchargements de fichiers

16