Prouver l’absence d’erreurs d’exécution dans le logiciel

Polyspace Code Prover™ est un solide outil d’analyse statique qui prouve l’absence d’overflow, de division par zéro, de débordement de tableaux et autres erreurs d’exécution dans le code source C et C++. Il produit des résultats sans exiger l’exécution du programme, l’instrumentation du code ou des cas de test. 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, le contrôle et les flux de données du logiciel. Polyspace Code Prover utilise l’analyse statique et l’interprétation abstraite basée sur des méthodes formelles. Vous pouvez l’utiliser sur un code écrit manuellement, un code généré ou une combinaison des deux. Chaque opération est mise en évidence via un code couleur indiquant si elle est exempte d’erreurs d’exécution, en défaut, inaccessible (code mort) ou indéterminée.

Polyspace Code Prover affiche également des informations sur les plages de valeur des variables et des valeurs de retour de fonction, et peut prouver les conditions selon lesquelles les variables excèdent les limites de plages spécifiées. Les résultats peuvent être publiés sur un tableau de bord afin de suivre les métriques de qualité et assurer la conformité aux objectifs de qualité logicielle. Polyspace Code Prover peut être intégré à des systèmes de déploiement pour une vérification automatisée.

La prise en charge des normes de l’industrie est assurée via IEC Certification Kit (pour IEC 61508 et ISO 26262) et DO Qualification Kit (pour DO-178). La prise en charge du langage Ada est aussi assurée.


Fonctionnalités

Vérification du logiciel embarqué C et C++

Vérifiez le code du logiciel embarqué C et C++ devant fonctionner aux niveaux de qualité et de sécurité les plus élevés.

En savoir plus

Détection des erreurs d’exécution

Prouvez, identifiez et diagnostiquez des erreurs d’exécution telles que les dépassements, les divisions par zéro et les débordements pointeur.

En savoir plus

Affichage des plages de valeur

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

En savoir plus

Suivi des métriques de qualité logicielle

Définissez un modèle qualité centralisé pour suivre les erreurs d'exécution, la complexité du code et les violations des règles de codage.

En savoir plus

Traçabilitédes résultats de vérification du code aux modèles Simulink

Vérifiez le code généré ou mixte, qui contient à la fois du code généré et du code écrit manuellement.

En savoir plus

Automatisation du processus de vérification du code

Automatisez la planification de la tâche de vérification et mettez en place des notifications par e-mail.

En savoir plus

Création d’artefacts de certification

Effectuez le processus de certification de projets basés sur les normes de l'industrie.

En savoir plus

Ressources produits

Découvrez-en davantage sur Polyspace Code Prover en consultant ces ressources.

Documentation

Consultez notre documentation pour connaître les fonctions et les caractéristiques de Polyspace Code Prover, notamment les notes de version et des exemples.

Exigences du système

Affichez les spécifications système requises pour la dernière version de Polyspace Code Prover.

Articles techniques

Consultez les notes expliquant les avantages techniques de l'utilisation d'Polyspace Code Prover.

Témoignages d'utilisateurs

Découvrez comment Polyspace Code Prover accélère la recherche et le développement de votre industrie.

Communauté et soutien

Trouvez les réponses à vos questions et consultez nos ressources dédiées à la résolution des problèmes.

Apps

Les applis Polyspace Code Prover vous permettent d'accéder rapidement aux tâches courantes via une interface interactive.


Essayer ou Acheter

Vous pouvez commencer à utiliser les Polyspace Code Prover de nombreuses façons. Téléchargez gratuitement la version d'essai, or consultez les tarifs et les options de licence.

Obtenez gratuitement la version d'essai

Essayez Polyspace Code Prover.

Essayer une version d'évaluation

Prêt à acheter?

Achetez Polyspace Code Prover et découvrez les produits complémentaires.

Contact commercial
Tarifs et licences

Vous avez des questions ?

Ram

Contacter Ram Cherukuri,
expert technique Polyspace Code Prover

Envoyer un e-mail à Ram

Polyspace Code Prover requires Polyspace Bug Finder.


 Solutions associées

Utilisez Polyspace Code Prover pour relever des défis scientifiques et d'ingénierie :


Au fil des événements

Fast-Track MISRA Compliance of Generated Code