Software Evolution Process Models Verification Based On Symbolic Model Checking

This thesis is a study of formal verification about software evolution process model which is modeled by evolution process meta-model (EPMM). The research work discussed in this thesis includes the following aspects:1) A software evolution model verification language CEPDL (Concise Evolution Process Description Language) is proposed;2) The good properties of the structure of white box modeling approach for software evolution process model are proved;3) The dynamic properties of software evolution process model is verified using CEPDL language;4) The behavior of software evolution process model is verified.CEPDL language is developed based on the EPMM proposed by Li. EPMM which is based on basic Petri net effectively supports modeling problem of software evolution process with formulation. A language for describing EPMM is also developed by Li named EPDL. However, the EPDL only supports the description of software evolution process model. The properties of the process model cannot be described using EPDL. CEPDL language includes a properties description module based on linear temporal logic, which can fully describe the property specification of the model and the proof is checked by modelers automatically using model checking approach.In this thesis, we use correlation metrices to describe the software evolution process model which modeling by white box approach and the refining operations between them. The structure properties are verified using correlation metrices such as the boundedness, the conservativeness and so on.The dynamic properties of software evolution process model can be verified in CEPDL language using the symbolic model checking technique. Traditional approach can only verify the dynamic properties between case and case. In this thesis a new verification method is proposed based on symbolic model checking approach. The describe conditions like strong reachability between conditions and dynamic properties between conditions is defined. Moreover, the verification of these dynamic properties is implemented.The CEPDL language can also describe the behavior of software evolution process model. Existing verification tools can’t verify the behavior of software evolution process model and the consistency of model behavior and process specification is not guaranteed. Although the verification method proposed can verify the model behavior manually, the users need strong theoretical background to verify the consistency of model behavior and specification which strongly limits EPMM’s application in industry. In this thesis, firstly, behavior graph is built. Furthermore, the software evolution process model is verified using symbolic model checking technique based on linear temporal logic. CEPDL can describe the behavior graph and also process specification which considered as the input language of the verification tool SEPMC (Software Evolution Process Model Checker), and achieve automatic validation of the behavior of software evolution process model.