GIVUP: Automated Generation and Verification of Textual Process Descriptions

A business process is defined as a set of tasks executed in a certain order to achieve a specific goal. Business Process Model and Notation (BPMN) has become the standard modelling language for describing and developing business processes. One of the main challenges in the business process management area is to provide techniques and tools for analysing and optimising processes, which are necessary for example to avoid bugs or unexpected process executions. However, modelling and debugging processes is a difficult task. This paper presents GIVUP, a tool that takes as input descriptions of a process and of a functional property written in natural language. GIVUP transforms the textual process into BPMN and the textual property into the corresponding Linear Temporal Logic (LTL) formula. It then verifies whether the BPMN process satisfies the property or not, in which case it returns a diagnostic. These steps are achieved by using several internal transformations and model checking techniques. This approach is helpful for any kind of users, either novices or experts, and can be used during several stages of the lifecycle of a process, such as the design phase or any refinement phase. GIVUP is freely accessible online, and a demo video can be found at: https://youtu.be/MdM4NaPQXMk.