Using CIMOSA and free-choice Petri nets for modeling and verification of manufacturing enterprise business processes

To deal with today's frequently changing and complex business processes, this paper presents a structured modeling algorithm for manufacturing enterprise business processes by using CIMOSA behavioral rules and free-choice Petri nets. The well-behaved properties such as liveness and boundedness are critical for enterprise business processes. They enable the avoidance of possible deadlock, endless loops and dangling tasks in process models. However, for complex systems, the checking of the well-behaved property is a NP-hard problem. In this paper, a structured process modeling algorithm is presented. The resulting process models from this algorithm are free-choice Petri nets whose well-behaved property can be decided in polynomial time. The process models resulted from this algorithm also have the advantages of modularity, readability and maintainability.