|
SDL Model Checking
Suite à une longue collaboration avec le laboratoire de recherche de l'ENSTA Bretagne, PragmaDev a intégré dans sa dernière version de PragmaDev Studio, OBP (Observer Based Prover) le model checker de l'ENSTA Bretagne.Simulation exhaustive
L'objectif principal de la vérification de modèle est d'explorer tous les scénarios possibles du modèle. Au cours de l'exploration il est possible de détecter les étreintes fatales (deadlock), les branches de modèle inatteignables, ou de vérifier des propriétés.Un explorateur agnostique
La caractéristique principale de OBP est qu'il ne s'appuie pas sur un langage dédié. Il s'appuie sur un exécuteur de modèle externe. Dans notre cas OBP intéragit avec l'exécuteur SDL de PragmaDev pour exécuter les transitions. OBP ne connait rien du modèle qu'il est en train d'explorer. C'est le même principe avec les propriétés. OBP évalue les propriétés complexes composées de propriété atomiques qui sont évaluées par l'exécuteur de modèle.
Gérer l'espace d'état
Par construction les systèmes communicants créés de nombreux cas possibles. Ceci est dû au fait que leur conception est basée sur des machines d'état concurrentes. Ceci créé de nombreux chemins possibles d'exécution. De ce fait nous avons implémenté des moyens de réduire l'espace d'état:- En réduisant les valeurs possibles des paramètres de message ainsi que le nombre de messages.
- En excluant des variables internes de l'état globale du système.
Broadcast
PragmaDev Studio support la fonctionnalité de Broadcast introduite dans la dernière version du standard SDL et de la recommendation SDL-RT. Jusqu'à maintenant, chaque message SDL (ou signal) était reçu par un unique agent. Si une réponse coordonnée était attendue, le message devait être explicitement dupliqué et envoyé à chacun des destinataires. La dernière version de SDL introduit une fonctionnalité de Broadcast. En utilisant l'expression 'to all', l'ingénieur indique de manière directe et naturelle que chaque agent pouvant recevoir le message le recevra, ceci facilitant la coordination. C'est une situation très commune dans les systèmes communicants, ceci simplifiera notablement les modèles.Avant cette fonctionnalité, l'envoyeur devait se rappeler des ids de tous les receveurs et faire une boucle d'envoi:
Version Windows 64 bits native
La version 6.0 de PragmaDev Studio est nativement 64 bits sur Windows. Ceci facilitera la gestion des grands modèles lors de la simulation ou de l'exploration.