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).
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.
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.
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
Gestion des autorisations de projet
Créez et appliquez des stratégies d'autorisation d'accès aux projets
Support AUTOSAR
Vérifiez la divergence run-time entre les spécifications AUTOSAR et l'implémentation du code
Calcul de la taille de la stack
Déterminez l'utilisation de la stack maximale par un programme C et des fonctions individuelles
Configuration à partir d'un système de build
Générez automatiquement des modules de configuration Polyspace à partir d'un système de build
Configuration de la vérification de code multitâches
Spécifiez des tâches cycliques et des interruptions non préemptables directement en tant qu'options de vérification
Reportez-vous aux notes de version pour en savoir plus sur ces fonctionnalités et les fonctions correspondantes.
