Facebook Twitter Newsletter Linkedin RSS

Portail de la presse

 

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

headerpragmadev

Paris - France - Le 14 juin 2022PragmaDev 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.

V600 fr

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.

A propos de PragmaDev

PragmaDev est une société indépendante basée à Paris en France qui fournit deux suites d’outils: PragmaDev Process pour la description et la vérification des processus métiers, et PragmaDev Studio pour la spécification et la conception des systèmes communicants.
PragmaDev compte parmi ses clients Airbus, Nokia, Renault, Wipro, la DGA, ST-Microelectronics, Korean Telecom, l’Agence Spatiale Européenne, Toshiba, et LG Electronics.

Contacts Presse
Emmanuel Gaudin
PragmaDev
tel: +33 1 42 74 15 38
http://www.pragmadev.com

 

Consulter le communiqué au format PDF