Simulink Design Verifier

Détection des erreurs à l’aide des méthodes formelles

Contrairement au contrôle ou à l’analyse de la sémantique en simulation, les méthodes formelles utilisées dans Simulink Design Verifier détectent si des scénarios d’exécution dynamique sont possibles et les conditions de leur survenue. Ces informations peuvent ensuite servir à améliorer la conception et ses spécifications, ou guider la simulation pour le débogage et la validation. Simulink Design Verifier identifie les erreurs communes de conception suivantes : dépassement d’entier, division par zéro, logique morte et violations des assertions.

Détection du dépassement d’entier et de la division par zéro

Vous utilisez le mode de détection des erreurs dans Simulink Design Verifier afin de repérer le dépassement d’entier et la division par zéro. L’analyse est automatisée et ne nécessite aucune entrée utilisateur supplémentaire. Des plages autorisées pour l’ensemble des signaux de tous les blocs sont fournies pour vous aider à identifier la cause racine du problème. Au terme de l’analyse, vous pouvez examiner les résultats directement dans le modèle ou sous forme de rapport HTML.

Dans le modèle, les blocs sont marqués en vert, en jaune ou en rouge. Le vert indique que les blocs ne peuvent causer de dépassement d’entier ni de division par zéro. Le jaune indique que l’analyse ne peut produire de résultat concluant ou que la limite de temps pour l’analyse est expirée. Lorsqu’une erreur est détectée dans le chemin d’exécution du modèle, tous les blocs consécutifs de ce chemin ayant un dépassement d’entier et une division par zéro sont marqués en jaune.

Le rouge indique des erreurs de conception. Pour ces blocs, Simulink Design Verifier génère un cas de test capable de reproduire le problème lors d’une simulation ou d’un test. Vous pouvez invoquer le cas de test et exécuter une simulation directement dans Simulink.

Détection d’une logique morte

Vous utilisez le mode de génération de test dans Simulink Design Verifier afin de détecter une logique morte, à savoir des objets du modèle obsolètes ou manifestement inactifs lors de l’exécution. La logique morte est souvent provoquée par une erreur de conception ou de spécification. Pendant la génération du code, une logique morte entraîne un code mort. La logique morte est difficile à détecter par le test en simulation seule, car, même après l’exécution d’une quantité importante de simulations, il peut être dur de prouver qu’un comportement donné ne peut être activé.

À l’issue de votre analyse de génération de test, le modèle est coloré en fonction des critères de génération de test. Les objets de modèle contenant une logique ne pouvant être activée en environnement de simulation sont marqués en rouge. Ceux qui contiennent une logique totalement activable en simulation sont marqués en vert. Simulink Design Verifier génère un cas de test capable de reproduire la logique morte durant la simulation.

Dead logic in a Stateflow chart detected by Simulink Design Verifier.
Transition dans un diagramme Stateflow mise en surbrillance en rouge par Simulink Design Verifier. La logique morte survient dans cette transition, car la condition « press < zero_thresh » ne peut jamais être fausse.

Détection des violations d’assertion

Vous utilisez l’option de détection de violation du mode preuves de propriétés dans Simulink Design Verifier afin d’identifier des violations d’assertion. Simulink Design Verifier contrôle si un scénario valide peut déclencher des assertions pendant la simulation au sein du nombre de pas indiqué dans les paramètres d’analyse. Ainsi, vous pouvez construire une assertion qui se déclenche chaque fois qu’un actionneur d’inverseur de poussée est engagé et qu’un indicateur d’état de vol présente la valeur « true ». Les assertions pouvant être violées avec des scénarios valides sont mises en surbrillance en rouge et un vecteur de test déclenchant l’assertion est généré. En plus des assertions disponibles dans Simulink, Simulink Design Verifier fournit des blocs supplémentaires pour définir les contraintes de l’analyse, ce qui permet d’analyser en totalité le comportement de conception et de détecter ses défauts avant d’exécuter une simulation.

Point suivant: Vérification de la conformité des conceptions aux spécifications

Essayer Simulink Design Verifier

Obtenir une version d'évaluation

Développez des tests pour des modèles Simulink et du code embarqué

Visionner le webinar