Simulink Design Verifier

Vérification de la conformité des conceptions aux spécifications

Les spécifications fonctionnelles des systèmes discrets sont généralement des instructions explicites concernant les comportements prévus d’un système et ceux qu’il ne doit jamais avoir. Les comportements interdits sont qualifiés de spécifications de sécurité.

Expression des spécifications fonctionnelles dans Simulink

Pour vérifier formellement que la conception agit conformément à ces spécifications, les instructions de spécification doivent d’abord être transposées en langage compris par le moteur de l’analyse formelle. Simulink Design Verifier permet d’exprimer des spécifications formelles à l’aide des fonctions Simulink, MATLAB® et Stateflow. Chaque spécification dans Simulink possède un ou plusieurs objectifs de vérification associés. Ces objectifs servent à produire des rapports sur la conformité ou non de la conception aux spécifications fonctionnelles et de sécurité.

Simulink Design Verifier fournit un ensemble de composants de base et de fonctions vous permettant de définir et d’organiser les objectifs de vérification. La bibliothèque de composants inclut des blocs et des fonctions pour les objectifs de test, les objectifs de preuve, les assertions, les contraintes et un ensemble dédié d’opérateurs temporels pour la modélisation des objectifs de vérification avec des aspects temporels.

Vous pouvez regrouper chaque spécification et ses objectifs de vérification associés dans des bibliothèques que vous pouvez gérer et examiner indépendamment de la conception.

Simulink Design Verifier library of property examples.
Bibliothèque d’exemples de propriétés Simulink Design Verifier

Lorsque vous utilisez Simulink Design Verifier avec l’interface de gestion des spécifications dans Simulink Verification and Validation™, vous pouvez lier les blocs et les fonctions utilisés pour capturer les objectifs de spécification et de vérification au plus haut niveau de spécification textuelle en dehors de Simulink.

Conformité des conceptions aux spécifications

Une fois les objectifs de spécification et de vérification capturés dans le modèle de vérification, ils peuvent être utilisés pour prouver l’exactitude d’une conception à l’aide de méthodes formelles.

Pour guider la vérification des spécifications fonctionnelles et conduire votre système à un état souhaité, vous pouvez utiliser les blocs des objectifs de test et les fonctions MATLAB afin de définir des objectifs de test. Pendant la génération du test, Simulink Design Verifier recherche un cas de test valide conforme aux objectifs indiqués. S’il ne trouve aucun objectif satisfaisant, la conception ne peut exécuter la fonctionnalité requise pour un ensemble donné de contraintes d’analyse.

Pour vérifier la conformité de votre conception à des spécifications de sécurité, vous pouvez utiliser les blocs des objectifs de preuve et les fonctions MATLAB pour définir des objectifs de preuve. Pendant l’analyse, Simulink Design Verifier examine toutes les conditions d’entrée possible susceptibles de causer le comportement indésirable, puis produit un rapport sur ses résultats. Pour chaque objectif de preuve, la conception peut être manifestement valide ou être détectée comme violant les spécifications de sécurité. Lorsqu’une violation est identifiée, Simulink Design Verifier génère un vecteur de test capable de démontrer la violation en simulation.

Simulink Design Verifier report for verifying a design against safety requirements represented with proof objectives.
Rapport de Simulink Design Verifier pour la vérification de la conformité d’une conception à des spécifications de sécurité représentées avec des objectifs de preuve. Le report affiche la liste des objectifs pour lesquels la conception est manifestement valide et la liste des objectifs pour lesquels l’analyse a détecté des contre-exemples.

Validation des résultats d’analyse

Les spécifications exprimées avec Simulink, les fonctions MATLAB et Stateflow, peuvent être simulées parallèlement à la conception. Vous pouvez aussi les utiliser afin de vérifier le code généré par une cosimulation en mode SIL ou PIL. Model Coverage Tool accumule des informations sur l’activation des objectifs de vérification pendant la simulation et fournit des résultats de couverture par l’intermédiaire des mesures de couverture Simulink Design Verifier. Vous pouvez accélérer l’analyse de la cause racine et le débogage en utilisant les objectifs de preuve qui représentent les spécifications de sécurité, afin d’interrompre la simulation au moment de leur violation.

Point suivant: Analyse de la couverture du modèle

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