Polyspace Code Prover

 

Polyspace Code Prover

Prouver l'absence d'erreurs run-time dans un logiciel

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.

Analyse d'impact

Suivez formellement et vérifiez l'impact d'une variable spécifiée, globale ou locale, sur d'autres variables ou sur des instructions spécifiques. Réalisez une analyse du signal pour répondre aux exigences du CARB concernant les logiciels OBD, puis démontrez la liberté d'interférence dans le contexte de la norme ISO 26262 et analysez l'effet des paramètres de calibrage. Dans le contexte de la sécurité des logiciels, réalisez une analyse de contamination et suivez les flux de données sensibles.

Vous souhaitez en savoir plus sur le produit  Polyspace Code Prover ?