Objectif: Se familiariser avec Polyspace Bug Finder et Code Prover au travers d'un exemple.

• Process de développement avec Polyspace
• Exemple simple de vérification
• Analyse des défauts et des erreurs d'exécution

Objectif: Vérifier du code qui ne respecte pas forcément la norme ANSI C en tenant compte de l'environnement d'exécution, et correction des défauts et des violations des règles de codage avec Bug Finder.

• Artefacts usuels d'un environnement d'exécution
• Gestion de code spécifique à un processeur
• Définition du contexte d'exécution
• Configuration en fonction de la cible matérielle
• Analyse et gestion des défauts Bug Finder
• Détection des violations de règles de codage

Objectif: Devenir compétent dans l'interprétation des résultats Polyspace Code Prover.

• Notions d'interprétation abstraite
• Analyse de l'arbre d'appel
• Navigation dans le code source
• Chemins d'exécution
• Plages de valeurs des variables
• Variable globale dans le code source

Objectif: Trouver les erreurs d'exécution à l'aide des diagnostics disponibles dans Polyspace Code Prover.

• Vue d'ensemble des points de contrôles de code source C
• Emplacement des points de contrôles dans le code source
• Description des points de contrôles
• Options utiles à la vérification

Objectif: Gestion des résultats de vérification qui contiennent un grand nombre de point de contrôle non-prouvés.

• Détermination de l'effort de vérification
• Revue rapide
• Revue sélective des oranges
• Configuration de la précision de vérification
• Priorisation des points de contrôle orange
• Revue des points de contrôle orange

Objectif: Apprendre comment Polyspace Code Prover gère le code manquant lors de la vérification, et comment modifier ce comportement pour produire des résultats plus significatifs.

• Vérification de robustesse et contextuelle
• Bouchonnage de fonction
• Spécification de plage de données
• Bouchonnage manuel

Objectif: Apprendre comment gérer les vérifications lorsque la complexité du code augmente, et comment interpréter et comparer l'analyse d'intégration avec l'analyse de robustesse.

• Gestion des modules de code
• Aanalyse des défauts d'intégration et violations des règles avec Bug Finder et Code Prover
• Import des commentaires

Objectif: Utiliser l'outil Web metrics pour partager et stocker les résultats des vérifications, et générer des rapports.

• Partage de résultats
• Utilisation de la vue Web metrics
• Définition et suivi des objectifs de qualité logicielle
• Création de documentation

Objectif: Revoir la procédure et les options utiles pour vérifier une application complète.

• Mettre en place la vérification d'une application
• Améliorer les résultats de la vérification d'une application
• Détecter les problèmes de concurrence
• Comparer l'analyse de robustesse et l'analyse contextuelle

Objectif: Revoir les acquis de la formation et utiliser Polyspace Code Prover directement sur un de vos projets. Les sujets peuvent être :

• Revue du processus de développement
• Intégration du workflow
• Installation Client/Serveur du logiciel
• Configuration d'un projet dans Polyspace
• Interprétation des résultats