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.
If the verified property is not satisfied by the process model, OBP2 generates a counter example which is automatically loaded by PragmaDev Process and shown as a layer over the Process model and as a MSC trace.
For more informations do not hesitate to contact PragmaDev