En poursuivant votre navigation sur ce site, vous acceptez l'utilisation de cookies pour vous proposer des contenus et services adaptés à vos centres d'intérêts. En savoir plus et gérer ces paramètres. OK X
 
 

 

 

Nouveaux produits

Une nouvelle génération de vérificateur de modèle avec PragmaDev Studio V6.0

Publication: 16 juin

Partagez sur
 
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).

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.

http://www.pragmadev.com/

Suivez Electronique Mag sur le Web

 

Newsletter

Inscrivez-vous a la newsletter d'Electronique Mag pour recevoir, régulièrement, des nouvelles du site par courrier électronique.

Email: