A ce jour, les DMIA sont principalement basés sur une approche logicielle au sens d’un programme informatique exécuté par un microprocesseur, qui pilote un étage électronique (souvent analogique) dédié à stimuler ou à mesurer une activité, sur un nerf, un muscle ou un organe. Cette approche basée logiciel implique un processus de cycle de développement très long qui doit se conformer au cycle de vie imposé par la norme IEC 62304 [56], et qui vise à assurer une conception et une mise en œuvre rigoureuses. Cependant, le recours à une approche basée processeur pose de multiples limitations dont celle relative à la capacité de contrôler une stimulation à la microseconde sans induire une consommation excessive, et celle relative à la capacité de prouver formellement un comportement correct et fiable. En effet, la gestion du parallélisme dans les applications multi-tâches temps réel est toujours délicate, alors que les tests sont inévitablement limités, au sens non-exhaustifs.

Ces deux considérations ont amené l’équipe DEMAR à concevoir des DMIA basés sur des circuits électroniques, soit des composants électroniques programmables (type FPGA  ), soit des circuits électroniques dédiés (type ASIC  ). La mise en oeuvre de systèmes numériques complexes directement sur circuits électroniques a pour avantage de permettre un parallélisme effectif, et ce à faible consommation. C’est donc dans le cadre de la conception formelle de ces systèmes que la méthodologie HILECOP a été développée au sein de l’équipe INRIA DEMAR.

Principes de HILECOP

HILECOP vise à permettre de gérer la complexité et les besoins de fiabilité de tels systèmes. Pour ce faire, la méthodologie sous-jacente se base sur les concepts d’ingénierie dirigée par les modèles [95, 62]. Il est essentiel de fournir aux ingénieurs des « outils » (modèles, mécanismes, méthodologies, etc.) facilitant certes la conception et sa validation, mais également permettant fondamentalement de visualiser la conception et de pouvoir exploiter les représentations graphiques associées comme support de discussions dans le cadre d’une réalisation en équipe. Ces représentations doivent bien sur être non ambiguës, pour éviter toute erreur d’interprétation. Cette dimension, plus relative à l’usage concret des « outils », ne doit pas être négligée; elle a d’ailleurs été prise en considération dans les choix des formalismes sur lesquels s’appuie HILECOP. Ainsi, un système numérique complexe critique est vu comme :
— Une architecture : pour faire face à la complexité du système, la description de l’architecture est basée sur un modèle à composants. Un composant est une entité manipulable et déployable, possédant une interface (ensemble de ports) et un comportement. Les composants peuvent être assemblés par interconnexion des ports de leurs interfaces. Ils peuvent également être « hiérarchisés » au sens de composants incluant des composants, dès lors appelés composites . L’approche à composants favorise donc la conception par raffinement et/ou composition, la modularité et la réutilisabilité.

— Un comportement : pour répondre tant au besoin de modélisation du comportement qu’à son analyse formelle, le comportement de chaque composant est basé sur les réseaux de Petri . L’assemblage de composants lors de la construction de l’architecture induit donc la composition des comportements de ces composants, donnant lieu alors à un modèle global au sens d’un modèle décrivant le comportement de l’intégralité de l’architecture. Il est alors possible d’effectuer une analyse formelle tant du comportement de chaque composant (ou composite) que du comportement du système numérique complet. Parmi les multiples formalismes existants (Machines à états finis [27], Grafcet [32], Statecharts [51], SyncCharts [2], etc.), le recours aux réseaux de Petri est, en plus de son côté formel, aussi motivé par son côté graphique. Ils permettent en effet de représenter explicitement la séquentialité, le parallélisme, la synchronisation, la concurrence et le partage de ressources, le raffinement, la composition, la hiérarchisation, etc. et s’avèrent être un vrai langage graphique et formel de conception pour les ingénieurs, qui peuvent aisément composer (assembler) leurs modèles et visualiser l’évolution de leur modèle même dans le cas d’une structure fortement parallèle.

— Un déploiement : la projection de l’architecture à composants sur une architecture matérielle, comprenant un ou plusieurs FPGA interconnectés, conduit à répartir les composants sur des domaines d’horloge potentiellement différents . Soit les composants sont tous sur le même FPGA et fonctionnent à la même horloge, soit ils sont sur un même FPGA mais ont des horloges différentes, soit ils sont sur des FPGA différents et donc nécessairement leurs horloges sont considérées différentes. Cette précision vise uniquement à souligner que le comportement global est dans certains cas assimilable à celui d’un système GALS : Globalement Asynchrone Localement Synchrone [75]. Il s’agit là aussi d’une caractéristique non-fonctionnelle, visant en particulier à permettre la minimisation de la consommation en faisant fonctionner chaque composant ou composite juste à la fréquence requise.

— Un contrôle d’activité : tous les composants ne doivent pas nécessairement être actifs tout le temps. Dès lors il peut être intéressant de contrôler l’activité des composants pour économiser de l’énergie. Ce contrôle s’exerce par le biais de l’horloge, selon le principe du « clock gating ». Ainsi, l’horloge d’un composant ou d’un composite, voire d’un ensemble de composants ou de composites, peut être contrôlée par un autre composant via un port d’interface dédié ; si l’horloge est « verrouillée » leur comportement n’évolue donc pas. C’est basé sur le principe de propagation d’activité au niveau composant : un composant peut activer ou non l’horloge d’un autre composant pour que son comportement soit exécuté. Cette représentation simplifiée   montre schématiquement les dépendances en termes d’activation et de désactivation, voire d’auto-désactivation (au sens où le composant s’arrête une fois qu’il a terminé son traitement). Par exemple, dès que le coupleur physique reçoit une trame, il active le composant interpréteur qui comprend le reste de la pile protocolaire, qui active à son tour le composant micro-machine (l’exécuteur des profils de stimulation, cf. chapitre 6) si la requête reçue correspond au lancement de la stimulation. La micromachine désactivera son propre fonctionnement une fois la stimulation terminée.

La méthodologie HILECOP ne saurait se limiter à la conception. Nous avons en effet mentionné que :
— Le modèle comportemental, en l’occurrence le réseau de Petri, sera mis en oeuvre au sein d’un circuit électronique. Qu’il s’agisse d’un FPGA ou d’un ASIC, le langage de description retenu est le langage standardisé VHDL  [91]. Au regard de la complexité du système et de la nécessité de minimiser l’intervention humaine dans la phase de programmation, le code VHDL équivalent au modèle est automatiquement généré par HILECOP.
— Le modèle comportemental, qu’il soit partiel (un ou un sous-ensemble de composants) ou global (tous les composants assemblés), doit pouvoir être analysé. De fait, HILECOP génère automatiquement une description équivalente dans le langage PNML  [52] afin de pouvoir exploiter tout analyseur acceptant ce langage normalisé en entrée.
— Le modèle comportemental doit, en d’autres termes, constituer un langage de programmation abstrait facilitant le travail des ingénieurs (à l’image du Grafcet par exemple).

Nos travaux portent sur cette relation entre le modèle initial et le code généré (issu du modèle implémenté, voir figure 1.5), et comment cela doit être pris en compte dans l’analyse formelle. Un code VHDL décrit certes des « relations logiques » mais aussi la manière selon laquelle ces relations logiques sont exécutées au sein du circuit. C’est donc cette génération de code que nous allons approfondir pour comprendre comment le modèle sera exécuté sur la cible (FPGA), et faire émerger les caractéristiques non-fonctionnelles qui doivent impérativement être prises en considération dès l’analyse formelle. En d’autres termes, il est nécessaire de : 1/ capturer tout ce que « cache » cette transformation de modèles (en l’occurrence une transformation de type « model-to-text », du modèle RdP initial au code VHDL), 2/ faire évoluer le formalisme du modèle pour exprimer ces informations significatives et 3/ proposer une technique d’analyse formelle adéquate, i.e. prenant en considération les caractéristiques non-fonctionnelles retranscrites sur le modèle.

Nous allons décrire en détails le formalisme RdP à partir duquel le système initial est modélisé, mais avant cela rappelons les fondamentaux sur les réseaux de Petri.