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 abiliser 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 2, 2014. Français
Liste complète des métadonnées

https://hal-lirmm.ccsd.cnrs.fr/tel-01111881
Contributeur : David Andreu <>
Soumis le : samedi 31 janvier 2015 - 19:56:31
Dernière modification le : samedi 27 janvier 2018 - 01:30:52

Identifiants

  • HAL Id : tel-01111881, 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 2, 2014. Français. 〈tel-01111881〉

Partager

Métriques

Consultations de la notice

613

Téléchargements de fichiers

11