Objectifs
Au terme de ce cours, la personne étudiante sera en mesure de/d’ :
• Définir les objectifs de la vérification formelle et de test des logiciels embarqués critiques
• Décrire les méthodes de vérification formelle et de test des logiciels embarqués critiques
• Connaitre les exigences des normes de développement des logiciels embarqués critiques pour la vérification formelle et le test
• Concevoir des plans de vérification formelle et de test
• Effectuer la vérification formelle et le test des logiciels embarqués à l’aide d’outils adéquats
Contenu
Cycle de vie, processus et outils de développement des logiciels embarqués. Notions de défauts, erreur et défaillance. Propriétés structurelles et fonctionnelles (sureté, vivacité, etc.) des logiciels embarqués. Objectifs, avantages et limites de la vérification formelle et du test. Exigences de vérification formelle et de test. Normes de l’assurance qualité des logiciels embarqués critiques : DO 178C/DO-333, ISO 26262, etc. Méthodes et outils de vérification formelle: model-checking, analyse statique, méthodes à base de résolution de contraintes. Test : approche d’élaboration et de maintenance des requis de test et des cas de test, couverture des requis de test, génération manuelle et automatique des données de test, maintenance des tests. Outils de vérification formelle et de test. Études de cas de vérification formelle et de test des logiciels dans les secteurs appliqués (Transport, du manufacturier, internet des objets, etc). Ce cours comporte des séances obligatoires de travaux dirigés (TD).