This is an analyzer for BPMN models, i.e., a BPMN-specific model checker written in Rust. It can parse BPMN files and analyze them for specific properties. The analyzer can detect deadlocks, livelocks, and other properties of BPMN models.
The Analyzer is structured into four crates:
core
: The core functionality of the analyzer, i.e., analyzing BPMN models (library).cli
: A CLI application providing BPMN analysis (binary).webserver
: A web server providing BPMN analysis as a service (binary).wasm
: The WebAssembly crate provides bindings to web assembly to analyze BPMN models on the client-side in the browser.
This crate contains the core functionality of the analyzer. See a detailed description on my website.
This binary crate is a CLI application to analyze BPMN models. The following command lists the available options:
cargo run -- -h
One can run the CLI application for a specific BPMN model and a set of properties like this:
cargo run -- -f benchmark_input/p10x01.bpmn -p safeness,option-to-complete,proper-completion,no-dead-activities
Build an optimized binary that can be used as shown above:
cargo build --release
This binary crate provides a web server with a web service to analyze BPMN models.
The webserver is available locally by running main.rs
, using docker, or online.
The web server serves not only the analyzer but also a custom BPMN editor to create BPMN models and get instantaneous feedback, counter examples, and quick fixes for the checked properties. See a detailed description on my website.
The webserver is available using docker. Building the image is done using GitHub actions (see release.yml).
Pull the application image:
docker pull tkra/rust_bpmn_analyzer
Run the application image:
docker run -p 8080:8080 tkra/rust_bpmn_analyzer
This crate provides wasm bindings to run BPMN analysis directly in the browser on the clients' machine. A demo using the WASM bindings is available here.
Install wasm-pack using (see documentation):
cargo install wasm-pack
Run the following command in the ./wasm
directory to cross-compile to WASM:
wasm-pack build --target web --out-dir ../../bpmn-analyzer-js/src/lib/analysis/wasm/generated
The output can be found in ../../bpmn-analyzer-js/src/lib/analysis/wasm/generated
.
The analyzer supports the green BPMN elements. We follow the structure of the Camunda 8 documentation.
Multiple pools are supported. The Analyzer will start one process for each pool and then analyze the given properties.
Call Activities are handled as tasks, i.e., we assume they terminate after a certain time.
All tasks are handled identically except Send/Receive tasks, which send/receive messages.
Markers, data, and artifacts are ignored.