Le français PragmaDev, éditeur d’environnements de conception, de spécification et de modélisation d’applications communicantes, propose avec PragmaDev Process une solution qui vérifie les processus métier décrits avec la notation BPMN (Business Process Model Notation).... L’outil qui intègre un éditeur, un module d'exécution et un explorateur de modèle est le résultat d’un projet de recherche de deux ans financé par la DGA (Direction générale de l’armement) avec des cas d’études réels venant des sociétés Eurocontrol et Airbus DS.

Les organisations et les systèmes complexes reposent sur des processus que l’on peut décrire dans des modèles graphiques. La notation la plus populaire est le BPMN. Elle permet de décrire ce que doivent faire les différents participants et comment ils interagissent. Ces processus sont au préalable méticuleusement validés car toute ambiguïté peut générer des situations catastrophiques sur le terrain. L’idée initiale du projet était de proposer le même type de fonctionnalités avancées que l’on trouve dans les outils de modélisation de PragmaDev au sein d’une solution fondée sur la notation BPMN.

« Lorsque nous avons démarré le projet nous pensions que les modèles BPMN étaient assez simples et ne prêtaient pas beaucoup à interprétation, raconte Emmanuel Gaudin, directeur et fondateur de PragmaDev. Mais au fur et à mesure que le projet avançait il s’est avéré que la sémantique des modèles pouvait créer des flots d’exécution inattendus et du coup la plupart des modèles dont nous disposions étaient incorrects. Dans ce cadre, PragmaDev Process aidera les modélisateurs de processus métier à lever toute ambiguïté. »

Dans le détail, l’éditeur de PragmaDev Process autorise l’édition de nouveaux diagrammes ou l'importation de diagrammes BPMN existants. Au moment de l’importation, l’outil vérifie la conformité du fichier .xml par rapport au standard, puis il vérifie la sémantique statique. Cette vérification sémantique s’appuie sur les règles décrites dans le standard comme la cohérence des flots de séquence, des flots de message, des branchements et des événements, etc.

Au niveau de l’exécution, l’outil permet le déroulement du modèle pas à pas sur la base de la sémantique standard du BPMN. Il propose en particulier les choix d’exécution possibles à chaque pas d’exécution. De ce fait, il n’y a pas d’interprétation possible de l’utilisateur qui pourrait conduire à une mauvaise lecture du modèle. En sus, une trace d’exécution est générée en tant que référence de documentation. Elle peut être rejouée automatiquement sur le modèle afin de vérifier qu’une nouvelle version du modèle se comporte comme une ancienne. Pour cela l’outil active automatiquement les mêmes symboles que ceux que l’utilisateur a activés manuellement sur la base de leurs identifiants et de leurs contenus. Cette trace est générée à la volée au format MSC (Message Sequence Chart) et peut être rejouée pas à pas ou automatiquement sur le modèle.

Au-delà, suite à une collaboration avec le laboratoire de recherche de l’ENSTA Bretagne, l’outil peut explorer automatiquement tous les chemins d’exécution. Il génère ainsi un index de complexité qui est le nombre total de tous les pas d’exécution. Cet indicateur permet d’alerter l’utilisateur sur de possibles erreurs dans le modèle. Par exemple, un modèle avec une quinzaine de symboles qui génère plus d’un millier de pas d’exécution ne se comporte probablement pas comme le développeur s’y attendait. Les propriétés peuvent aussi être vérifiées automatiquement à chaque pas d’exécution lors de la phase d’exploration. Si une violation de propriété est détectée, l’outil génère alors automatiquement le scénario qui y mène.

Rappelons qu’une propriété est un invariant lors de l’exécution, par exemple une séquence d’événements. Une propriété peut être exprimée dans l’outil PragmaDev Process avec un PSC (Property Sequence Chart). Une fois que la propriété est définie, elle est vérifiée automatiquement par l’outil OBP (Observer Based Prover) de l’ENSTA Bretagne.