Polyspace Code Prover

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

Polyspace Code Prover™ prouve l’absence d’erreurs d’exécution comme le dépassement, la division par zéro ou le débordement de tableaux. 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 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.

Automatiser et optimiser la vérification et le test de logiciel embarqué

Visionner le webinar

Essayer Polyspace Code Prover

Obtenir une version d'évaluation