formal tools for BPMN

NEW: fBPMN Web Application (since v0.3.8)

We provide the user with a Web application of fbpmn so that its installation and use is made easier.

To use it:

• install Docker on your computer
• clone fbpmn from the GitHub repository here
• go to fbpmn/web
• read README.md
• run docker-compose build and then docker-compose up
• open http://localhost:3000/

Note: sBPMN (see below) is not yet supported in the Web application.

Note: the old fBPMN Web application, available here is now deprecated. It may stop operating at any time.

NEW: sBPMN, BPMN extension for spatial information (since v0.3.6)

To use it:

• install fbpmn as explained below
• in addition to steps 1. -- 5. below, ensure sfbpmn-check from the scripts/ directory is found on your command PATH
• design your model (M.bpmn), user definitions (M.userdefs, optional), user specific properties (M.userprops, optional), and boundedness constraints (M.constraint, optional); see models with ids s0xx in the models/bpmn-origin/src for examples
• verify your model with sfbpmn-check M.bpmn cores (the script will check if the optional files are there or not, cores is the number of cores to uses)

In next releases

• more documentation on associating time information to time-related BPMN constructs (available since v0.3.4)
• more documentation on sBPMN extension fields (available since v0.3.6)
• alignment between the fbpmn-check and sfbpmn-check verification scripts
• support for sBPMN in the Web application
• pre-built Docker image

fbpmn supports the verification of business processes (workflows and collaborations) properties:

• option to complete
• proper completion
• no dead activity
• safety
• soundness
• message-relaxed soundness

for seven different communication semantics:

• Bag (shared message multiset, no ordering)
• Fifo all (shared message queue, ordering wrt. emission time)
• Causal, (shared message causality structure, ordering wrt. message emission causality)
• Realizable with Synchronous Communication (RSC) (shared 1-sized message buffer)
• Fifo pair (message queue for each couple of processes, ordering wrt. emission time)
• Fifo inbox (input message queue for each process, ordering wrt. emission time)
• Fifo outbox, (output message queue for each process, ordering wrt. emission time)

New properties and communication semantics can be easily taken into account (see Sect. 5, Extending the verification).

• Sara Houhou, Souheib Baarir, Pascal Poizat, Philippe Quéinnec, and Laïd Kahloul. A First-Order Logic Verification Framework for Communication-Parametric and Time-Aware BPMN Collaborations. Information Systems, 2022.

• Rim Saddem-Yagoubi, Pascal Poizat, and Sara Houhou. Business Processes Meet Spatial Concerns: the sBPMN Verification Framework. In: 24th International Symposium on Formal Methods (FM), 2021.

• Sara Houhou, Souheib Baarir, Pascal Poizat, and Philippe Quéinnec. A Direct Formal Semantics for BPMN Time-Related Constructs. In: 16th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE), 2021.

• Sara Houhou, Souheib Baarir, Pascal Poizat, and Philippe Quéinnec. A First-Order Logic Semantics for Communication-Parametric BPMN Collaborations. In: 17th International Conference on Business Process Management (BPM), Springer, 2019.

Since we now provide you with a new Web application, all this can also be performed using it. If you like it the "command line interface" way, here is the procedure:

1. use the modeler of your choice to model a process or a collaboration

2. verify your model for all combinations of property and communication semantics

   ❯ fbpmn-check $FBPMN_HOME/models/bpmn-origin/src/e033MBE.bpmn 2
   Working in /tmp/e033MBE.T07y4 with 2 worker(s)
   transformation done
   <<"Processes=", 2, "Nodes=", 22, "Gateway=", 4, "SF=", 20, "MF=", 6>>
   ---------- Network01Bag ----------
   [X] Prop01Type
        states=101 trans=169 depth=23
   [X] Prop02Safe
        states=101 trans=169 depth=23
   [ ] Prop03Sound
        states=101 trans=169 depth=
   [X] Prop04MsgSound
        states=101 trans=169 depth=23
   [... other communication semantics ...]
   done.

3. generate interactive counter example exploration pages for all fbpmn-check analysis log files

   ❯ (cd /tmp/e033MBE.T07y4; fbpmn-log-transform html)
   transformation done
   transformation done
   transformation done
   [...]

4. open one of the generated files with a browser and play with the counter example using ←/→/Shift←/Shift→ on your keyboard

   

   01	...	12	13	14	...	24

   note: for security issues, and since the interactive counter example exploration pages load local files (your BPMN models), you will have either to:

   • (preferred) serve the pages using a server such as http-server or SimpleHTTPServer.

     ❯ npm install -g http-server # run only once to install http-server
     ❯ (cd /tmp/e033MBE.T07y4; http-server .)

     ❯ (cd /tmp/e033MBE.T07y4; python2 -m SimpleHTTPServer 8080) # for Python 2
     ❯ (cd /tmp/e033MBE.T07y4; python3 -m http.server 8080) # for Python 3

   • (not recommended) de-activate local file restrictions, see here.

To verify your BPMN models, you will need:

• 1.1. A Java SE Development Kit, get it here.

• 1.2. The TLA+ tools, get tla2tools.jar here.

• 1.3. The task-based command-line shell and scripting language Powershell, get it here

⚠️ fbpmn is known to be working with:

• Java 12 and TLA+ tools version 1.6.0 (not 1.5.7)
• Java 8 and TLA+ tools version 1.5.7 or 1.6.0

If you build fbpmn from sources (not required in most situations since binaries are available, see Sect. 3a), you will also need:

• 2.1. The stack build system for Haskell, see here.

  Under Windows, due to a bug, please use:

  curl -sS -ostack.zip -L --insecure https://www.stackage.org/stack/windows-x86_64
  7z x stack.zip stack.exe

Required for all platforms to get the TLA+ theories that are used in the verification process.

You can get the source files in either way:

• 2a. as an archive from the fbpmn repository by clicking the "Clone or download" button.

• 2b. by cloning the repository using the git command.

  git clone https://github.com/pascalpoizat/fbpmn

Please then set the FBPMN_HOME environment variable to the place where the fbpmn sources have been installed.

export FBPMN_HOME=/Somewhere/On/Your/Disk/fbpmn

You may typically add such a command in your shell configuration file, e.g., ~/.bashrc or ~/.zshenv under Linux and MacOS.

Linux, MacOS, and Windows binaries of stable versions of fbpmn are built using the continuous integration server and are available here.

Please then put the fbpmn command in a directory that is in your PATH environment variable.

cd fbpmn
stack clean
stack build
stack install

This will install the fbpmn command in some place that depends on your OS. You can use stack path --local-bin to find out which directory it is.

Please then put this directory in your PATH environment variable.

fbpmn is able to deal with collaborations either in BPMN or in its own JSON format (see Sect. 7, below). Please note that you can also deal with a standalone process model (workflow) as long as you put it in a standalone pool lane (see some examples of this here).

Please see the BPMN 2.0 standard.

The subset of BPMN that we support is presented in Fig. 1.

Figure 1: supported subset of the BPMN notation.

fbpmn has been tested with models made with the Camunda Modeler, which you can get here.

Verification requires that:

• FBPMN_HOME is set to the place where the fbpmn sources have been installed (see Sect. 2).
• TLA2TOOLS_HOME is set to the place where tla2tools.jar is installed (see Sect. 1).
• fbpmn is found on the command PATH (see Sect. 3a/3b).
• fbpmn-check and fbpmn-log-transform (from the scripts directory of the source distribution) are found on the command PATH.

Verification is achieved in two steps (see Fig. 2):

1. generate a TLA+ representation of the BPMN collaboration
2. use this representation and the TLA+ implementation of our FOL semantics for BPMN collaborations to perform verification (using the TLC model checker from the TLA+ tool box).

Figure 2: fbpmn approach to the verification of BPMN collaborations.

In the sequel, we will use the model in Fig. 3.

Figure 3: example collaboration model (e033MBE.bpmn).

We provide you with a fbpmn-check script (in the scripts directory of the source distribution) that does the two steps described in Fig. 2 for you and performs verification for each possible communication model.

❯ fbpmn-check $FBPMN_HOME/models/bpmn-origin/src/e033MBE.bpmn 2
Working in /tmp/e033MBE.T07y4 with 2 worker(s)
transformation done
<<"Processes=", 2, "Nodes=", 22, "Gateway=", 4, "SF=", 20, "MF=", 6>>
---------- Network01Bag ----------
[X] Prop01Type
     states=101 trans=169 depth=23
[X] Prop02Safe
     states=101 trans=169 depth=23
[ ] Prop03Sound
     states=101 trans=169 depth=
[X] Prop04MsgSound
     states=101 trans=169 depth=23
---------- Network02FifoPair ----------
[X] Prop01Type
     states=101 trans=169 depth=23
[X] Prop02Safe
     states=101 trans=169 depth=23
[ ] Prop03Sound
     states=101 trans=169 depth=
[X] Prop04MsgSound
     states=101 trans=169 depth=23
---------- Network03Causal ----------
[X] Prop01Type
     states=105 trans=173 depth=23
[X] Prop02Safe
     states=105 trans=173 depth=23
[ ] Prop03Sound
     states=105 trans=173 depth=
[X] Prop04MsgSound
     states=105 trans=173 depth=23
---------- Network04Inbox ----------
[X] Prop01Type
     states=101 trans=169 depth=23
[X] Prop02Safe
     states=101 trans=169 depth=23
[ ] Prop03Sound
     states=101 trans=169 depth=
[X] Prop04MsgSound
     states=101 trans=169 depth=23
---------- Network05Outbox ----------
[X] Prop01Type
     states=101 trans=169 depth=23
[X] Prop02Safe
     states=101 trans=169 depth=23
[ ] Prop03Sound
     states=101 trans=169 depth=
[X] Prop04MsgSound
     states=101 trans=169 depth=23
---------- Network06Fifo ----------
[X] Prop01Type
     states=120 trans=194 depth=23
[X] Prop02Safe
     states=120 trans=194 depth=23
[ ] Prop03Sound
     states=120 trans=194 depth=
[ ] Prop04MsgSound
     states=120 trans=194 depth=
---------- Network07RSC ----------
[X] Prop01Type
     states=60 trans=92 depth=20
[X] Prop02Safe
     states=60 trans=92 depth=20
[ ] Prop03Sound
     states=60 trans=92 depth=
[ ] Prop04MsgSound
     states=60 trans=92 depth=
done.

Verification for a single communication model and choosing the properties of interest is also possible but requires some more commands to run (mostly copying files and launching Java, as can be seen in fbpmn-check). We are working on an extension of fbpm-check with options to help there.

When a model is analysed, counter-examples are generated for each property that does not yield.

Using fbpmn-check, the counter examples are in .log files that are generated in the directory of analysis, e.g., in /tmp/e033MBE.T07y4 in the example above.

❯ (cd /tmp/e033MBE.T07y4; ls *.log)
e033MBE.Network01Bag.Prop01Type.log          e033MBE.Network03Causal.Prop03Sound.log      e033MBE.Network06Fifo.Prop01Type.log
e033MBE.Network01Bag.Prop02Safe.log          e033MBE.Network03Causal.Prop04MsgSound.log   e033MBE.Network06Fifo.Prop02Safe.log
e033MBE.Network01Bag.Prop03Sound.log         e033MBE.Network04Inbox.Prop01Type.log        e033MBE.Network06Fifo.Prop03Sound.log
e033MBE.Network01Bag.Prop04MsgSound.log      e033MBE.Network04Inbox.Prop02Safe.log        e033MBE.Network06Fifo.Prop04MsgSound.log
e033MBE.Network02FifoPair.Prop01Type.log     e033MBE.Network04Inbox.Prop03Sound.log       e033MBE.Network07RSC.Prop01Type.log
e033MBE.Network02FifoPair.Prop02Safe.log     e033MBE.Network04Inbox.Prop04MsgSound.log    e033MBE.Network07RSC.Prop02Safe.log
e033MBE.Network02FifoPair.Prop03Sound.log    e033MBE.Network05Outbox.Prop01Type.log       e033MBE.Network07RSC.Prop03Sound.log
e033MBE.Network02FifoPair.Prop04MsgSound.log e033MBE.Network05Outbox.Prop02Safe.log       e033MBE.Network07RSC.Prop04MsgSound.log
e033MBE.Network03Causal.Prop01Type.log       e033MBE.Network05Outbox.Prop03Sound.log
e033MBE.Network03Causal.Prop02Safe.log       e033MBE.Network05Outbox.Prop04MsgSound.log

These files include information about the computation time and the counter-examples themselves in a verbose mode.

[...]
State 13: <Action line 156, col 1 to line 156, col 21 of module e033MBE>
/\ edgemarks = [MessageFlow_0qo10kt |-> 0, MessageFlow_1a8bsa8 |-> 0, MessageFlow_1r7fyxg |-> 0, MessageFlow_091cszi |-> 0, MessageFlow_1tq79cn |-> 1, MessageFlow_1okf1vd |-> 0, SequenceFlow_0nps006 |-> 0, SequenceFlow_1wtnl4z |-> 0, SequenceFlow_0o5vg8x |-> 0, SequenceFlow_0fplzau |-> 1, SequenceFlow_1dte0vc |-> 0, SequenceFlow_0k086s0 |-> 0, SequenceFlow_0698suh |-> 0, SequenceFlow_1wgoun9 |-> 0, SequenceFlow_16ovyt7 |-> 0, SequenceFlow_0mgjt9y |-> 0, SequenceFlow_1xvdo11 |-> 1, SequenceFlow_1y1oo45 |-> 0, SequenceFlow_0rjtib7 |-> 0, SequenceFlow_0k02j79 |-> 0, SequenceFlow_0f0ojke |-> 0, SequenceFlow_1oxapbj |-> 0, SequenceFlow_096ubuj |-> 0, SequenceFlow_0eej3d6 |-> 0, SequenceFlow_0jq12xx |-> 0, SequenceFlow_0v4m6o8 |-> 0]
/\ net = (<<"P_id", "Q_id", "results">> :> 1)
/\ nodemarks = [P_id |-> 1, StartEvent_1 |-> 0, Task_05seu1l |-> 0, Task_0yk02ke |-> 0, BoundaryEvent_1fgc3dg |-> 0, EndEvent_1yasgxk |-> 0, ExclusiveGateway_06st2fh |-> 0, IntermediateThrowEvent_16df5b4 |-> 0, Task_1lnz72e |-> 0, Task_1ypg0u2 |-> 0, Q_id |-> 1, StartEvent_1axpofs |-> 0, Task_0k7ip70 |-> 0, IntermediateThrowEvent_0yo36nb |-> 0, ExclusiveGateway_0phbzc0 |-> 0, IntermediateThrowEvent_1ewiw3i |-> 0, ExclusiveGateway_14e5fg8 |-> 0, IntermediateThrowEvent_0nfi6to |-> 0, EndEvent_0l9fmhf |-> 0, ExclusiveGateway_06aycf0 |-> 0, IntermediateThrowEvent_1s2ehzf |-> 0, IntermediateThrowEvent_1q2mw0e |-> 0]
[...]

To generate versions of the counter-examples that are easier to analyse you can use:

• fbpmn log2json to get a JSON version of the counter-example

  ❯ fbpmn log2json /tmp/e033MBE.T07y4/e033MBE.Network01Bag.Prop03Sound /tmp/e033MBE.T07y4/e033MBE.Network01Bag.Prop03Sound
  transformation done

• fbpmn log2dot to get a graph version of the counter example in the format of the dot command (see here) and then use this command to generate PDF or PNG images.

  ❯ fbpmn log2dot /tmp/e033MBE.T07y4/e033MBE.Network01Bag.Prop03Sound /tmp/e033MBE.T07y4/e033MBE.Network01Bag.Prop03Sound
  transformation done

• fbpmn log2html to generate an interactive counter example exploration page (use the ←/→ keys to navigate between states of the counter example, in combination with the Shiftkey to go the the start/end of the counter example).

  ❯ fbpmn log2html /tmp/e033MBE.T07y4/e033MBE.Network01Bag.Prop03Sound /tmp/e033MBE.T07y4/e033MBE.Network01Bag.Prop03Sound
  transformation done

  An excerpt of a counter example for the model in Fig. 3 is given in Fig. 4.

  

  Figure 4: last state of the animation of the counter example for soundness of the model in Fig. 4 with network unordered semantics.

The first parameter of the three commands is the source .log file and the second one is the target .json/.dot/.html file (no suffixes in both cases, fbpmn adds them given the type of the read/generated file).

In all three cases, the counter-examples are filtered of the markings that are null.

To perform these transformations for all .log files contained in the current directory, we provide you with a fbpmn-log-transform script (in the scripts directory of the source distribution) for which you can precise the kind of files to generate (json/dot/html).

❯ (cd /tmp/e033MBE.T07y4; fbpmn-log-transform html)
transformation done
transformation done
transformation done
[...]

Some models are unbounded (see e.g., models e004 to e006 here). To be able to check these models, you may add constraints to the verification process. For this, given your model is in file myModel.bpmn, create a file myModel.constraint of the form:

CONSTANT ConstraintNode <- <ConstraintOnNodes>
         ConstraintEdge <- <ConstraintOnEdges>
         Constraint <- <Overall constraint defined in termes of ConstraintNode and ConstraintEdge>

The available constraints that you can reuse are defined here are can be extended.

For example, for model e006 we may use:

CONSTANT ConstraintNode <- TRUE
         ConstraintEdge <- MaxEdgeMarking2
         Constraint <- ConstraintNodeEdge

that states that node markings (the maximum number of tokens authorized on a node) is not constrained, that edge markings (the maximum number of tokens authorized on an edge) is 2, and that the overall constraint is to have both the constraint on nodes and the constraint on edges.

To add a new communication model:

1. define your new communication model semantics, say MyNet, in a NetworkMyNet.tla file in $FBPMN_HOME/theories/tla/
2. copy one of the files in $FBPMN_HOME/theories/tla/Configs/ to a new file NetworkNNMyNet.tla in the same directory, with NN being a number different from the existing communication models there
3. in the contents of NetworkNNMyNet.tla change the line of the network implementation definition to refer to your new communication model as defined in step 1.

LOCAL NetworkImpl == INSTANCE NetworkMyNet

To add a new property to verify:

1. define your new property, say MyProperty, at the end of the PWSSemantics.tla file in $FBPMN_HOME/theories/tla
2. create a new file PropNNMyProperty.cfg in $FBPMN_HOME/theories/tla/Configs, with NN being a number different from the existing properties there
3. in the contents of PropNNMyProperty.cfg refer to your property name as defined in step 1.

\* run with -deadlock
SPECIFICATION Spec
INVARIANT TypeInvariant

PROPERTY
  MyProperty

To get help with fbpmn, run fbpmn -h.

➜ fbpmn -h
0.3.8

Usage: fbpmn COMMAND
  formal transformations for BPMN models

Available options:
  -h,--help                Show this help text

Available commands:
  version                  prints the version
  json2dot                 transforms a model from JSON to DOT
  json2tla                 transforms a model from JSON to TLA+
  json2alloy               transforms a model from JSON to Alloy
  bpmn2json                transforms a model from BPMN to JSON
  bpmn2tla                 transforms a model from BPMN to TLA+
  bpmn2alloy               transforms a model from BPMN to Alloy
  sbpmn2tla                transforms a model from space BPMN to TLA+
  log2json                 transforms a TLA+ log from LOG to JSON
  log2dot                  transforms a TLA+ log from LOG to DOT
  log2html                 transforms a TLA+ log from LOG to HTML
  slog2html                transforms a TLA+ space log from LOG to HTML

But for the version command, you must provide two arguments: the source file and the target file for the transformation.

No suffixes are to be given for source/target files when running fbpmn.

The JSON format for a model can be generated from the BPMN format of it, using fbpmn bpmn2json. In general, there should therefore be no need to write out models in the JSON format manually.

Examples of models are given here for files generated from BPMN.

To help in writing the JSON format, fbpmn has a very basic output to the format of the dot command (see here). To transform a JSON file into DOT, run:

fbpmn json2dot sourcefile targetfile

where neither sourcefile nor targetfile have a suffix (the correct ones will be added by fbpmn). Then provided you have dot installed, you can generate a PNG picture for your collaboration, using:

dot -Tpng sourcefile.dot -o targetfile.png