Accueil > FR > Recherche > Projets > FAUST    (EN)


FAUST

Formal Analysis Using Specification Tools

L’atelier FAUST assure le développement de cahiers des charges de haute qualité, notamment dans le domaine de systèmes complexes ayant des aspects critiques. Il fournit des outils de vérification, validation et générations de jeux de test centrés sur les exigences de tels systèmes. Le niveau d’analyse formel est rendu accessible par son intégration naturelle dans des notations textuelles et graphique, de même que la présence d’un outil d’animation exploitant des visualisations propres au domaine étudié. L’intégration dans des méthodes et chaînes d’outils industrielle a également été traitée en détail.

Objectifs du projet

L’ingénierie des exigences est une étape cruciale dans le développement d’un système informatique. Plus particulièrement dans le cadre de systèmes ayant des dimensions il est impératif d’atteindre des niveaux de qualité élevés.

L’objectif est d’offrir une gamme intégrée d’outils d’analyse de cahiers des charges permettant la production de cahiers des charges de haute qualité pour des logiciels industriels complexes. Cet outillage exploite la formalisation des exigences dans une modélisation orientée buts et propose des raisonnements rigoureux sur ces modèles dont les principaux sont :

  • La vérification : s’assurer que les exigences sont consistantes, non ambiguës, robustes par rapport à des menaces.
  • La validation : s’assurer que les exigences correspondent aux souhaits des parties prenantes.
  • L’acceptation : s’assurer que le système délivré correspond bien aux exigences formulées dans le cahier des charges.

Afin de rendre les outils accessibles, l’atelier met en œuvre des technologies formelles automatisée de model-checking et de satisfiabilité qui peuvent produire des scénarios explicatifs des défauts détectés. Des outils appropriés de visualisation par animation utilisant des notations graphiques familières des parties prenantes sont également mis en œuvre.

Résultats du projet

- Atelier logiciel de modélisation et d’analyse formelle des exigences de systèmes critiques ;
- Outils et services pour l’exploitation de l’atelier auprès d’entreprises ayant des besoins critiques.

Plus-value du projet pour les entreprises

Possibilité de formaliser intelligemment les parties critiques d’un système dès le stade du cahier de charges, permettant de détecter rapidement des défauts ou erreurs qui conduiront à des problèmes généralement très coûteux à résoudre plus tard dans le cycle de développement. Cette formalisation se concentre sur les parties identifiées comme critiques et s’intègre dans des modèles semi-formels textuels et graphiques qui en préservent la lisibilité. De même les outils d’animations basés sur des notations du domaine permettent une validation par toutes les parties prenantes.

Meilleur lien des processus de développement industriels avec la phase de définition des exigences : traçabilité forte des modèles dans les phases aval, possibilité de dérivation de certains de ces modèles (architecture, modèles de données…). Ces liens se situent dans une approche d’ingénierie basée sur les modèles et leur transformation.

Intégrabilité dans les chaînes d’outils industriels, notamment sur via l’outil commercial Objectiver (Respect-IT) et de la base de la plateforme Eclipse. Les méthodes AADL et B/Event-B sont en particulier traités au sein de projets spécifiques.

Application industrielle validée par des expérimentations dans divers domaines tels que la sécurité (Grid, eID…) et la sûreté de fonctionnement (transport ferroviaire, contrôle aérien…).

Partenaires