HtmlToText
skip to content 04 42 37 12 70 rechercher : accueil actualités méthode b méthode b langages b raffinement automatique preuve formelle génération de code outils b travaux r&d travaux r&d open source documentation documentation liens publications contact 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: conférence afis 2006 à toulouse: article – présentation – article afis 2005 conférence afadl’06 à paris: présentation séminaire « ingénierie des systèmes complexes à logiciels prépondérants » ceat 2005: présentation 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. 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. 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
Informations Whois
Whois est un protocole qui permet d'accéder aux informations d'enregistrement.Vous pouvez atteindre quand le site Web a été enregistré, quand il va expirer, quelles sont les coordonnées du site avec les informations suivantes. En un mot, il comprend ces informations;
%%
%% This is the AFNIC Whois server.
%%
%% complete date format : DD/MM/YYYY
%% short date format : DD/MM
%% version : FRNIC-2.5
%%
%% Rights restricted by copyright.
%% See https://www.afnic.fr/en/products-and-services/services/whois/whois-special-notice/
%%
%% Use '-h' option to obtain more information about this service.
%%
%% [2600:3c03:0000:0000:f03c:91ff:feae:779d REQUEST] >> composys.fr
%%
%% RL Net [##########] - RL IP [#########.]
%%
domain: composys.fr
status: ACTIVE
hold: NO
holder-c: C6914-FRNIC
admin-c: C38480-FRNIC
tech-c: UIS153-FRNIC
zone-c: NFC1-FRNIC
nsl-id: NSL9098-FRNIC
registrar: 1&1 Internet SE
Expiry Date: 31/05/2018
created: 31/05/2005
last-update: 31/05/2017
source: FRNIC
ns-list: NSL9098-FRNIC
nserver: ns5.schlund.de
nserver: ns6.schlund.de
source: FRNIC
registrar: 1&1 Internet SE
type: Isp Option 1
address: Ernst-Frey Strasse 9
address: 76135 KARLSRUHE
country: DE
phone: +49 721 91374 50
fax-no: +49 721 91374 215
e-mail: hostmaster@1und1.de
website: http://registrar.1and1.info
anonymous: NO
registered: 17/01/2001
source: FRNIC
nic-hdl: C38480-FRNIC
type: ORGANIZATION
contact: Clearsy
address: Clearsy
address: 320, avenue Archimède
address: les Pléiades 3 batiment A
address: 13857 Aix en Provence
country: FR
phone: +33 4 42 37 12 70
e-mail: helene.bourgeaud@clearsy.com
registrar: 1&1 Internet SE
changed: 12/11/2015 nic@nic.fr
anonymous: NO
obsoleted: NO
source: FRNIC
nic-hdl: UIS153-FRNIC
type: ORGANIZATION
contact: 1&1 Internet SARL
address: 1&1 Internet SARL
address: 7, place de la Gare
address: 57200 Sarreguemines
country: FR
phone: +33 9 70 80 89 11
fax-no: +33 3 87 95 99 74
e-mail: hostmaster@1and1.fr
registrar: 1&1 Internet SE
changed: 30/06/2015 nic@nic.fr
anonymous: NO
obsoleted: NO
source: FRNIC
nic-hdl: C6914-FRNIC
type: ORGANIZATION
contact: Clearsy
address: 320, avenue Archimede
address: les Pleiades 3 batiment A
address: 13857 Aix-en-Provence
country: FR
phone: +33 4 42 37 12 70
e-mail: helene.bourgeaud@clearsy.com
registrar: 1&1 Internet SE
changed: 09/10/2008 whoismaster@nic.fr
anonymous: NO
obsoleted: NO
eligstatus: ok
eligdate: 30/09/2008 00:00:00
source: FRNIC
REFERRER http://www.nic.fr
REGISTRAR AFNIC
SERVERS
SERVER fr.whois-servers.net
ARGS composys.fr
PORT 43
TYPE domain
RegrInfo
DISCLAIMER
%
% This is the AFNIC Whois server.
%
% complete date format : DD/MM/YYYY
% short date format : DD/MM
% version : FRNIC-2.5
%
% Rights restricted by copyright.
% See https://www.afnic.fr/en/products-and-services/services/whois/whois-special-notice/
%
% Use '-h' option to obtain more information about this service.
%
% [2600:3c03:0000:0000:f03c:91ff:feae:779d REQUEST] >> composys.fr
%
% RL Net [##########] - RL IP [#########.]
%
REGISTERED yes
ADMIN
HANDLE C38480-FRNIC
TYPE ORGANIZATION
CONTACT Clearsy
ADDRESS
Clearsy
320, avenue Archimède
les Pléiades 3 batiment A
13857 Aix en Provence
COUNTRY FR
PHONE +33 4 42 37 12 70
EMAIL helene.bourgeaud@clearsy.com
SPONSOR 1&1 Internet SE
CHANGED 2015-11-12
ANONYMOUS NO
OBSOLETED NO
SOURCE FRNIC
TECH
HANDLE UIS153-FRNIC
TYPE ORGANIZATION
CONTACT 1&1 Internet SARL
ADDRESS
1&1 Internet SARL
7, place de la Gare
57200 Sarreguemines
COUNTRY FR
PHONE +33 9 70 80 89 11
FAX +33 3 87 95 99 74
EMAIL hostmaster@1and1.fr
SPONSOR 1&1 Internet SE
CHANGED 2015-06-30
ANONYMOUS NO
OBSOLETED NO
SOURCE FRNIC
OWNER
HANDLE C6914-FRNIC
TYPE ORGANIZATION
CONTACT Clearsy
ADDRESS
320, avenue Archimede
les Pleiades 3 batiment A
13857 Aix-en-Provence
COUNTRY FR
PHONE +33 4 42 37 12 70
EMAIL helene.bourgeaud@clearsy.com
SPONSOR 1&1 Internet SE
CHANGED 2008-10-09
ANONYMOUS NO
OBSOLETED NO
ELIGSTATUS ok
ELIGDATE 30/09/2008 00:00:00
SOURCE FRNIC
DOMAIN
STATUS ACTIVE
HOLD NO
SPONSOR 1&1 Internet SE
EXPIRY DATE 31/05/2018
CREATED 2005-05-31
CHANGED 2017-05-31
SOURCE FRNIC
HANDLE NSL9098-FRNIC
NSERVER
NS5.SCHLUND.DE 217.160.80.132
NS6.SCHLUND.DE 217.160.81.132
NAME composys.fr
Go to top
composys.fr rapport :
Visitez le site