Vérification formelle

La vérification formelle permet de confirmer que le code du système embarqué a le même  comportement que les modèles logiciels. Les méthodes de vérification formelle reposent sur des procédures mathématiquement rigoureuses et passent en revue les différentes possibilités d'exécution de votre modèle ou code afin d'identifier les erreurs dans votre conception. Vous pouvez effectuer cette vérification sur les modèles et le code généré à partir de ces modèles.

Vérification formelle de modèles

Vous pouvez employer des méthodes de vérification formelle afin d'identifier des erreurs dans votre modèle et générer des vecteurs de test qui reproduisent l'erreur en simulation. À la différence des méthodes de test traditionnelles dans lesquelles les résultats attendus sont exprimés en valeurs concrètes, les techniques de vérification formelle vous permettent de travailler sur des modèles de comportement système. Ces modèles peuvent inclure des scénarios de test et des objectifs de vérification qui décrivent les comportements système souhaités et non souhaités. Une analyse formelle effectuée sur ces modèles complète la simulation et permet une meilleure compréhension de votre conception.

Pour plus d'informations, reportez-vous à Simulink Design Verifier™.

Vérification formelle de code

Avec l'analyse statique du code et des méthodes de vérification formelle, vous pouvez utiliser des outils pour détecter et démontrer l’absence d’overflow, de division par zéro, de débordement de tableaux et d'autres erreurs d'exécution dans le code source écrit en C/C++ ou Ada. Vous pouvez les utiliser pour effectuer une vérification du code écrit manuellement ou généré des logiciels embarqués. Vous pouvez également vérifier la conformité avec les normes de codage, passer en revue les mesures de complexité du code et mesurer la qualité des logiciels.

Pour plus d'informations, reportez-vous aux produits Polyspace^®.