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™.

Point suivant: Détection des erreurs d’exécution

Essayer Polyspace Code Prover

Obtenir une version d'évaluation

Automatiser et optimiser la vérification et le test de logiciel embarqué

Visionner le webinar