A new verification technique for large processes based on identification of relevant tasks. (January 2015)

• Record Type: Journal Article
• Authors: Mrasek, Richard; Mülle, Jutta; Böhm, Klemens
• Is Part Of: Information systems. Volume 47(2015)
• Page Start: 82
• Page End: 97
• Publication Date: 2015-01
• Subjects: Business process management -- Business process modeling -- Workflow modeling -- Verification -- Model checking -- Petri net; Database management -- Periodicals; Electronic data processing -- Periodicals; Bases de données -- Gestion -- Périodiques; Informatique -- Périodiques; Database management; Electronic data processing; Periodicals; 005.7
• DOI: 10.1016/j.is.2014.07.001
• Languages: English
• ISSNs: 0306-4379

Abstract

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. Abstract : Highlights: Verification allows ensuring that a process complies with domain requirements. The state space for verification tends to increase exponentially. We use a reduction that confines the process model to regions for the verification. For the evaluation we use real-world industrial processes and requirements. Our approach verifies complex processes with many parallel branches in few seconds.