Accueil > Produits > PragmaDev Process > Vérification


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

Les organisations ou les systèmes complexes sont basés sur des processus qui peuvent être décrits dans des modèles graphiques. La notation standard la plus populaire pour cela est le BPMN (Business Process Model and Notation). Elle permet de décrire les activités des différents participants dans une organisation et comment ils interagissent. Ces processus sont discutés et validés avant d'être appliqués en situation réelle. Toute ambiguïté peut conduire à une situation catastrophique sur le terrain.


Présentation en 10mn

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. Résultat du partenariat avec MEGA International une intégration spécifique est disponible pour les utilisateurs d'Hopex.

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...

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

Chemins inatteignables

Grâce au moteur d'exécution exhaustif l'outil peut automatiquement identifier les chemins inatteignables dans le modèle. Après analyse les éléments impossibles à atteindre sont affichés en rouge dans l'éditeur.

BPMN unreachable paths

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.

Analyse de deadlock

Un deadlock est une situation dans laquelle il n'y a plus d'action à exécuter alors que le processus n'est pas terminé. La propriété prédéfinie de deadlock permet de les identifier automatiquement dans votre modèle

Exécution

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.

BPMN execution engine

Traces

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 traces

Couverture

L'information de couverture peut être extraite et fusionnée après chaque scénario d'exécution.

BPMN execution coverage

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.

Découvrez aussi nos fonctionnalités d'optimisation.