Process Verification Of Complex Information Systems And Implementation Of Unified Modeling Platform

The features of complex information system are that complex process es, stronger concurrency and multi-branch node. If discover system existen ce question after completed, the cost of changing the system would be m uch worse. For this, we need to model system, to check deadlock and liv elock problems of system processes. In order to provide a user-friendly sy mbol, BPMI developed a set of standard Business Process Modeling Notat ion. However, since BPMN is a semi-formal language, it can not be dedu ced by itself to find the problems of model. Therefore, it is necessary to provide a method to verify for BPMN model. For complex information sy stem of stronger concurrency, model checking is exhaustive search to the state space that state explosion is inevitable, therefore, we should find a method to reduce the chance of state explosion.To tackle the problems of non-unified platform and poor portability in business process design, formal analysis and verification phase, introduces a formal verification protocols which based on our unified modeling platform to process the output processes of Business Process Model Notation(BPMN2.0)model is introduced. First of all, the formal modeling platform is built based on Java language and its input is directly from the output of BPMN model. Then, aJava code based verification approach for Business Processes Modeling method is proposed by using the BPMN 2.0 standard. In this way after the modeling phase, the created Java code can be automatically run in order to find out possible deadlocks and livelocks and solve the problem of state explosion caused by livelocks by setting the "cut-off " point. Finally, complex information system corresponding instances are introduced to demonstrate the effectiveness of our method. The main work includes the following aspects:1. Analyzes the business process validation methods and summed up the mapping for core elements of the BPMN model to Petri net and core elements of the BPMN model to π- calculus. The two validation methods existing problem that they don’t have a unified platform to verify for BPMN model, therefore, the paper propose a verification methods based on the unified Eclipse modeling platform.2. According to the mapping idea of various verification algorithms,we made the core element of BPMN model packaged as java class. Then,the BPMN model converted into java code firstly, and then run the java code to find out possible deadlocks and livelocks.3. Add a mark named "cut-off " to unfolding. The processes identify the cutoff point and then end the same path search, thus can reduces the chance of state explosion.According to comparing the methods of verification of BPMN processes based on the unified modeling platform, verification BPMN Business Process ofPetri nets and verification BPMN Business Process of π- calculus, we can draw the former method can complete the whole modeling and verification work in a unified platform and simplify the verification steps. And according to compare number of primitives and search paths of BPMN and Petri nets, we can draw that BPMN is relatively low complexity in describing complex system and the chance of state explosion can be reduced by reducing the state space and the search path.