一句话：GIVUP 将自然语言流程与属性转为 BPMN 和 LTL，并用模型检测验证，不满足时给出诊断。
业务流程通常用 BPMN 建模，但建模与调试困难，且需要分析优化以避免错误或不期望执行。本文提出工具 GIVUP，输入自然语言描述的流程和功能属性；它通过内部转换将文本流程生成 BPMN 模型，将文本属性转换为线性时序逻辑（LTL）公式，再用模型检测判断 BPMN 流程是否满足该属性，若不满足则返回诊断信息。该工具面向新手和专家，可辅助流程设计及精化阶段。GIVUP 已在线公开并提供演示视频，展示了其可用性。
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.