Based Epmm Software Evolution Process Model Validation

Recently, software evolution has become the most important form in the software life cycle and a hot area of software engineering research. On the one hand, the software evolution process can construct a framework of tasks to support software evolution and is considered as an important technology which is used to improve the quality and efficiency of software evolution. On the other hand, with a large number of software evolution process models modeled by a variety of process modeling tools, how to verify the correctness of these models becomes the urgent needs.In the field of software process, software process modeling and verification are two key activities. However, the discussion and research related to software process verification are not as good as that of software process modeling. Specifically, from the perspective of properties, existing literature on software process verification is mainly focused on structure verification and property verification. With the lack of behavior verification, it can't guarantee that process models'behavior is consistent with their specification. From the perspective of methods, existing verification methods based on Petri Nets can be divided into four categories, namely state space based verification methods, structure based verification methods, logic reasoning based verification methods and algebraic nets based verification methods. However, they cannot well support behavior verification, so their application is very limited. Therefore, existing literature can not well solve the problems of software process verification.This thesis proposes a process algebra verification approach based on Petri Nets to verify software evolution process models modeled by evolution process meta-model. Specifically, it addresses the following problems:(1) With respect to verification theory, as the existing research related to software process model verification which is mainly focused on structure verification and property verification, the theory of behavior verification is proposed. From the viewpoint of semantics, it uses process algebra's equation derivation to ensure that process models' behavior be consistent with their specification.(2) With respect to verification methods, as the existing software process verification methods based on Petri Nets, such as state space based verification methods, structure based verification methods, logic reasoning based verification methods and algebraic nets based verification methods, cannot well support behavior verification, a process algebra verification method based on Petri Nets is proposed. This method not only verifies the structure and the dynamic properties of software evolution process models, but also verifies the behavior of software evolution process models.(3) With respect to verification techniques, on the one hand, Petri nets-related technologies are used to specify and verify the structure and properties of software evolution process models, on the other hand, ACP-style process algebra is used to specify and verify the behavior of software evolution process models. Specifically, when verifying the structure and the properties of a software evolution process model, the verification approach uses the abstract operation to effectively reduce the number of its nodes according to property preservation so that the corresponding algorithms can avoid state space explosion; when verifying the behavior of a software evolution process model, according to its algebraic semantics, the verification approach uses algebraic derivation to support algebra reasoning instead of model-based reasoning.(4) With respect to process improvement, four types of process model improvement operations are systematically proposed, namely, insertion operation, deletion operation, refinement operation and abstract operation.In summary, this thesis proposes the theory of behavior verification, the process algebra approach based on Petri Nets and related verification techniques to support structure verification, property verification and behavior verification of a software evolution process model modeled by EPMM.