CompoSys: méthode et outil dédié aux descriptions formelles de systèmes

Qu’est-ce que CompoSys ?

La distribution de CompoSys a été suspendue en 2012. La dernière version distribuée a été la version 1.6.

CompoSys est un outil de conception formelle d’architecture système. Développé par la société ClearSy, société spécialiste en développement de systèmes sécuritaires, CompoSys est un outil de modélisation de systèmes qui bénéficie des outils formels et de l’expérience de l’Atelier B.

CompoSys a déjà été utilisé par ClearSy sur les projets industriels suivants :

  • Intégration fonctionnelle d’un véhicule militaire (SPRAT) réalisé par CNIM
  • Modélisation de 3 véhicules pour le diagnostic : 206, 307, 407
  • Étude système des façades de quai mises en place par RATP lignes 13 et 14
  • Modélisation de la politique de sécurité d’un composant hardware ST Micro-Electronics
  • Modélisation de l’interface d’un micro-noyau dans le domaine micro-électronique
  • Modélisation de l’architecture d’une carte de communication USB/CAN
  • Modélisation du dispositif d’ouverture et de fermeture des façades de quai qui vont équiper la ligne 1 du métro parisien
  • Modélisation d’un système de commande automatique du déploiement d’une marche pour piéton pour combler l’espace entre un quai et un train

Les résultats obtenus par CompoSys ont été à l’origine de plusieurs communications:

Zoom sur CompoSys

CompoSys possède de nombreuses fonctionnalités, parmi lesquelles nous pouvons compter :

  • un processus de modélisation couplée : méthode formelle B / langage naturel
  • des vérifications automatiques et semi-automatiques de la cohérence du modèle
  • une génération automatique du document final et de différentes vues du système

Un outil de description formelle de système

CompoSys est, d’une part un outil d’aide à la description formelle des composants et de leurs interactions dans un système hybride.

schema+atelierb+composysD’autre part, CompoSys exploite cette base d’informations (ou modèle formel) commune pour produire des informations nécessaires aux activités qui nécessitent une vue précise de l’ensemble du système. Par exemple :

  • sûreté de fonctionnement,
  • démonstration formelle de propriétés,
  • spécifications fonctionnelles,
  • fiches de validation,
  • matrices réseaux,
  • bilans électriques …

Une méthode de modélisation formelle de système

Le modélisateur est la personne responsable de créer et d’enrichir la description du système au fur et à mesure de sa définition. Il aide à l’exploitation de cette base d’informations. Il décrit dans des « opérations » comment les composants utilisent les différents paramètres du système et pour les paramètres inter-composants par quels média physiques ils sont partagés : bus, circuits hydrauliques,analogiques, électriques…

Le contenu des opérations est formalisé sous forme d’expressions mathématiques univoques. Ainsi la dépendance entre les opérations et les interactions entre les composants sont faites naturellement et rapidement par ces « explications » formelles.

Exploitation du modèle pour produire un document de projet

Par ailleurs, CompoSys prévoit que le modèle formel soit enrichi en langage naturel et en illustrations, en respectant des règles strictes. La base d’informations est ainsi à deux faces indissociables :

  • la face formelle qui permet de guider le modélisateur, d’automatiser les vérifications et d’automatiser la génération des documents dans tous les formats nécessaires à l’exploitation pluri-disciplinaire de cette information.
  • la face informelle, qui permet de restituer une information plus complète, et compréhensible par un lecteur non expert en langage formel(que la face formelle). Dans les documents générés, on retrouve, sous forme de dessins et d’explications homogènes, la description des composants du système, de leurs fonctions et des entrée/sorties.

Une intégration virtuelle des composants du système

Chaque fois que le modélisateur saisit une nouvelle opération, CompoSys, en plus des vérifications syntaxiques et de typage, vérifie 50 règles de cohérence, calcule et dessine les interactions entre les composants et ceci même à partir d’un modèle incomplet. Ainsi CompoSys permet de valider et de tester plusieurs architectures fonctionnelles au fur et à mesure de leur description. Cette caractéristique constitue un atout lorsque le système est en cours de définition et que l’on souhaite connaître son niveau de cohérence à un instant donné.

Le langage formel utilisé est le B événementiel. Les modèles réalisés peuvent par ailleurs être exploités par l’outil formel Atelier B pour faire la démonstration formelle de propriétés en utilisant les concepts d’abstractions, de raffinements et d’invariants. CompoSys a été développé dans l’environnement Eclipse. Deux versions sont disponibles : une version Unix/Linux  et une version Windows. CompoSys est un plugin Eclipse qui intègre :

  • un éditeur de modèles B
  • un éditeur de dictionnaire de termes
  • un outil de vérification des modèles B
  • un outil de vérification de cohérence des composants
  • un générateur de documentation technique en langage naturel

 Références Industrielles: Le Projet Peugeot

Avec l’arrivée massive de l’électronique embarquée, les fonctionnalités proposées par les constructeurs automobiles sont devenues de plus en plus complexes. Les réparateurs automobiles sont confrontés à de nouveaux problèmes avec ces fonctions, qui dépendent de plusieurs calculateurs et actionneurs répartis sur des réseaux informatiques internes au véhicule (multiplexage). Les services après-vente doivent se munir de nouvelles méthodes et de nouveaux outils.

La méthode proposée par ClearSy consiste à décrire les propriétés essentielles de fonctionnement que doit respecter le véhicule avec un niveau de détail constant. Les diagnostics sont ensuite effectués en comparant le comportement réel du véhicule par rapport à ces règles de fonctionnement. L’utilisation d’un formalisme mathématique rigoureux nous permet de : décrire précisément les propriétés du système pour chaque élément remplaçable qui participe à une fonctionnalité, trouver rapidement les ambiguïtés et les lacunes dans les documents de spécification, prouver la cohérence des spécifications.

Cette méthode a été appliquée pour toutes les fonctions de deux véhicules (206, 307 et 407), y compris les fonctions mécaniques et électroniques (Moteurs, boîtes de vitesse automatiques. Les documents produits sont actuellement exploités par les experts des plateaux d’assistance du service après-vente PEUGEOT. La prochaine phase de travaux est la définition d’outils informatiques exploitant directement les modèles mathématiques pour faire du diagnostic automatique.

Références Industrielles: Le Projet CNIM (Pont d’Assaut Modulaire ou « SPRAT »)

L’originalité du système vient du fait que la longueur du pont est modulée en fonction de la largeur de l’obstacle à franchir. La CNIM développe et fabrique le « SPRAT » (Système de Pose Rapide de Travures). Ce pont d’assaut comprend une travure modulaire de classe MLC 70, de 26 m en deux parties, lancée par un véhicule tout terrain à roues. ClearSy est chargée de l’intégration fonctionnelle du véhicule.

Ce matériel de franchissement de l’avant se caractérise par :

  • une excellente mobilité grâce au progrès des véhicules de transport à roues;
  • un coût de possession bien inférieur à celui des véhicules sur chenilles.

Réalisation :

  • Développement des interfaces entre les sous-systèmes du ponteur du SPRAT et l’allocation des fonctions inter-systèmes à chaque système.
  • Les paramètres réseaux, électriques qu’il utilise et qu’il produit (matrice CAN par exemple)
  • Les grandeurs physiques mesurées (capteurs)
  • Les actionneurs qui sont pris en charge
  • Les opérations élémentaires qui doivent être effectuées
  • Les dépendances entre les fonctions

La modélisation de l’architecture est maintenant utilisée à la CNIM pour l’élaboration des études de dysfonctionnement (AMDEC). Elle a permit de définir le niveau d’architecture de la base roulante véhicule, travail très utilisé aujourd’hui pour l’élaboration des plans de tests du SPRAT. De plus, cette étude a permis de mettre en place une documentation technique très utilisée par les fournisseurs des différents éléments de cette architecture.

Cette modélisation du système SPRAT a permis d’aider à la mise en place de l’architecture dans un but de contrôler la cohérence inter systèmes. Cette modélisation fut la première représentation complète de l’architecture électrique électronique du ponteur SPRAT.

Les commentaires sont fermés.