Polyspace Code Prover

Principales fonctionnalités

  • Absence prouvée de certaines erreurs d’exécution dans les codes C et C++
  • Mise en évidence des erreurs d’exécution par un code couleur directement dans le code
  • Calcul des plages de valeur des variables et des valeurs de retour de fonction
  • Identification des variables dépassant des limites de plage définies
  • Métriques pour le suivi de la conformité aux objectifs de qualité logicielle
  • Interface Web fournissant des métriques de code une vue d’ensemble de la qualité du logiciel
  • Assistance à la revue de code avec classification des résultats et des erreurs d’exécutions détéctées
  • Affichage graphique des lectures et écritures de variables
Run-time error results displayed by Polyspace Code Prover.

Affichage des résultats d’erreur d’exécution par Polyspace Code Prover.

Vérification du logiciel embarqué C et C++

Polyspace Code Prover vérifie le code de logiciel embarqué C et C++ devant fonctionner aux niveaux de qualité et de sécurité les plus élevés. Il utilise une technique des méthodes formelles appelée interprétation abstraite afin de produire des résultats de vérification sains. Polyspace Code Prover identifie l’emplacement des erreurs d’exécution ainsi que le code prouvé comme étant exempt d’erreurs d’exécution. Vous utilisez Polyspace Code Prover dans le cadre d’un processus d’assurance qualité soutenu afin de vérifier l’intégralité des valeurs d’entrées, chemins et variables. Polyspace Code Prover utilise un code couleur pour indiquer le statut de chaque élément du code. Il s’intègre à Simulink® et offre la traçabilité des résultats d’exécution au niveau du code jusqu’aux modèles Simulink.

Avec Polyspace Code Prover, vous pouvez :

  • Prouver la qualité de votre code : vérifier que votre code est exempt d’erreurs d’exécution
  • Obtenir des résultats exempts de faux négatifs : toutes les potentielles erreurs d’exécution sont intégralement identifiées
  • Accroître votre confiance dans la qualité du code : code prouvé par des mesures par rapport à un code non prouvé

Vous pouvez accéder à Polyspace Code Prover en ligne de commande, depuis une interface utilisateur graphique ou via des plugins Visual Studio® et Eclipse™. Il permet de prendre en charge toutes les activités critiques inhérentes au flux du développement logiciel, dont les suivantes :

  • Détection des erreurs d’exécution
  • Preuve de l’absence de certaines erreurs d’exécution
  • Détermination des plages de valeur de variables et assurance du respect des limites de plage
  • Assurance du respect des objectifs de qualité logicielle
  • Traçabilité des erreurs d’exécution jusqu’aux blocs Simulink ou aux modèles IBM® Rational® Rhapsody®
  • Création d’artefacts de certification

Polyspace Code Prover fonctionne avec Polyspace Bug Finder pour détecter les défauts et vérifier la conformité aux régles de codage. Ces produits offrent une capacité d’analyse statique complète pour une utilisation dès les premières étapes du développement, couvrant la détection d’erreurs, le contrôle des règles de codage et la preuve d’ erreurs d’exécution. Cette capacité assure la fiabilité du logiciel embarqué qui doit respecter les plus hauts niveaux de qualité et de sécurité.

Vous pouvez accélérer et déporter la vérification du code à un cluster d’ordinateurs en soumettant des tâches de vérification grâce à Parallel Computing Toolbox™ et MATLAB Distributed Computing Server™.

Détection des erreurs d’exécution

Polyspace Code Prover utilise l’interprétation abstraite avec l’analyse statique de code afin de prouver, d’identifier et de diagnostiquer des erreurs d’exécution telles que les dépassements (overflows), les divisions par zéro et les débordements pointeur. Cette technique vérifie complètement et intégralement toutes les conditions d’exécution et fournit automatiquement un diagnostic de preuve, d’échec, d’inaccessibilité ou d’absence de preuve pour chaque opération de code. Dans les résultats de vérification produits par Polyspace Code Prover, chaque opération C ou C++ est repérée par un code couleur indiquant son statut :

Vert: fiabilité prouvée, sans aucune erreur d’exécution
Rouge: erreur prouvée chaque fois que l’opération est exécutée
Gris: inaccessibilité prouvée / code mort (peut indiquer un problème fonctionnel)
Orange: opération non prouvée pouvant présenter une erreur sous certaines conditions

Color-coded run-time error attributes identified by Polyspace Code Prover.

Attributs d’une erreur d’exécution identifiée par Polyspace Code Prover.

Les erreurs détectées comprennent :

  • Overflows, underflows, divisions par zéro et autres erreurs arithmétiques
  • Débordements de tableau et pointeurs déréférencés illégalement
  • Conditions toujours vraies / fausses
  • Membres de classe non initialisées (C++)
  • Accès en lecture à des données non initialisées
  • Accès un pointeur null this (C++)
  • Code mort
  • Erreurs dynamiques liées à la programmation objet, à l’héritage et à la gestion des exceptions (C++)

Affichage des informations sur les plages de valeur

Polyspace Code Prover suit le contrôle et le flux de données au sein du logiciel et affiche les informations de plage associées à des variables et à des opérateurs. En passant votre curseur sur un opérateur ou une variable, une info-bulle affiche les informations de plage. La méthode formelle appelée interprétation abstraite permet de déterminer des informations de plage précises afin de prouver que le logiciel est exempt de certaines erreurs d’exécution. Vous pouvez utiliser les informations de plage pour déboguer votre logiciel ou pour vous assurer que certaines variables ou opérations ne violent pas des limites de plage spécifiques.

Dans l’exemple ci-dessous, Polyspace Code Prover a établi que l’opération de division fait intervenir une plage de -1701 à 3276 pour l’opérande de gauche, tandis que l’opérande de droite vaut 9. Le résultat de la division est compris entre -189 et 364.

Tooltip displaying the possible ranges for all run time conditions.
Affichage par l’info-bulle des plages possibles pour toutes les conditions d’exécution.

Vous pouvez également visualiser le flux de contrôle à l’aide l’arbre d’appel et des graphiques du flux d’appel.

Call flow graph displaying the order of function calls in an interprocedural analysis.

Ordre des appels de fonction dans une analyse inter-procédures.

Suivi des métriques de qualité logicielle

Vous pouvez définir un modèle qualité centralisé pour suivre les erreurs d’exécution, la complexité du code et les violations des règles de codage. À l’aide de ces métriques, vous pouvez suivre votre progression vers des objectifs de qualité logicielle prédéfinis depuis la première itération jusqu’à la version finale. En mesurant le taux d’amélioration de la qualité de code, Polyspace Code Prover permet aux développeurs, testeurs et gestionnaires de projet de cibler un niveau de code d’excellente qualité et de le réaliser.

Software quality metrics displayed via web browser.

Affichage des métriques de qualité logicielle via le navigateur Web.

Traçabilité des résultats de vérification du code jusqu’aux modèles Simulink

Vous pouvez utiliser Polyspace Code Prover pour vérifier du code généré ou du code mixte (contenant à la fois du code généré et du code manuel). Les résultats des défauts identifiés dans le code généré automatiquement sont retracés jusqu’au modèle dans Simulink. Vous pouvez identifier les parties du modèle qui sont fiables et corriger les problèmes de conception à l’origine des erreurs dans le code. De plus, vous pouvez identifier les potentiels problèmes entre l’interface du code généré et le code écrit manuellement. Ainsi, le mélange de codemanuel contenu dans une S-Function avec du code généré peut être source d’erreur d’exécution si les plages de valeurs des signaux à l’interface sont erronées.

Polyspace Code Prover assure également la traçabilité des résultats de vérification de code vers les blocs dSPACE® TargetLink® et les modèles IBM Rational Rhapsody.

Tracing code verification results to the Simulink model.

Traçabilité des résultats de vérification du code jusqu’au modèle Simulink.

Automatisation du processus de vérification du code

Vous pouvez utiliser Polyspace Code Prover dans le cadre d’un processus d’intégration continue en l’incorporant à votre processus de déploiement. Vous pouvez automatiser la planification de la tâche de vérification et mettre en place des notifications par e-mail. Vous pouvez configurer Polyspace Code Prover pour qu’il gère la planification de tâches de vérification sur un cluster de calcul (à l’aide de MATLAB Distributed Computing Server) et recevoir des notifications par e-mail à l’arrivée des résultats. Ces résultats contiennent les écarts par rapport à la précédente version de votre code, que le serveur calcule automatiquement.

Vous pouvez définir la fréquence de ces analyses, le modèle qualité à appliquer à une portion donnée de votre base de code et les e-mails que vos utilisateurs reçoivent à la parution des résultats. De même, vous pouvez définir les caractéristiques du processus de déploiement que les vérifications automatisées doivent prendre en compte.

Création d’artefacts de certification

Vous pouvez utiliser Polyspace Bug Finder et Polyspace Code Prover avec IEC Certification Kit (for IEC 61508 and ISO 26262) et DO Qualification Kit (for DO-178B) dans le processus de certification, pour les projets devant répondre à ces normes de l’industrie.

Les rapports et artefacts montrent la qualité finale du code, mettent en évidence les sections qui ont été révisées, génèrent les métriques de code et documentent l’application des règles de codage et le statut des erreurs d’exécution. Vous pouvez créer ces rapports aux formats PDF, HTML, RTF ou à d’autres formats.

DO Qualification Kit contents.

Disponibilité des kits de certification et de qualification.

Améliorer la qualité de votre logiciel embarqué avec Polyspace

Visionner le webinar