Abstract: The modeling and verification of functional and non-functional constraints is an important means to ensure that business processes achieve their business goals. Controllability verification, which considers environmental factors and constructs control strategies, is more practical than traditional soundness verification. This paper proposes a method of verifying the controllability of business processes, which supports modeling constraints on BPMN business processes, describes the behavior of business processes with Markov decision processes, and verifies controllability with the PRISM model checker. The method can quantitatively verify the controllability of business processes under functional and non-functional constraints, and construct optimal control strategies that make business processes satisfy constraints. This paper analyzes the execution efficiency of the method and explores how to improve execution efficiency.