Accelerating the pace of engineering and science

Simulink Design Verifier

Principales fonctionnalités

  • Génération de cas de test à partir de spécifications fonctionnelles et d’objectifs de couverture de modèle, y compris les conditions, les décisions et les conditions/décisions modifiées (MCDC).
  • Détection de la logique morte, des dépassements d'entiers et de virgules fixes, des violations de l'accès aux tableaux, de la division par zéro et des violations des spécifications
  • Blocs de vérification pour la modélisation des spécifications fonctionnelles et de sécurité
  • Preuves de propriétés, avec génération d’exemples de violation pour l’analyse et le débogage.
  • Model Slicer pour l'analyse des dépendances fonctionnelles et des comportements problématiques dans les grands modèles
  • Moteurs de vérification formelle Polyspace® et Prover® pour les modèles en virgule fixe et en virgule flottante

Vue d'ensemble de la solution Simulink Design Verifier
Identify design errors, generate test cases, and verify designs against requirements using Simulink Design Verifier™.

valider rapidement les spécifications sans avoir à générer de codeSimulink Design Verifier™ vous permet de vérifier vos modèles et de valider rapidement les spécifications sans avoir à générer de code. Il vous aide à améliorer la robustesse de vos modèles au sein de l'environnement Simulink®. Vous pouvez analyser la logique de contrôle, les S-fonctions et le code MATLAB® via des méthodes formelles mathématiquement rigoureuses. À la différence des méthodes de test traditionnelles dans lesquelles les scénarios de test et les résultats attendus sont exprimés en valeurs concrètes, les techniques de vérification formelle vous permettent de travailler avec des modèles de comportement système. La vérification formelle peut prouver certains attributs du logiciel, par exemple le fait qu'il contienne ou non des erreurs d'exécution, et ce grâce à une meilleure compréhension des spécifications du système.

Détection des erreurs de conception

Simulink Design Verifier peut détecter si des scénarios d'exécution dynamique spécifiques peuvent se produire, et sous quelles conditions. Vous pouvez détecter les erreurs de conception suivantes : dépassement d'entier, division par zéro, logique morte et tableaux hors limites. Détecter ces erreurs dès le début du cycle de conception, avant les tests basés sur la simulation, permet d'éviter les réparations coûteuses par la suite.

Design error detection in a model using Simulink Design Verifier.
Détection des erreurs de conception. Le bloc apparaissant en rouge présente une erreur de conception ; le sous-système apparaissant en vert est correct.

La détection des erreurs de conception est entièrement automatisée, et vous pouvez consulter les résultats directement dans le modèle ou dans un rapport au format HTML. Les plages autorisées pour tous les signaux sur tous les blocs sont fournies pour vous aider à détecter la cause principale du problème. Dans le modèle, les blocs sont marqués en vert, orange ou rouge : le vert indique qu'aucune erreur n'a été détectée, l'orange indique que l'analyse n'a pas été concluante dans le temps imparti et le rouge signale les blocs qui présentent des erreurs de conception. Simulink Design Verifier génère automatiquement des cas de test afin de recréer le scénario d'erreur pour chaque bloc rouge. Vous pouvez utiliser ces cas de test dans Simulink pour comprendre et déboguer les conditions sous lesquelles l'erreur se produit.

Détection de logique morte

Dead logic in a Stateflow chart detected by Simulink Design Verifier.
Détection d'une logique morte, avec transition dans un diagramme Stateflow mise en surbrillance en rouge par Simulink Design Verifier Une logique morte se produit lors de cette transition car la condition « press < zero_thresh » ne peut jamais être fausse.

Le mode de détection de logique morte trouve les parties du modèle qui sont obsolètes ou inactives lors de l'exécution. Souvent, la logique morte est due à une erreur de conception ou de spécification. Lors de la génération du code, une logique morte engendre du code mort. Les objets de modèle qui contiennent une logique impossible à activer lors d'une simulation sont marqués en rouge ; ceux qui contiennent une logique qui peut être entièrement activée lors d'une simulation sont marqués en vert. Une 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é.

Génération de cas de test

Vérifier le comportement entrée - sortie du modèle d'implémentation uniquement ne garantit pas une conception correcte. Les tests fonctionnels constituent une première étape importante pour la vérification des modèles, mais ces tests sont essentiellement dérivés des spécifications, qui peuvent être incomplètes. Pour améliorer la robustesse de votre conception, vous pouvez utiliser des techniques de vérification structurelle telles que la couverture de modèle pour vous aider à identifier les chemins de simulation non utilisés dans le modèle. Fondamentalement, la couverture de modèle indique comment un cas de test parcourt un modèle et vous indique le pourcentage de chemins parcourus par un cas de test. L'examen des chemins non testés vous permet de détecter les erreurs de conception potentielles.

Étendez les cas de test existants pour obtenir une couverture complète du modèle
Tirez parti des cas de test existants et obtenez une couverture complète à l'aide de méthodes formelles pour la génération de test dans Simulink Design Verifier™.

Simulink Design Verifier combine des méthodes formelles et des techniques heuristiques de façon à générer des cas de test pour la couverture de modèle et les critères personnalisés de l'utilisateur. La génération de cas de test pour la couverture de modèle augmente et étend les jeux de test basés sur les exigences créés manuellement ou enregistrés lors de la simulation de l'intégralité du système. Outre les objectifs de couverture pour les conditions, les décisions et la couverture MCDC, vous pouvez également définir des objectifs de test personnalisés afin de générer des cas de test basés sur les exigences.

Tests basés sur les exigences
Générez des cas de test à partir des modèles de spécifications système à l'aide de Simulink Design Verifier™.

Vous pouvez utiliser le Test Generation Advisor pour sélectionner les composants d'un modèle (sous-systèmes atomiques et blocs du modèle) pour la génération de test. Le Generation Advisor réalise une analyse approfondie pour vous aider à mieux comprendre votre modèle avant la génération d'un test, particulièrement lorsqu'il s'agit de modèles volumineux, complexes ou de modèles pour lesquels vous n'êtes pas certain de la compatibilité de la génération du test. Tous les cas de test générés sont capturés en tant que structure MATLAB pouvant être utilisée directement comme une entrée pour l'exécution de test de simulation, de test SIL ou de test PIL. Les données de test collectées peuvent également être utilisées dans Simulink Test™ et dans les harnais de test associés. Lors de l'exécution des tests, vous pouvez intégrer les outils de couverture de code tiers disponibles dans Embedded Coder® pour collecter la couverture de code.

Simulink Design Verifier est certifié par TÜV SÜD pour une utilisation dans le cadre de processus de développement qui doivent être conformes aux normes ISO 26262, IEC 61508 et EN 50128.

Visual display of a generated test vector that activates previously untested functionality.
Test Generation Advisor : Résumé de la compatibilité pour la génération de test, des objectifs de couverture et de la logique morte pour le modèle et les composants du modèle dans un affichage hiérarchique.

Isolement des comportements problématiques à l'aide de Model Slicer

Simulink Design Verifier isole les comportements problématiques au sein d'un modèle en utilisant une association d'analyses dynamiques et statiques pour assurer la traçabilité des dépendances. L'analyse des dépendances comprend la détermination des dépendances au niveau des blocs, des signaux et des composants de modèle. Ce processus est long pour les modèles volumineux, étant donné la complexité des niveaux de hiérarchie et de la conception. Model Slicer vous aide à comprendre quelles parties de votre modèle influencent un comportement particulier. Les analyses statiques vous permettent d'identifier les dépendances de modèles pour tous les chemins de simulation possibles, tandis qu'en utilisant des analyses basées sur la simulation, seuls les chemins actifs lors de la simulation sont mis en évidence.

Cette analyse des dépendances se propage en amont, en aval ou de façon bidirectionnelle à partir d'un point de départ. Vous pouvez mettre en évidence les dépendances fonctionnelles des ports, signaux et blocs et assurer leur traçabilité, mais également diviser un modèle de grande taille en modèles autonomes de plus petite taille afin de réaliser des analyses. Vous pouvez également visualiser les blocs qui affectent la sortie d'un sous-système et assurer la traçabilité d'un chemin de signaux grâce à de nombreux commutateurs et blocs de conditions logiques.

Testing and debugging complex models
Testez et déboguez des modèles complexes. Identifiez la zone d'intérêt dans votre modèle et réduisez le modèle à la portion utile pour une analyse et un débogage approfondis.

Vérification basée sur les spécifications

Pour vérifier de façon formelle que le comportement d'un modèle est conforme à certaines exigences de sécurité ou fonctionnelles, celles-ci doivent d'abord être traduites d'un langage humain vers un langage compris par le moteur d'analyse formelle. Simulink Design Verifier vous permet d'exprimer des spécifications formelles à l'aide des fonctions MATLAB, Simulink et Stateflow®. Chaque spécification dans Simulink est associée à un ou plusieurs objectifs de vérification. Une fois que les spécifications et les objectifs de vérification sont capturés, ils peuvent être utilisés pour démontrer qu'un modèle utilisant des méthodes formelles est correct.

Par exemple, dans un système de suivi de vol, vous pouvez concevoir une assertion ou un objectif de preuve qui se déclenche lorsqu'un actionneur d'inverseur de poussée est engagé et qu'un indicateur de statut de vol maintient la valeur VRAI. Simulink Design Verifier examine toutes les conditions d'entrée possibles qui peuvent être à l'origine d'un comportement non désiré, puis il génère un rapport avec ses résultats. Pour un objectif de preuve donné, la conception peut être valide ou enfreindre les spécifications de sécurité. Lorsqu'il détecte une violation, Simulink Design Verifier génère un cas de test qui démontre l'infraction en simulation.

Simulink Design Verifier report for verifying a design against safety requirements represented with proof objectives.
Rapport généré par Simulink Design Verifier lors de la vérification d'un modèle par rapport aux exigences de sécurité, représentées par des objectifs de démonstration Le rapport indique la liste des objectifs pour lesquels la validité du modèle a été démontrée et la liste des objectifs pour lesquels l'analyse a rencontré des contre-exemples.

Lorsque vous utilisez Simulink Design Verifier avec l'interface de gestion des spécifications dans Simulink Verification and Validation™, vous pouvez relier les blocs et fonctions utilisés pour capturer les spécifications et les objectifs de vérification à des exigences de plus haut niveau décrites textuellement en dehors de Simulink.

Augmenter la confiance en votre logiciel embarqué avec Simulink...

Visionner le webinar