CompoSys

Outil de description formelle de système

Site Web  : www.composys.fr


CompoSys

CompoSys

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

D’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.

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é.

Modèles compatibles avec l’outil Atelier B de Clearsy

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.

Outils et techniques de CompoSys

CompoSys a été développé dans l’environnement Eclipse. Il 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

Les commentaires sont fermés.