Accueil l Actualités B l La Méthode B l Travaux R&D l Preuve Formelle l Publications
B, les différents langages
 
l Outils B l Documents l B Tools Forum  l Nos Liens l Contact    


Projet COSYC

 

Présentation du Projet Cosyc

Le projet aura une durée de 30 mois. Il s’articulera autour de deux axes :

    •  B : langage, méthode et outils permettant de construire des logiciels sans défaut, et de valider la spécification fonctionnelle de systèmes complexes

    • AltaRica : langage formel pour les études de fiabilité. Les outils ont été choisis par Dassault Aviation pour les études de sûreté de fonctionnement de ses avions Falcon F7X et par Airbus Industries pour son programme A350.

Dans un outil de modélisation hybride :

  • L’analyse de cas tests industriels sous l’angle de cette intégration (étude de système de contrôle/commande de portes palières de type Coppilot).

Il associe :

  • l’université de Marseille – groupe de recherche ERISCS

  • ClearSy

  • Arboost Technologies

      


Cadre du Projet

Ce projet s’inscrit dans le cadre du pôle de compétitivité « Systèmes Communicants Sécurisés » de la région PACA. Il concerne plus particulièrement les systèmes communicants embarqués critiques, c'est-à-dire qui présentent un risque en cas de fonctionnement incorrect pour les personnes et/ou l'environnement. Parmi ceux-ci, on peut citer les systèmes de supervision, de commande ou de contrôle d’installations industrielles telles que les usines chimiques et nucléaires, des réseaux de transport ou de télécommunications, les systèmes critiques de santé, les systèmes transactionnels,... La caractéristique de ces systèmes, outre le fait d’être critiques, est qu’ils intègrent à la fois des composants matériels et des composants logiciels. La part des logiciels y est de plus en plus importante. Il faut donc garantir que ces derniers fonctionnent correctement sur l'architecture matérielle choisie, y compris lorsque l’environnement est perturbé. En d’autres termes, il est essentiel d’étudier la résistance du système aux pannes des composants matériels et/ou logiciels, et les conséquences de ces pannes lorsque le fonctionnement correct ne peut plus être garanti.

Le développement de systèmes communicants embarqués critiques requiert donc celui de modèles formels. Dans la pratique industrielle actuelle, ces modèles sont souvent hétérogènes et multiples. Il s’agit :

  • d’une part de modèles fonctionnels qui ont pour objet de décrire comment le système doit se comporter, de garantir que son comportement est conforme à ses spécifications et de dériver correctement son implémentation à partir de ces dernières. Parmi les formalismes utilisés pour construire ces modèles, on peut citer les states-charts, les langages formels comme Lustre et Esterel (et les outils associés comme Scade, etc), les modèles communicants asynchrones comme CSP, DCS, ASM,  la méthode B (et outils associés comme Atelier B, FDR, etc.).

  • D’autre part de modèles dysfonctionnels qui ont pour objet d’analyser et de réduire la fréquence d’incidents ou d’accidents liés à l’exploitation d’un système complexe. Ces modèles sont typiquement des arbres de défaillance ou des schémas blocs-diagrammes de fiabilité.

Jusqu’à présent, ces deux types de modèles ont été développés séparément et souvent par des équipes différentes, avec des cultures « métiers » différentes (ingénieurs de conception d’une part, fiabiliste de l’autre). Les formalismes utilisés dans l’un et l’autre cas sont souvent trop lointains pour être connectés de manière évidente. Le passage du fonctionnel au dysfonctionnel ou leur cohabitation dans un système réel se fait donc aujourd’hui encore largement de manière ad-hoc et souvent « à la main », avec tous les risques et surcoûts que cela comporte en cas de dysfonctionnement. Il faut en particulier souligner que le moindre changement dans la spécification fonctionnelle du système demande de revoir souvent entièrement les modèles dysfonctionnels associés, d’où un coût de maintenance important et une possibilité d’adaptation réduite des systèmes tant pour leur évolution architecturale (réseaux, « scalabilité ») que pour leurs nouvelles fonctionnalités (répartition, évolution, modularité, etc.).

La conséquence est que l’on peut observer un décalage préjudiciable entre les modèles fonctionnels et les modèles dysfonctionnels d’un même système. Leur intégration est donc un enjeu technologique majeur pour la complexité croissante des systèmes communicants et embarqués critiques du futur et leurs applications.

Elle est d’actualité pour au moins quatre raisons :

  • La demande de la société et la pression économique pousse à intégrer les exigences de sûreté de fonctionnement au plus tôt dans le cycle de vie des systèmes embarqués critiques, c’est à dire dès leur spécification fonctionnelle initiale.

  • Les exigences de sûreté de fonctionnement se doublent d’exigences de disponibilité des services. Ces dernières ne peuvent être atteintes que par une analyse fine des modes de fonctionnement dégradés du système.

  • L’évolution récente des formalismes de modélisation fonctionnels et dysfonctionnels rend aujourd’hui possible leur intégration grâce aux travaux que nous menons dans la région

  • Les modèles sont aujourd’hui réalisés dans le cadre d’ateliers logiciels complexes. Ces progiciels facilitent l’intégration des différentes techniques.

Le projet a pour objectif de démontrer la faisabilité de cette intégration, tant d’un point de vue fondamental que sur la base de cas d’étude industriels.


Objectifs de Cosyc

Ce projet vise, dans une première étape, le développement d'une méthodologie d'aide à la conception de systèmes hybrides, basée sur des techniques de modélisation utilisant à la fois la Méthode B et le langage AltaRica.

Du point de vue de la modélisation, il s'agit d'étudier des formalismes hétérogènes capables de permettre une spécification aisée des systèmes complexes et interactions des comportements les constituant et basés sur les deux types de méthodes.

Du point de vue de l'analyse, le premier problème qui se pose de manière tout à fait naturelle est celui de la consistance des modèles. Le principal intérêt du projet est la vérification des propriétés de sûreté tout au long du processus de développement d’un système communicant complexe.

Bien entendu, la recherche d'une telle méthodologie hétérogène sera guidée par des études de cas issues des domaines d'application rencontrés par les partenaires industriels et métiers spécifiques du Pôle SCS (transports, santé, risques, sécurité).

Dans une seconde étape, nous envisageons la mise en œuvre de ces techniques dans le cadre d'un prototype d'Atelier Mixte permettant l’utilisation cohérente des deux approches.

 

  

ClearSy System Engineering - Parc de la Duranne - 320 av. Archimède - Les Pléïades III Bat A
13857 AIX EN PROVENCE CEDEX 3
Tel : 04 42 37 12 70 - Fax : 04 42 37 12 71 -
contact@clearsy.com