Abstract:

The solution against the changing business environment is construction of flexible business processes in order to be aligned with actual business needs and requirements. The reliability of a business process can be increased through modelling of the process before the implementation of code, followed by the verification of its correctness. Verification of a business process involves checking whether the process in question behaves as it was designed to behave. Model checking is a technology widely used for the automated system verification and represents a technique for verifying that finite state systems satisfy specifications expressed in the language of temporal logics. Formal verification of business process model aims checking for process correctness and business compliance. This paper presents a suitable approach for automatic verification of a business process using Alternating-time Temporal Logic (ATL). In development of a user-friendly supporting tool, we will use our original ATL model checker.