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 de variables dépassant les limites de plage définies
  • Métriques de qualité pour le suivi de la conformité aux objectifs de qualité logicielle
  • Interface Web fournissant des métriques de code et l’état de qualité
  • Assistance à la revue de code avec classification des résultats et de l’état des erreurs d’exécution
  • Affichage graphique des lectures et écritures des variables

Affichage des résultats d’erreurs 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 s’agit d’un outil d’analyse statistique basée sur une méthode formelle appelée interprétation abstraite, et permettant afin d’obtenir des résultats de vérification sans faux négatif. 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 pouvez utiliser 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, de chemins et de variables. Polyspace Code Prover utilise un code de couleur pour indiquer l’état de chaque élément du code. Son intégration à Simulink® vous permet de gérer la traçabilité des résultats d’exécution au niveau du code jusqu’aux modèles Simulink.

Grâce à Polyspace Code Prover, vous pouvez réaliser les actions suivantes :

  • Prouver la qualité de votre code : vérifiez que votre code est exempt de toute erreur d’exécution.
  • Obtenir des résultats exempts de faux négatifs : toutes les erreurs d’exécution possibles sont intégralement identifiées.
  • Accroître votre confiance dans la qualité du code : quantifier la part de code prouvée comme exempte d’erreurs.

Vous pouvez accéder à Polyspace Code Prover à l’aide d’un appel de ligne de commande, via l’interface utilisateur graphique ou via des modules complémentaires de Visual Studio® et Eclipse™. Il vous permet de prendre en charge toutes les activités critiques inhérentes au flux de développement logiciel, dont les suivantes :

  • Détection des erreurs d’exécution comme les divisions par zéro
  • Preuve de l’absence de certaines erreurs d’exécution critiques pour la sécurité, comme les débordements de tableau
  • Détermination des plages de valeurs de variables et s’assurer du respect des limites de plage définies
  • Assurance du respect des objectifs de qualité pour les logiciels
  • 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 identifier les défauts critiques pour la sécurité dans votre code source, notamment la division par zéro ou le débordement de tableau. Il vous permet également de vérifier la conformité aux normes de codage, telles que MISRA. Ces produits offrent une capacité d’analyse statique complète pouvant être utilisée dès les premières étapes du développement et couvrant la détection des bugs, le contrôle des règles de codage et la démonstration de l’absence 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 sur 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 statistique du code pour prouver, identifier et diagnostiquer des erreurs d’exécution, telles que les dépassements d’entiers, les divisions par zéro et les débordements de tableau. Cette technique permet de vérifier toutes les conditions d’exécution possibles de manière approfondie et de fournir automatiquement un diagnostic de preuve, d’erreur, 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 état :

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 (peut indiquer un problème fonctionnel)
Orange : opération non prouvée pouvant présenter une erreur sous certaines conditions

Plusieurs types d’erreurs peuvent être détectés :

  • Dépassements d’entiers, underflows, division par zéro et autres erreurs arithmétiques
  • Débordements de tableau et de 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 nul (C++)
  • Code mort
  • Erreurs dynamiques liées à la programmation objet, à l’héritage et à la gestion des exceptions (C++)

Identification des attributs d’erreurs d’exécution par Polyspace Code Prover.


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. Une info-bulle affiche les informations de plage si vous passez votre curseur sur un opérateur ou une variable. 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, comme les divisions par zéro et les débordements de tableau. Vous pouvez utiliser les informations de plage pour suivre le contrôle et le flux de données de manière détaillée afin de déboguer votre logiciel, ou de vérifier la conformité de certaines variables ou opérations par rapport à 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.

Vous pouvez également visualiser le flux de contrôle à l’aide de l’arbre d’appel et des graphiques du flux d’appel, ou afficher les chemins d’accès pour vos données variables globales.

Explore gallery (3 images)


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é du code, Polyspace Code Prover permet aux développeurs, testeurs et gestionnaires de projet de cibler et de livrer du code d’excellente qualité.

Affichage des métriques de qualité du logiciel via un navigateur Web.


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 code manuel 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 dans l’interface sont erronées.

Polyspace Code Prover assure également la traçabilité des résultats d’exécution vers les blocs dSPACE® TargetLink® et les modèles IBM Rational Rhapsody.

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 planifie la publication des tâches de vérification sur un ordinateur du cluster (à 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 (IEC 61508 et ISO 26262) et DO Qualification Kit (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 du code et décrivent 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.

Disponibilité des kits de certification et de qualification.