This chapter provides a formal specification of non-atomic, relaxed action refinement suited for component-based business process engineering. Engineering a business process involves multiple process models created by different people on different levels of abstractions. Keeping the models consistent during the engineering procedure—refinement validation—is one objective of this chapter. In component-based software engineering, the lowest abstraction of a business process is mapped on existing components that have a description of their behaviors. Checking the consistency of process and component behavior—grounding validation—is the second objective. Both refinement and grounding validation increase the robustness of business process implementations and the productivity of process engineers. Technically, the specification given in this chapter is in terms of deadlock analysis in safe Petri nets. The evaluation of this straight-forward implementation underlines the exponential complexity of deadlock analysis in safe Petri nets. For use cases with more than 30 activities per process or heavy parallelism, optimized implementations are needed.
Deadlock analysis and control based on Petri nets: A siphon approach review
