Research On Formal Verification Technologies Of ASBS Based On Reflective Petri Nets

With the development of SOA and Web service technologies, more and more software systems are implemented using SOA architecture. These systems are called service based software systems. Service based software systems needs to collect runtime information of themselves and the environment in an open and continuous operation environment, actively or passively adapt and adjust in the whole life cycle, guarantee behavior meet the expected goal in the micro and macro objectives, and have the adaptive ability. As a result, they are Adaptive Service Based System (ASBS). Academia and industry have been researching ASBS system from different aspects, and make a lot of achievements, but there still exist the following shortcomings:what kind of formal model should be based on to define and simulate the dynamic changes of ASBS system, which is the core problem needs to be solved; how to define the evolution strategy during the ASBS adjustment procedure to make evolution strategy flexible for different kind of evolution scenes; in facing offline evolution, how to determine whether the evolution strategy result maintains the system process consistency; and in facing online evolution, what kind of standard should be based on to judge whether the replacement strategy can be normally executed during the adjustment process.Because ASBS system has self-adaptive characteristics, the formal tools to validate and analysis the ASBS system need to consider continuously change and adjustment. This dissertation extends the existing reflected Petri-net model to puts forward a colored reflected Petri net model, which models ASBS system from two aspects of the system itself and the change of the system; define and describe the evolution strategy from two aspects of online and offline evolution of the ASBS system, and propose an evolution strategy generation algorithm; according to the consistency problem of offline evolution process, proposes the process consistency analysis and determination method from the aspects of control flow and data flow; according to which standard should be based on to effectively replace services in online evolution, proposes replaceable analysis and determination method based on the service behavior effect. This dissertation researches on the following aspects.(1) The dissertation puts forward a reflected Petri net ASBS evolution model. Based on that the ASBS need to adapt and adjust to the external changes dynamically, this dissertation proposes a reflected Petri net model to model the system itself and change separately, which fully expresses ASBS system self-adaptive characteristics. But the reflected Petri net base model has shortages in describing the semantics of the composite service, this dissertation extends existing reflected Petri net model and puts forward colored reflected Petri net model. This dissertation models ASBS system based on the colored reflected Petri net model, and describes the process of modeling, which lays foundation for validation and analysis of the ASBS system. Using the online shopping system modeling as an example, this dissertation shows the colored reflected Petri net model can effectively support modeling of the ASBS system.(2) The dissertation puts forward the ASBS evolution strategy generation algorithm. The ASBS system is in a changing environment. On one hand, it needs online real-time adjustment to respond to the change of external environment, on the other hand, the system needs offline process structure adjustment oriented to the change of user requirement and system design. In order to support ASBS oriented to different adjustment of change scenes, this dissertation defines service replaced oriented and process reconstruction evolution strategy from aspects of online and offline. When ASBS is reconstructing its process, as users defined the process describing documents before and after the change, this dissertation put forward an evolution strategy generation algorithm based on the idea of graph-edit-distance, and shows the algorithm is correct and effective through examples.(3) This dissertation solves the consistency problem oriented to offline evolution. When ASBS system runs to a certain stage, in order to satisfy the new business requirements, the system will execute the evolution strategy and re-configuration. In the re-configuration process, the system needs to analyze and validate the process consistency during the evolution process to ensure the normal execution. This dissertation put forward a consistency verification method based on colored reflected Petri net model from two aspects of control flow and data flow of the ASBS system. Control flow consistency verification mainly analyzes the flow structure by determining if there is dead lock or death transition. Data flow consistency mainly analyzes the data dependencies, and determines the data redundancy, data mismatch of the process. Combining both of the methods, this dissertation realizes process consistency analysis of ASBS system oriented to offline evolution.(4) This dissertation solves the problem of service replaceable of online evolution. When ASBS system conducts online adjustment dynamically, if there is new service in the network or some service became unavailable, this is the time that dynamic service replacement is needed. Analysis of replaceable service is an important problem resolving service seamless integration and coordination.In the behavior based composite service scene, considering the behavior effect based service replaceable determination method, by defining the service behavior model, the service behavior effect, behavior consistency and service replaceable degree, combined with the Petri net transformation theory to calculate the service replaceable degree, this dissertation implements the service replaceable analysis based on service behavior effect.