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.

Gestion de l'espace d'états

Les systèmes communicants créent intrinsèquement un grand nombre de cas possibles. Cela est dû au fait que leur conception repose sur des machines à états concurrentes. Cela engendre de nombreux chemins d'exécution possibles. Nous avons donc mis en œuvre plusieurs moyens pour réduire l'exploration :

• Ajuster finement la sémantique d'exécution
  Les options suivantes visent à réduire l'espace d'états ou à se rapprocher de certains environnements d'exécution spécifiques.
  
  • Message queues contrôle l'ordre dans lequel les messages peuvent être reçus par les instances de processus.
  • Initial transitions contrôle la priorité des transitions initiales par rapport aux autres transitions.
  • continuous signals contrôle la sémantique des signaux continus.
  • Internal transitions contrôle la priorité des transitions internes par rapport aux transitions déclenchées par des messages provenant de l'environnement.

• Réduire les valeurs possibles des paramètres des messages entrants ainsi que le nombre de messages.
  

  La version précédente de Studio ne pouvait gérer que les types simples. Cette version peut gérer tout type complexe ou structuré et définir les valeurs possibles de chacun de ses sous-champs. Dans cet exemple, seules deux valeurs seront explorées pour le champ prio du message CONNECT_ACK. Toutes les autres valeurs de champs sont fixées et ne seront pas explorées.

• Exclure certaines variables internes de l'état global du modèle.
  La valeur de chaque variable interne fait partie de l'évaluation de l'état global du système. Cependant, il arrive que différentes valeurs d'une variable n'aient aucun impact sur le comportement global du système, ce qui rend leur exploration inutile. Il est possible d'indiquer si une variable interne doit être prise en compte dans l'état du système.
  

  Cette nouvelle version effectue une analyse automatique du modèle et peut prédéfinir quelles variables internes doivent faire partie de l'état global du système ou non. Par exemple, une variable n'a pas besoin d'être incluse dans l'état du système si elle est toujours affectée avant d'être lue dans cette transition.