Nouvelle génération de vérificateur de modèle

PragmaDev Studio introduit une nouvelle génération de vérificateur de modèle et le support du broadcast, dernière nouveauté du standard SDL, ce qui en fait la meilleure suite d’outils dédiés à la spécification et la conception des logiciels communicants sûrs.

Suite à une longue collaboration avec le laboratoire de recherche de l’ENSTA Bretagne, PragmaDev a intégré dans sa dernière version de Studio le vérificateur de modèle OBP (Observer Based Prover).

Explorer tous les scénarios possibles

L’objectif principal d’un vérificateur de modèle est d’explorer tous les scénarios possibles, et lors de l’exploration de détecter les éventuelles étreintes fatales (deadlock), les chemins inatteignables, ou de vérifier des propriétés. C’est une fonctionnalité majeure qui permet de concevoir des systèmes plus sûrs.

La caractéristique clé de l’outil OBP est qu’il ne s’appuie sur aucun langage dédié mais sur un exécuteur de modèle externe. Au sein de PragmaDev Studio, OBP interagit avec l’exécuteur de modèle SDL pour explorer l’espace d’états. L’originalité est que OBP ne sait rien du modèle qu’il explore. C’est le même principe pour l’évaluation des propriétés. OBP évalue les propriétés complexes composées de propriétés atomiques qui sont évaluées par l’exécuteur de modèle.

De par leur nature, les systèmes communicants sont basés sur des machines d’état concurrentes. Ceci génère de nombreux chemins d’exécution possibles. PragmaDev Studio a intégré des moyens de réduire l’espace d’état :

• En réduisant les valeurs possibles des paramètres des messages entrants ainsi que le nombre de messages.
• En excluant certaines variables internes de l’état système.

Le support du broadcast et l’intégration de ce nouveau vérificateur de modèle font de PragmaDev Studio le meilleur outil pour la spécification et la conception des systèmes communicants sûrs." précise Emmanuel Gaudin, directeur fondateur de PragmaDev.

Parmi les nouveautés majeures on retiendra :

• Introduction d’un nouveau vérificateur de modèle.
• Support du broadcast SDL.
• Application Windows 64 bits native.

Source : PragmaDev