A new verification technique for large processes based on identification of relevant tasks |
| |
| Affiliation: | 1. Vienna University of Economics and Business, Austria;2. University of Tartu, Estonia;3. Free University of Bozen-Bolzano, Italy;1. Eindhoven University of Technology, P.O. Box 513, Eindhoven 5600 MB, The Netherlands;2. Vrije Universiteit Amsterdam, De Boelelaan 1081, Amsterdam 1081 HV, The Netherlands;3. Norwegian University of Science and Technology, Trondheim 7491, Norway;1. Insight Centre for Data Analytics, National University of Ireland, Galway (NUIG), Ireland;2. OASIS, National Engineering School of Tunis, University Tunis El Manar, Tunisia;1. Vienna University of Economics and Business, Institute for Information Business, Welthandelsplatz 1, 1020 Vienna, Austria;2. University of Tartu, Institute of Computer Science, J. Liivi 2, 50409 Tartu, Estonia;3. Free University of Bozen-Bolzano, KRDB Research Centre for Knowledge and Data, Piazza Domenicani 3, 39100 Bolzano, Italy |
| |
| Abstract: | Verification recently has become a challenging topic for business process languages. Verification techniques like model checking allow to ensure that a process complies with domain-specific requirements, prior to the execution. To execute full-state verification techniques like model checking, the state space of the process needs to be constructed. This tends to increase exponentially with the size of the process schema, or it can even be infinite. We address this issue by means of requirements-specific reduction techniques, i.e., reducing the size of the state space without changing the result of the verification. We present an approach that, for a given requirement the system must fulfill, identifies the tasks relevant for the verification. Our approach then uses these relevant tasks for a reduction that confines the process to regions of interest for the verification. To evaluate our new technique, we use real-world industrial processes and requirements. Mainly because these processes make heavy use of parallelization, full-state-search verification algorithms are not able to verify them. With our reduction in turn, even complex processes with many parallel branches can be verified in less than 10 s. |
| |
| Keywords: | Business process management Business process modeling Workflow modeling Verification Model checking Petri net |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
