PragmaDEV Process uses OBP2

PragmaDev released the version 1.0 of PragmaDev PROCESS, a BPMN process modeling tool, which uses OBP2 for formal process verification.

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.

overview

Property Verification

PragmaDev Process uses OBP2 for property-driven process verification. The properties can be expressed either with the Property Sequence Charts (PSC) formalism or with the GPSL formalism.

OBP2 counter example in PROCESS

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.

Further informations

For more informations do not hesitate to contact PragmaDev