Home > Products > PragmaDev Process

PragmaDev Process is a simple and powerful tool that aims at helping business process modelers to verify 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.

A business process described with BPMN

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. The editor is completely free and the executor offers free execution of small models.

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


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.

Static check

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


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

PSC alternative

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.


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.

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.

BPMN execution engine

Execution scenarios are generated on the fly as an MSC (Message Sequence Chart) and can be manually or automatically replayed on the model.

BPMN execution traces


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.

Exhaustive exploration

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.