Séminaire R-D : Un cadre automatisé pour la vérification et la génération de tests pour des contrôleurs embarqués

Séminaire R-D : Un cadre automatisé pour la vérification et la génération de tests pour des contrôleurs embarqués
10/02/15 11h00
CRIM (405, avenue Ogilvy, bureau 101)

Par Guillaume Langelier et Omer Nguena Timo, chercheurs postdoctorants dans l’équipe Modélisation et développement logiciel avancé du CRIM.

Résumé :
Les contrôleurs numériques sont une partie importante des systèmes critiques. Ces contrôleurs sont des systèmes temps-réel réactifs qui activent des commandes et des fonctionnalités. L’activation des commandes de contrôle se fait via l’exécution de tâches périodiques non préemptibles et peut nécessiter de longues séquences d’entrées. Vérifier et générer automatiquement les tests contribue à détecter des disfonctionnements et à augmenter la confiance vis-à-vis des contrôleurs. Dans cet exposé, nous présentons et évaluons un cadre pour la vérification du code C des contrôleurs et une application à la génération automatique des tests. Notre cadre intègre le « bounded model-checker » CBMC et Frama-C. CBMC permet d’analyser du code C et de vérifier des propriétés classiques de sûreté. Cependant, il ne s’adapte pas bien à l’analyse du code complexe. L’élagage des parties du code à l’aide de Frama-C permet dès lors de réduire sa complexité et de faciliter ainsi son analyse. L’évaluation de notre approche sur du code C d’un contrôleur réel du groupe motopropulseur (Powertrain) d’une automobile montre que notre cadre peut aider à la production de tests dans un contexte industriel, bien qu’il ne puisse pas s’adapter à du code complexe invariant à l’opération d’élagage.


Les séminaires scientifiques sont donnés par des experts de renommée internationale, des professeurs d'université avec lesquels le CRIM collabore, le personnel de R-D du CRIM et ses boursiers de 2e et 3e cycles. Au programme, des présentations conviviales sur les dernières avancées scientifiques et technologiques. Ouvert à tous.

Inscription : Carmen.Robert@crim.ca ou 514 840-7992.
Conférence gratuite. Mercredi, le 10 février 2015, de 11 h à 12 h.
Au CRIM, 405, avenue Ogilvy, bureau 101, Montréal.

  • #Bientôt ???? Le CRIM présentera le projet Application des technologies vocales aux langues autochtones le 19 novembre… https://t.co/FnO5IKw79H
  • Tom Landry RT @Tom_Landry_: Ce fût un réel plaisir que de partager ma vision de l'avenir de la géomatique. Et que dire des mots-clés sélectionné par l…