Polyspace Code Prover analyse tous les chemins d'exécution par rapport à toutes les entrées possibles afin de prouver l'absence de certaines erreurs run-time telles que le dépassement de capacité, la division par zéro et l'accès hors limites aux tableaux dans le code C/C++. Il propose également des informations sur le contrôle et le flux de données et prouve la validité de l'accès concurrent aux variables globales partagées entre les tâches (threads).
Polyspace Code Prover utilise l'analyse statique par interprétation abstraite basée sur des méthodes formelles, produisant des résultats sans nécessiter l'exécution du programme, l'instrumentation du code ou des cas de test. Les résultats sont faciles à comprendre et exploitables : ils apparaissent directement dans le code source avec des résultats codés par couleur, des informations sur la plage des variables et une navigation dans le code. Vous pouvez utiliser Polyspace Code Prover sur n'importe quelle combinaison de code C/C++, écrit manuellement ou généré par Simulink ou un assistant d'IA.
Le support des normes industrielles est assuré via l'IEC Certification Kit (for IEC 61508 and ISO 26262) et le DO Qualification Kit (for DO-178).
Prouver l’absence d’erreurs run-time critiques
Analysez tous les chemins du code avec toutes les entrées possibles sans exécuter le code. Identifiez les instructions qui ne seront jamais associées à une erreur run-time, quelles que soient les conditions run-time, et trouvez d'autres instructions nécessitant votre intervention.
Améliorer le design du logiciel et la compréhension du code
Examinez les flux de contrôle et de données dans votre code C/C++, et consultez les informations sur les plages associées aux variables et aux opérateurs.
Optimiser le logiciel pour de meilleures performances
Supprimez le code défensif en identifiant les opérations sûres et sécurisées, telles que la division par zéro et les overflows. Détectez les branches du code qui ne sont accessibles par aucun chemin d'exécution. Trouvez les erreurs dans la logique et la structure du programme, et supprimez-les pour réduire l'empreinte mémoire.
Analyser l’utilisation des variables globales
Passez moins de temps à débugger les opérations de lecture/écriture sur des variables globales, comme les variables partagées par plusieurs tâches ou plusieurs threads.
Utilisez le graphe des accès concurrents pour comprendre les flux de contrôle et de données susceptibles de conduire à des situations d'accès concurrent aux données. Identifiez les variables globales inutilisées pour optimiser le code.
Support de certification
Créez les artefacts nécessaires pour finaliser le processus de certification aux normes industrielles. Certification réalisée par TÜV SÜD pour une utilisation avec les normes IEC 61508 et ISO 26262. Utilisez les rapports et les artefacts pour les processus DO-178C.
Intégration de Simulink et Stateflow
Exécutez une analyse sur le code généré et tracez vos résultats jusqu'aux blocs sources du modèle Simulink et aux graphiques Stateflow. Démarrez une analyse Polyspace® directement depuis l'environnement Simulink.
Analyse interactive sur desktop
Exécutez une analyse statique de code sur des projets logiciels complets ou des sous-ensembles. Utilisez l'outil desktop pour générer des rapports, puis examinez et triez les résultats.
Identifiez la cause première de bugs complexes en mode debug, en naviguant pas à pas dans chaque instruction qui conduit à une erreur run-time. Organisez et configurez vos projets, avec le support natif de plus de 60 compilateurs C et C++, et la configuration automatique de l'analyse Polyspace extraite du système de compilation du projet.
Test statique de sécurité des applications
Prouvez l'absence de vulnérabilités de sécurité critiques telles que les dépassements de mémoire tampon, l'accès à la mémoire et les dépassements numériques. Réduisez la nécessité du fuzzing en analysant le code sur l'ensemble des chemins du code et des entrées sans exécuter le code.
Ressources liées au produit :
Famille de produits Polyspace
Les produits Polyspace sécurisent les codes critiques en testant et en contrôlant la qualité du software tout au long du cycle de développement.
Polyspace Access
Identifier les défauts de codage, revoir les résultats de l'analyse statique et contrôler les métriques de qualité logicielle.
Polyspace Copilot
Assistant IA optimisé pour Polyspace.
Polyspace Test
Développer, gérer et exécuter des tests sur le code C et C++ de vos systèmes embarqués.
Polyspace as You Code
Identifiez les violations des normes de codage et les vulnérabilités logicielles dans votre IDE.
Polyspace Test Server
Exécutez des tests et analysez la couverture structurelle du code C/C++ sur les serveurs d'automatisation.
Polyspace Code Prover Server
Vérifiez de manière continue et exhaustive les instructions de code C et C++ critiques dans les pipelines CI.
Polyspace Bug Finder
Vérifiez les règles de codage, les normes de sécurité et les métriques du code, et trouvez les bugs.
Polyspace Client for Ada
Vérifiez de manière exhaustive les unités critiques des instructions Ada à l'aide de méthodes formelles.
Polyspace Bug Finder Server
Identifiez les défauts software et appliquez les règles de codage dans vos pipelines CI.
Polyspace Server for Ada
Vérifiez de manière continue et exhaustive les instructions de code Ada critiques dans les pipelines CI.
Polyspace Code Prover
Vérifiez de manière exhaustive les instructions C et C++ les plus critiques à l'aide de méthodes formelles.
FAQ sur Polyspace Code Prover
Polyspace Code Prover prouve l'absence d'erreurs d'exécution critiques telles que les dépassements de capacité, la division par zéro et les accès hors bornes aux tableaux dans le code C/C++. Il fournit également des vues architecturales telles que les graphes d'appels et l'utilisation des données globales pour aider à comprendre la structure du logiciel à partir du code.
Polyspace Code Prover utilise une analyse statique fondée sur des méthodes formelles pour explorer tous les chemins d'exécution et toutes les entrées du code C/C++ sans l'exécuter.
Polyspace Code Prover affiche les résultats directement dans le code source à l'aide d'annotations colorées indiquant si des opérations sont prouvées exemptes d'erreurs d'exécution, prouvées comme provoquant une erreur, inaccessibles ou non prouvées. Il fournit également des informations sur les plages de valeurs des variables et des valeurs de retour des fonctions pour faciliter l'analyse des causes racines.
Il contribue à améliorer la sécurité logicielle en prouvant l'absence de vulnérabilités critiques telles que les dépassements de tampon, les accès mémoire invalides et les dépassements de capacité numériques, sur tous les chemins d'exécution et toutes les entrées, sans exécuter le code.
Polyspace Code Prover utilise des méthodes formelles pour prouver de manière exhaustive l'absence d'erreurs d'exécution sélectionnées. Polyspace Bug Finder identifie les bugs, les violations des règles de codage et les métriques de qualité du code sur des projets complets lors de l'intégration et de la vérification. Polyspace as You Code exécute un sous-ensemble de l'analyse de Polyspace Bug Finder directement dans l'IDE pour aider les développeurs à détecter les problèmes au moment de l'écriture du code.
Polyspace Code Prover est utilisé de manière interactive via une interface utilisateur de bureau, tandis que Polyspace Code Prover Server est optimisé pour l'analyse automatisée dans les workflows d'intégration continue (CI) et le partage des résultats via Polyspace Access.
Oui, il peut analyser du code généré automatiquement, avec des résultats traçables jusqu'aux modèles Simulink et aux blocs dSPACE TargetLink. Lorsqu'il est exécuté depuis Simulink, l'analyse est configurée automatiquement en fonction du modèle et des paramètres de génération de code.
Il prend en charge les workflows de certification pour IEC 61508, ISO 26262, EN 50128, EN 50657, IEC 62304, ISO 25119 et DO 178C/ED 12C via des kits de certification et de qualification, avec des conseils supplémentaires pour ISO/SAE 21434 et Automotive SPICE.
Vous souhaitez en savoir plus sur le produit Polyspace Code Prover ?
Pour aller plus loin…
Navigation dans l'interface
ARTICLES GRATUITS
Articles sur Polyspace
Navigation dans l'interface
PRODUIT
