PragmaDev Process is a simple and powerful tool that aims at helping business process modelers to verify and optimize their models.

Complex organizations or systems operations are based on processes described in graphical models. The most popular notation is BPMN (Business Process Model and Notation). It describes what the different participants in a process do and how they interact with each other. These processes must be thoroughly discussed before they are applied in a real situation. Any misunderstanding of the process might lead to a catastrophic situation in operation.

Check our 10 mn presentation

PragmaDev Process is a BPMN editor, executor, and verifier. It is the outcome of a 2 years research project with the French Army, Eurocontrol, and Airbus DS. As a result of our partnership with MEGA International a special integration is available for Hopex users.

The editor is completely free and the executor offers free execution of small models. Download it here.

Editor

The editor can edit brand new diagrams, it can also import or export any BPMN diagram. When importing the tool will check the XML conformity to the standard, then it will check the static semantic of the diagrams.

The static semantic check implements all the rules defined in the standard such as:

• Sequence flow consistency.
• Message flow consistency.
• Gateway and events consistency.
• etc...

Exploration

As a result of a collaboration with ENSTA Bretagne research lab, the tool can explore the different paths of execution automatically.

Complexity index

The number of possible paths is a rough indicator that can alert on possible flaws in the process. For example if a model made of 15 symbols can generate more than a 1000 possible steps of execution, it is doubtful that is what the designer intended to describe.

Unreachable paths

Thanks to its exhaustive execution engine the tool can automatically identify unreachable paths in the model. After analyze the impossible paths are displayed in red in the editor.

Property verification

A property can be automatically verified at each step of execution. If a violation is encountered the tool will automatically generate the scenario leading to the issue.

Deadlock analysis

A deadlock is a situation where there are no further actions to be performed even though the process is not finished. The built-in deadlock property will automatically identify possible deadlocks in your model.

Execution

No compromise on the semantic

Based on BPMN standard semantic, the modeler can execute the process step by step. The tool will outline the possible choices at each step of execution. There is no possible human interpretation leading to misunderstanding.

Traces

The execution can generate a trace which can be used as a reference documentation. It can also be automatically re-executed on the model to verify it has the same behavior. For that purpose the tool will trigger the same symbols the user did manually step by step. The tool will verify the same symbols are executed when the scenario is replayed based on their logical ids and on their contents.

Coverage

Coverage information can be extracted and merged after each scenario.

Properties

A property is something that should always be true during execution, for example a sequence of events. Properties can be expressed in PragmaDev Process with the PSC (Property Sequence Chart).

Once the property is defined it can be verified automatically with OBP (Observer Based Prover) tool from our partner ENSTA Bretagne. The tool will automatically explore all possible scenarios.

Check our process optimization features.