
Développement : PragmaDev enrichit son environnement de conception avec un vérificateur de modèles OBP pour plus de sûreté Avec la version 6.0 de son environnement de développement orienté modèles PragmaDev Studio, le français PragmaDev introduit une nouvelle génération de vérificateur de modèles et la prise en charge du "broadcast", dernière nouveauté du langage standardisé SDL (Specification and Description Language) sur lequel s’appuie PragmaDev Studio. Un apport qui fait suite à une collaboration sur plusieurs années avec le laboratoire de recherche de l'ENSTA Bretagne (École nationale supérieure de techniques avancées) autour du vérificateur de modèles OBP (Observer Based Prover). PragmaDev rappelle à ce niveau que l’objectif principal d’un vérificateur de modèles est d’explorer tous les scénarios possibles et, lors de cette exploration, de détecter les éventuelles "deadlocks" (situations d’interblocage entre processus) et les chemins inatteignables ou de vérifier des propriétés. Selon PragmaDev, il s’agit ici d’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 spécifique mais sur un exécuteur de modèles externe. Au sein de l’environnement PragmaDev Studio, OBP interagit avec l'exécuteur de modèles SDL pour explorer l'espace d'états, avec comme originalité qu'OBP ne sait rien du modèle qu'il explore. C'est le même principe pour l'évaluation des propriétés ; OBP propose les propriétés complexes composées de propriétés atomiques fournies par l'exécuteur de modèles. Parallèlement, du fait de la nature des systèmes communicants fondés sur des machines d'état concurrentes, avec la génération de nombreux chemins d'exécution possibles, PragmaDev Studio intégre désormais des moyens de réduction de l'espace d'état. Et ce en utilisant les valeurs possibles des paramètres des messages entrants, ainsi que le nombre de messages et en excluant certaines variables internes de l'état système. Enfin, PragmaDev Studio prend dorénavant en charge la fonctionnalité de "broadcast" introduite dans la dernière version du standard SDL. Jusqu'à maintenant, explique PragmaDev, 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é dite Broadcast qui, en utilisant l'expression "to all", indique de manière directe et naturelle que chaque agent pouvant recevoir le message le recevra. Une approche qui va simplifier la conception de modèles de systèmes communicants où cette situation est communément rencontrée. « Le support du broadcast et l'intégration du nouveau vérificateur de modèles renforce la capacité de l’outil PragmaDev Studo à spécifier et concevoir des systèmes communicants sûrs », précise Emmanuel Gaudin, directeur fondateur de PragmaDev.

Développement : PragmaDev enrichit son environnement de conception avec un vérificateur de modèles OBP pour plus de sûreté

Avec la version 6.0 de son environnement de développement orienté modèles PragmaDev Studio, le français PragmaDev introduit une nouvelle génération de vérificateur de modèles et la prise en charge du "broadcast", dernière nouveauté du langage standardisé SDL (Specification and Description Language) sur lequel s’appuie PragmaDev Studio.

Un apport qui fait suite à une collaboration sur plusieurs années avec le laboratoire de recherche de l'ENSTA Bretagne (École nationale supérieure de techniques avancées) autour du vérificateur de modèles OBP (Observer Based Prover). PragmaDev rappelle à ce niveau que l’objectif principal d’un vérificateur de modèles est d’explorer tous les scénarios possibles et, lors de cette exploration, de détecter les éventuelles "deadlocks" (situations d’interblocage entre processus) et les chemins inatteignables ou de vérifier des propriétés.

Selon PragmaDev, il s’agit ici d’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 spécifique mais sur un exécuteur de modèles externe. Au sein de l’environnement PragmaDev Studio, OBP interagit avec l'exécuteur de modèles SDL pour explorer l'espace d'états, avec comme originalité qu'OBP ne sait rien du modèle qu'il explore. C'est le même principe pour l'évaluation des propriétés ; OBP propose les propriétés complexes composées de propriétés atomiques fournies par l'exécuteur de modèles.

Parallèlement, du fait de la nature des systèmes communicants fondés sur des machines d'état concurrentes, avec la génération de nombreux chemins d'exécution possibles, PragmaDev Studio intégre désormais des moyens de réduction de l'espace d'état. Et ce en utilisant les valeurs possibles des paramètres des messages entrants, ainsi que le nombre de messages et en excluant certaines variables internes de l'état système.

Enfin, PragmaDev Studio prend dorénavant en charge la fonctionnalité de "broadcast" introduite dans la dernière version du standard SDL. Jusqu'à maintenant, explique PragmaDev, 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é dite Broadcast qui, en utilisant l'expression "to all", indique de manière directe et naturelle que chaque agent pouvant recevoir le message le recevra. Une approche qui va simplifier la conception de modèles de systèmes communicants où cette situation est communément rencontrée.

« Le support du broadcast et l'intégration du nouveau vérificateur de modèles renforce la capacité de l’outil PragmaDev Studo à spécifier et concevoir des systèmes communicants sûrs », précise Emmanuel Gaudin, directeur fondateur de PragmaDev.