Présentation de CompoSys
Composys, 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.
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 ...
Composys, 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.
Composys : 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.
Composys vous permet 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é.
Les modèles de Composys sont 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. Deux versions sont disponibles : une
version Unix/Linux (en cours de développement) 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
D'autres explications seront données ultérieurement.
|
