Séminaires
Séminaire du 27 mai 2016
Lieu
CNAM : comment y aller
Programme
14h00-15h00: Cécile Braunstein (LIP6/UPMC), "Application du Model-based Testing dans le projet OpenETCS (Open European train Control System)"
Abstract : 
Le Model-based testing est une approche prometteuse pour faire face à la
complexité des systèmes d'aujourd'hui. Il déplace l'effort
traditionnellement mis dans l'écriture de la spécification des cas de
tests sur la réalisation d'un modèle comportemental du système. De ce
modèle, les cas de tests peuvent alors être automatiquement générés.
Dans cet exposé je présenterai l'application du model-based testing
dans le cadre du projet OpenETCS (2012-2015). Ce projet avait pour
objectif de proposer une chaîne d'outils open-source pour la
conception, la validation et la vérification du système européen de
contrôle des trains (ETCS).
15h00-15h30 : Amira Methni (CEDRIC/CNAM), "Méthode de spécification de logiciel système critique couplée à une démarche de vérification formelle"
Abstract : Les logiciels critiques doivent offrir une garantie de sûreté de fonctionnement pour lesquels un dysfonctionnement peut avoir des conséquences graves. Les méthodes formelles fournissent des outils permettant de garantir mathématiquement l'absence de certaines erreurs. Mais l'application de ces méthodes sur un code système bas niveau se heurte à des difficultés d'ordre pratique et théorique. Les principales difficultés concernent la prise en compte des aspects bas niveau ainsi que la complexité de leur vérification.
Dans ce travail, nous proposons une méthodologie pour la spécification et la vérification par model-checking de ce type de systèmes, en particulier, ceux implémentés en C. Cette méthodologie est basée sur la traduction de la sémantique de C en TLA+, un langage de spécification formel adapté à la modélisation de systèmes concurrents. Nous proposons un modèle de mémoire et d'exécution d'un programme concurrent en TLA+. En se basant sur ce modèle, nous décrivons un ensemble de règles de traduction d'un code C en TLA+ que nous avons implémenté dans un outil, appelé C2TLA+. Nous montrons comment ce modèle peut s'étendre pour gérer la synchronisation entre plusieurs processus. Pour réduire la complexité du model-checking, nous proposons une technique permettant de réduire significativement la complexité de la vérification. Nous avons appliqué la méthodologie proposée sur un cas d'étude réel issu de l'implémentation d'un micronoyau industriel, sur lequel nous avons vérifié un ensemble de propriétés fonctionnelles. L'application de la réduction a permis de réduire considérablement le temps de la vérification, ce qui la rend utilisable en pratique.