Simulink Design Verifier

Principales fonctionnalités

  • Moteurs d’analyse formelle Polyspace® et Prover Plug-In®
  • Détection de logique morte, dépassement entier et virgule fixe, division par zéro et violation de propriétés de conception
  • Blocs et fonctions pour la modélisation des spécifications fonctionnelles et sécuritaires
  • Génération de vecteur de test à partir de spécifications fonctionnelles et d’objectifs de couverture du modèle, y compris la couverture de condition, de décision et de condition/décision modifiée (MC/DC)
  • Preuves de propriétés, avec génération d’exemples de violation pour l’analyse et le débogage
  • Prise en charge des modèles en virgule fixe et flottante

Simulink Design Verifier vous permet d’effectuer une analyse du modèle dans l’environnement Simulink®. Il permet de vérifier vos conceptions et de valider les spécifications en amont sans devoir générer de code. Ainsi, vous pouvez vérifier et valider tout au long du processus de conception. L’analyse de modèle avec Simulink Design Verifier complète la simulation en vous permettant d’utiliser les résultats de simulation comme entrées pour l’analyse avec les méthodes formelles.

Simulink Design Verifier prend en charge le sous-ensemble à temps discret de Simulink et Stateflow® généralement utilisé dans des conceptions au contrôle embarqué.

Design error detection in a model using Simulink Design Verifier.
Détection des erreurs de conception dans un modèle à l’aide de Simulink Design Verifier. Le bloc mis en surbrillance en rouge possède une erreur de conception. Le sous-système en vert est manifestement exempt d’erreurs.

Méthodes formelles dans Model-Based Design

Simulink Design Verifier utilise les techniques d’analyse formelle fournies par Prover Plug-In de Prover Technology et le moteur d’analyse formelle Polyspace de MathWorks. Ces techniques s’appuient sur de rigoureuses procédures mathématiques afin de rechercher dans les divers chemins d’exécution possibles de votre modèle, des cas de test et des contre-exemples. Contrairement aux méthodes de test traditionnelles, dans lesquelles les scénarios de test et les résultats escomptés sont exprimés par des valeurs de données concrètes, les techniques d’analyse formelle vous permettent d’utiliser des modèles du comportement système au lieu de ces valeurs. Un modèle de comportement système peut inclure des modèles de scénarios de test et des objectifs de vérification décrivant les comportements désirés et indésirables du système. L’exécution d’une analyse formelle avec de tels modèles complète la simulation et offre une meilleure compréhension de votre conception.

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.

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.

Analyse de la couverture du modèle

Simulink Design Verifier analyse les algorithmes et la logique dans vos modèles Simulink et Stateflow pour générer des cas de test et des paramètres requis par les normes de l’industrie pour le développement de systèmes haute intégrité. La génération de test pour les critères de la couverture structurelle inclut la couverture de condition, de décision et de condition/décision modifiée (MC/DC).

Génération de test

La génération de test pour la couverture de modèle augmente les tests basés sur les spécifications créés manuellement ou collectés lors de la simulation du système terminé. Selon cette approche, Simulink Design Verifier extrait les informations de couverture du modèle et génère des vecteurs de test supplémentaires, conformes à tous les objectifs de couverture non satisfaits pendant les tests basés sur les spécifications.

Visual display of a generated test vector that activates previously untested functionality.

Affichage visuel d’un vecteur de test généré activant une fonctionnalité précédemment non testée.

Vous pouvez utiliser ces vecteurs de test afin de mieux comprendre les spécifications manquantes et de créer un logiciel de test plus complet. Pour simplifier les tests de modèles possédant un grand nombre d’importations et d’exportations, Simulink Design Verifier contrôle les signaux inutilisés et les supprime automatiquement du logiciel de test.

Tous les vecteurs de test générés sont capturés en tant que structure MATLAB pouvant être utilisée directement comme entrée pour l’exécution du test en simulation, SIL ou PIL. Les données de test collectées peuvent également servir à générer un modèle de logiciel de test.

Validation des vecteurs de test générés

Pour valider les vecteurs de test générés conformes aux critères de couverture structurelle, vous pouvez utiliser le Model Coverage Tool fourni dans Simulink Verification and Validation. Il surveille la simulation et évalue si les objectifs signalés pendant l’analyse formelle ont été atteints. Outre les objectifs de couverture pour la couverture de condition, de décision et de condition/décision modifiée (MC/DC), Model Coverage Tool signale aussi la couverture des objectifs de test, objectifs de preuve, hypothèses, contraintes, tables de recherche et plages de signaux enregistrés pendant la simulation.

Simulink Design Verifier est certifié TÜV SÜD pour une utilisation dans le cadre de processus de développement devant se conformer aux normes ISO 26262, IEC 61508 ou EN 50128.

Analyse de la couverture de test sur le code généré

Simulink Design Verifier offre des fonctions d’automatisation de test applicables à l’exécution de cas de test générés par rapport au code dans SIL et PIL. Les fonctions de vérification de code dans Simulink Design Verifier requièrent Embedded Coder™. Pendant l’exécution du test, vous pouvez intégrer les outils de couverture de code disponibles dans Embedded Coder afin de collecter la couverture de code.

Essayer Simulink Design Verifier

Obtenir une version d'évaluation

Vérifier et valider exhaustivement vos systèmes embarqués dans Simulink avant leur implémentation !

Visionner le webinar