Accueil > Produits > PragmaDev Process


PragmaDev Process est un outil simple et puissant qui permet aux modélisateurs de processus de vérifier leurs modèles.

Les organisations complexes ou les opérations systèmes sont basés sur des processus décrits dans des modèles graphiques. La notation la plus populaire pour cela est le BPMN (Business Process Model Notation). Elle permet de décrire ce que font les différents participants à un process et comment ils intéragissent. Ces processus doivent être discutés et validés avant d'être appliqués en situation réelle. Toute mésentente du processus peut conduire à une situation catastrophique sur le terrain.

Un processus métier décrit avec BPMN

PragmaDev Process est un éditeur, un exécuteur, et un explorateur de modèles BPMN. C'est le résultat de 2 ans de travaux avec la Direction Générale de l'Armement, Eurocontrol, et Airbus DS. L'éditeur de modèle est gratuit et l'exécuteur permet gratuitement l'exécution de petits modèles.

L'éditeur est intégralement gratuit et l'exécuteur permet l'exécution gratuite de petits modèles. Télécharger ici.

Éditeur

L'éditeur permet de créer de nouveaux diagrammes, il permet aussi d'importer et d'exporter n'importe quel diagramme BPMN. Lors de l'importation l'outil vérifiera la conformité au xml du standard, puis fera une vérification statique de la sémantique des diagrammes.

Static check

L'analyse sémantique statique s'appuie sur les règles définies dans le standard telles que:
  • la cohérence des flux séquentiels.
  • la cohérence des flux de messages.
  • la cohérence des évènements et des portes logiques.
  • etc...

Propriétés

Une propriété est une règle qui est toujours vraie lors de l'exécution, par exemple une séquence d'évènements. Dans l'outil PragmaDev Process les propriétés sont exprimées avec un PSC (Property Sequence Chart).

PSC alternative

Une fois que le propriété est définie elle peut être vérifiée automatiquement avec l'outil OBP (Observer Based Prover) du laboratoire de recherche partenaire de l'ENSTA Bretagne. L'outil explorera automatiquement tous les scénarios possibles du modèle.

Exécution

PragmaDev Process permet d'exécuter les modèles en s'appuyant sur la sémantique définie dans le standard BPMN. L'outil propose à l'utilisateur les choix possibles à chaque pas d'exécution. Cette approche permet d'éviter toute erreur d'interprétation du modèle.

Lors de l'exécution une trace peut être générée qui peut être utilisée comme documentation de référence. Elle peut aussi être automatiquement rejouée sur le modèle pour vérifier que le scénario est toujours valide. Pour cela l'outil déclenche automatiquement les mêmes symboles que l'utilisateur a déclanché pas à pas. L'outil vérifie alors que les mêmes symboles sont exécutés sur la base de leur identifiant logique et de leur contenu.

BPMN execution engine

Les scénarios d'exécution sont générés à la volée au format MSC (Message Sequence Chart) et peuvent être manuellement ou automatiquement rejoués sur le modèle.

BPMN execution traces

Exploration

Résultat d'une collaboration avec le laboratoire de recherche de l'ENSTA Bretagne, l'outil peut explorer automatiquement tous les chemins possibles d'exécution.

Index de complexité

Le nombre de chemins possibles est un indicateur qui permet d'alerter sur de possibles problèmes dans le process. Par exemple si un modèle constitué d'une quinzaine de symboles permet des milliers de pas d'exécution, il est probable que ce n'est pas ce que voulait décrire le modeleur.

Exhaustive exploration

Vérification de propriété

Une propriété peut être automatiquement vérifiée à chaque pas d'exécution. En cas de violation l'outil générera automatiquement le scénario qui a mené à ce cas.