A l’occasion de la conférence ABZ 2014, un tutoriel sur la validation formelle des données est organisé à l’ENSEEIHT ainsi que des ateliers.
Le tutoriel aura lieu le 3 juin 2014 de 14h00 à 17h30.
Au cours de ce tutoriel, les principes de la validation formelle des données seront exposés (concepts clés, langage mathématique pour exprimer les propriétés, chaîne d’outils) et appliqués à des exemples simples couvrant différents aspects.
Télécharger les slides TéléchargerLe programme est le suivant :
- Introduction
- La validation formelle des données en quelques mots
- Exemples industriels
- L’approche : langage mathématique et outils de vérification
- Etudes de cas
Si vous souhaitez assister au tutoriel ou obtenir plus d’informations sur cet événement, veuillez contacter thierry.lecomte@clearsy.com.
Introduction
Dans le cadre des projets Rodin et DEPLOY financés par l’UE, un modèle de données sur la topologie des voies a été élaboré afin de vérifier les architectures des systèmes ferroviaires réels. Ce modèle de données est d’une importance capitale, car il s’agit d’une condition préalable essentielle pour que les logiciels se comportent en toute sécurité (par exemple, si un signal est mal positionné, une collision est susceptible de se produire). La validation de données concrètes est complexe en raison de la grande quantité de données (50 à 100 000 cellules Excel, modifiées plusieurs fois au cours du développement) et du nombre de vérifications à effectuer (jusqu’à 1 000 règles, exprimant des propriétés complexes basées sur des graphes) sur cet ensemble de données. Par conséquent, la vérification humaine prend du temps et est sujette à de nombreuses erreurs. L’automatisation du processus, en formalisant le modèle de données avec le langage mathématique de la méthode B et en effectuant la vérification avec le model-checker et le solveur de contraintes (ProB), a permis de réduire considérablement le temps de vérification, qui est passé de plusieurs mois à quelques minutes.