|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
INRIA Grenoble / CONVECS and CORSE teams (FRANCE)
|
|---|---|
| Functionality: |
Business Processes.
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
Activiti VBPMN |
| Period: |
2024
|
| Description: |
Business processes are structured tasks that model a specific service
or product. Such processes are present in any company or institution
worldwide, and there is a need for better controlling these processes
to reduce costs and improve throughput. Many companies model their
services and processes using various notations, among which BPMN
(Business Process Modelling Notation), thereby increasing their level
of automation. One of the challenges in this context is to ensure the
quality, correctness, and efficiency of these processes.
This work proposes to rely on PMC (Probabilistic Model Checking) to automatically verify that multiple executions of a process respect some specific probabilistic property. This approach applies at runtime, thus the evaluation of the property is periodically verified and the corresponding results updated. Besides performing runtime PMC for BPMN, the approach also considers runtime enforcement techniques to keep executing the process while avoiding the violation of the property. This is achieved by combining monitoring techniques, computation of probabilistic models (by translating BPMN processes to LNT using the VBPMN tools), PMC (using the CADP model checker), and runtime enforcement techniques. The approach has been implemented as a toolchain and has been validated on several realistic BPMN processes. |
| Conclusions: |
The experiments carried out show that without enforcement techniques,
the correctness results present a satisfaction rate below 100%, whereas
this rate is systematically 100% in presence of enforcement.
Although the enforcement mechanism slightly increases the execution
time of the BPMN process, it systematically ensures that the process
executes while preserving the given property.
|
| Publications: |
[Falcone-Salaun-Zuo-24]
Yliès Falcone, Gwen Salaün, and Ahang Zuo.
"Probabilistic Runtime Enforcement of Executable BPMN Processes".
Proc. of the 27th International Conference on Fundamental Approaches
to Software Engineering (FASE'2024), Luxembourg City, Luxembourg,
April 6-11, 2024.
Available on-line at: https://inria.hal.science/hal-04533195/en |
| Contact: | Gwen Salaün INRIA Center of University Grenoble Alpes 655, avenue de l'Europe F-38330 Montbonnot Saint Martin FRANCE Email: gwen.salaun@inria.fr |
| Further remarks: | This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software |
Back to the CADP research tools page