Contact

Travaux R&D (Recherche & Développement)

CLEARSY mène des travaux de Recherche & Développement dans différents cadres : des projets financés (Europe, France ou région) et des projets internes. Le tableau ci-dessous retrace les derniers projets de recherche publics auquel CLEARSY a participé de manière active.

LES THÉMATIQUES

CES PROJETS DE RECHERCHE PERMETTENT D’ABORDER DES THÉMATIQUES NOUVELLES ET D’APPROFONDIR DES SUJETS INNOVANTS :

LA GESTION DES EXIGENCES

La gestion des exigences se fait traditionnellement au travers de la traçabilité entre documents amonts et modèles B. Un outil dédié permet de lier les exigences d’un document au format Word avec le contenu d’un projet B et d’en calculer la traçabilité au cours des évolutions des exigences et/ou des modèles B. Les vérifications réalisées sont toutefois purement textuelles (on vérifie la présence d’une croix dans une case) alors qu’un traitement sémantique serait nécessaire. Des travaux devraient être initiés avec le LACL et l’IRISA afin de fournir une sémantique à un modèle de buts « à la KAOS » puis de réaliser une véritable preuve de couverture.

LE PROCESSUS DE RAFFINEMENT AUTOMATIQUE

Le raffinement automatique permet de diminuer significativement le temps de développement d’un logiciel B grâce à l’automatisation du processus et à un corpus extensible de règles de raffinement. L’écriture de règles et la résolution des conflits de raffinement nécessite toutefois des compétences expertes. La capacité de pouvoir prouver la validité d’une règle de raffinement, permettant ainsi d’admettre les obligations de preuve associées, est un premier axe d’amélioration. L’optimisation des algorithmes de raffinement actuels devrait par ailleurs permettre de traiter de manière entièrement automatique les conflits de raffinement (par exemple, une variable implémentée dans deux composants différents). Un stage relatif à ce dernier thème est proposé.

L’AUTOMATISATION ET NIVEAU DE CONFIANCE DU PROCESSUS DE PREUVE AUTOMATIQUE

La preuve mathématique de modèles B permet d’éviter les tests unitaires et une grande partie des tests d’intégration du logiciel résultant. Cette preuve mathématique est un processus non entièrement automatisé (une intervention humaine est nécessaire pour compléter certaines démonstrations) qui repose sur un seul outil (validé grâce à d’autres outils de preuve ainsi que grâce à des expertises humaines). La connexion à d’autres outils de preuve permet d’augmenter à la fois le taux de preuve automatique (diminuer les interventions humaines) et le niveau de confiance en les résultats (quand deux outils, développés avec des technologies différentes et par des équipes disjoints, arrivent de manière concomitante à la même conclusion positive). Cette connexion est en cours dans le cadre du projet ANR BWare.

LA SÉCURISATION DE LA GÉNÉRATION DE CODE

Le développement de programmes sécuritaires avec B nécessite non seulement de prouver que les implémentations sont conformes à leurs spécifications mais aussi de s’assurer que le code compilé, obtenu après traduction vers un code source puis compilation, ne peut pas induire de comportement antisécuritaire. Pour des cibles à haut niveau de sûreté, il s’agit d’utiliser des techniques de diversification et de redondance (un même modèle B est utilisé pour produire, grâce à deux générateurs de code différents, deux codes sources qui seront compilés puis exécutés sur deux calculateurs différents. Cette approche nécessite de développer deux outils de traduction qui devront être développés et validés par deux équipes différentes. Une alternative consiste à produire un code intermédiaire (IR LLVM) grâce à un seul générateur de code sur lequel reposera tout l’effort de développement et de validation, puis à générer le code source cible grâce aux générateurs de code développés par la Communauté. Des travaux sont réalisés en ce sens avec l’UFRN. Enfin la production de code binaire à partir de modèles B permet de supprimer l’étape de compilation et donc un niveau de vérification. Une expérimentation grandeur nature a lieu concernant la génération de code HEX pour des microcontrôleurs PIC.

L’ADAPTATION DE L’APPROCHE SYSTÈME À LA CONCEPTION DE CIRCUITS MICRO-ÉLECTRONIQUES

L’Atelier B supporte le B événementiel pour la description de systèmes. Il a notamment été utilisé par NYCT pour démontrer la sécurité du CBTC de la ligne 7 du métro de New-York. Des travaux communs avec STMicroelectronics ont permis de montrer la faisabilité technique de la spécification système et de la production de modèles VHDL à partir de modèles B événementiel. Des travaux complémentaires doivent être engagés en 2014 afin de pouvoir asseoir les bases scientifiques de l’approche et industrialiser le générateur de code.

L’EXTENSION DE LA VALIDATION FORMELLE DE DONNÉES CONSTANTES

La validation formelle de données constantes est appliquée aujourd’hui par la quasi intégralité des acteurs du monde ferroviaire, notamment pour la validation des données de voie. Elle permet de vérifier que le paramétrage d’un système, au sens le plus large du terme, est acceptable vis à vis de règles définissant cette acceptabilité. Les règles sont formalisées grâce au langage mathématique de B et la vérification d’acceptabilité réalisé par le model-checker ProB. Pour des besoins de sécurisation de la décision, un deuxième outil de vérification, PredicateB++, permet de confirmer une décision positive de ProB. Cette approche est en cours d’expérimentation dans d’autres domaines sécuritaires tels que l’aéronautique et le nucléaire. Le langage de modélisation des propriétés est étendu alors que les interfaces d’entrée et de sortie sont diversifiées.

LA CONNEXION DES MODÉLISATIONS AVEC D’AUTRES OUTILS ET MÉTHODES D’ANALYSE

Les modèles formels B et B événementiel permettent de vérifier formellement la correction d’un logiciel ou d’un système d’un point de vue fonctionnel. Cette vérification doit être couplée à d’autres techniques et outils afin d’obtenir un meilleur niveau de confiance: animation formelle de modèle (ProB, BMotionStudio), simulation hétérogène distribuée, analyse temporelle, etc.

Voir nos travaux de R&D

Copy link
Powered by Social Snap