Polyspace Code Prover

Prouvez l'absence d'erreurs run-time dans les logiciels

Polyspace Code Prover™ est un outil d'analyse statique permettant de prouver l'absence d'overflow, de division par zéro, de débordement de tableaux et autres erreurs run-time dans du code source C et C++. L'exécution du programme, l'instrumentation du code ou des cas de test  ne sont pas nécessaires. Polyspace Code Prover utilise l'analyse sémantique et l'interprétation abstraite basée sur des méthodes formelles pour vérifier le comportement interprocédural, de contrôle et de flux de données du logiciel. Vous pouvez l'utiliser pour vérifier du code écrit à la main, du code généré ou une combinaison des deux types. Chaque instruction de code est repérée par un code couleur indiquant si elle est exempte de toute erreur run-time, avérée défaillante, inaccessible ou non prouvée.

Polyspace Code Prover affiche les informations de plage de valeur pour les variables et les valeurs retournées par les fonctions, et prouver quelles variables dépassent les limites de plage définies. Les résultats de vérification du code peuvent servir à effectuer le suivi des métriques de qualité et à vérifier la conformité à vos objectifs de qualité logicielle. Polyspace Code Prover peut être utilisé avec l'IDE Eclipse™ pour vérifier du code sur votre ordinateur de bureau.

Le support des normes industrielles est assuré via IEC Certification Kit (IEC 61508 et ISO 26262) et DO Qualification Kit (DO-178).

En savoir plus:

Vérifier le code avec les mathématiques formelles

Atteignez des niveaux de qualité et de sécurité élevés sans faux négatifs.

Prouver l'absence d'erreurs run-time critiques

Identifiez les opérations de code C/C++ et Ada qui ne rencontreront aucune erreur run-time, quelles que soient les conditions d'exécution.

Détection des erreurs run-time

Détecter des erreurs impossibles à repérer avec d'autres méthodes de test

Analysez toutes les chemins du code par rapport à toutes les entrées possibles, sans exécuter le code.

Hiérarchie d'appels.

Créez des artefacts pour la certification

Réalisez le processus de certification du projet basés sur les normes de l'industrie.

DO Qualification Kit.

Comprendre et améliorer le code

Consacrez moins de temps aux revues, au débogage et aux tests de robustesse du code.

Comprenez la cause principale des problèmes et améliorez le design

Examinez le contrôle et le flux de données au sein du logiciel, et affichez les informations de plage associées à des variables et à des opérateurs.

Affichage par l'info-bulle des plages possibles pour toutes les conditions d'exécution.

Évitez les comportements logiciels indésirables

Trouvez toutes les sections de code qu'aucun chemin d'exécution ne permet d'atteindre, et identifiez les erreurs de logique et de structure du programme.

Identification du code mort.

Tracez les résultats de vérification du code jusqu'aux modèles Simulink

Vérifiez du code généré et assurez la traçabilité des résultats jusqu'au bloc source dans le modèle Simulink.

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

Automatisation de la vérification du code à l'aide de Polyspace Code Prover Server

Favorisez l'intégration continue en analysant les modifications de code de manière précoce et fréquente.

Automatiser le processus de vérification du code

Utilisez Polyspace Code Prover Server™ pour exécuter le moteur d'analyse statique Polyspace Code Prover sur une machine de type serveur avec des outils d'automatisation intégrés, tels que Jenkins et Bamboo.

Automatiser le processus de vérification du code.

Notifiez et publiez les résultats pour une revue collaborative

Assignez automatiquement les défauts aux responsables des composants, envoyez des notifications par email et importez des résultats dans Polyspace Code Prover Access afin de trier et de résoudre les problèmes.

Envoyez des notifications par email avec les résultats  de Polyspace Code Prover.

Revue collaborative avec Polyspace Code Prover Access

Partagez les résultats de vérification et les métriques de qualité avec l'équipe de développement logiciel.

Examinez les résultats de Polyspace Code Prover afin de trier et de résoudre les problèmes

Polyspace Code Prover Access™ offre une interface web pour les résultats de vérification de code Polyspace et les métriques de qualité stockés dans une base de données centrale. Utilisez les outils de navigation dans votre navigateur web pour étudier les résultats de vérification du code, qui s'affichent à côté du code.

Détection des erreurs run-time

Objectifs de qualité des projets et du logiciel

Les tableaux de bord affichent des informations que vous pouvez utiliser afin de surveiller la qualité du logiciel, l'état des projets, le nombre de défauts, les métriques de code et les objectifs qualité du logiciel.

Tableau de bord de vue d'ensemble du projet.

S'intégrer avec les outils de suivi de bugs que vous utilisez déjà

Utilisez l'interface web afin de créer et d'assigner des tickets dans des outils de suivi de bugs comme Jira.

Création d'un ticket.

Nouveautés

Mode de variables partagées

Réalisez une analyse Code Prover moins complète sur l’intégralité de l’application pour calculer uniquement l’utilisation et le partage des variables globales.

Support des compilateurs

Configurez facilement des analyses Polyspace pour du code compilé avec des compilateurs Cosmic.

Support de Simulink

Analysez du code généré en utilisant les boutons contextuels de la barre d’outils de l’éditeur Simulink.

Support de Simulink

Vérifiez du code personnalisé appelé depuis les blocs C Caller et des diagrammes Stateflow dans le contexte du modèle.

Reportez-vous aux notes de version pour en savoir plus sur ces fonctionnalités et les fonctions correspondantes.

Version d’évaluation

Bénéficiez d'une version d'évaluation de 30 jours.

Télécharger

Prêt à acheter ?

Obtenez les tarifs et explorez les produits associés.

Vous êtes étudiant ?

Obtenez la version étudiante des logiciels MATLAB et Simulink.

En savoir plus