软件演化过程的行为验证研究

Software process verification has evolved in response to a pervasive need for a research that ensures expectations of a modeler of software process modeling and improves the validity of software process implementation. How to verify behavior of software processes is a significant challenge in the field of software process engineering. To address this issue, this research is conducted to establish the theoretical basis for behavior verification, regarding the software evolution process model modeled by EPMM (Software Evolution Process Meta-Model). Moreover, the corresponding verification approach and process model improvement operatios are proposed. Three strands of research are discussed: 1) EPMM-PA (Software Evolution Process Meta Model-Process Algebra) is proposed, which extends EPMM with ACP (Algebra of Communicating Processe). In order to discuss behavior verification in the unified framework of EPMM-PA, a process term is used to define an algebraic semantics of a software evolutio process model so as to verify whether its behavior meets process specification, using equational reasoning of EPMM-PA. 2) an algebra verification approach based on Petri Nets is proposed to verify the structure, properties and behavior of the modeled software evolution process model, combining the advantages of both Petri Nets and ACP. 3) process model improvement operations are systematically proposed to modify the unauthenticated process models. This research proposes theoretical basis, approach and prototype tools of formal behavior verification of the software evolution process that will trigger step change in the way software process verification.

软件过程验证是软件过程建模的后续研究，可以确保过程模型符合建模者的期望，提高过程实施的有效性。针对现有过程验证研究缺乏行为验证的不足，在已有软件演化过程建模的基础上，建立支持行为验证的理论基础，提出支持行为验证的验证方法，设计过程模型改进操作。采用通信基础代数ACP对已有软件演化过程元模型进行扩展，提出软件演化过程元模型进程代数，使用进程项指定软件演化过程模型的代数语义，进而在进程代数的统一框架下，基于公理系统，使用等式推理验证软件演化过程的行为是否满足过程规约；以此为基础，充分结合Petri网和ACP的长处，提出基于Petri网的进程代数验证方法，支持软件演化过程结构、性质和行为的形式验证，并使用过程模型改进操作对不能通过验证的过程模型进行修改，提高过程模型的可靠性。本课题建立支持软件演化过程行为验证的理论基础、方法和工具原型，为软件过程验证的进一步研究提供新方法和理论依据。

软件过程验证是软件过程建模的后续研究，可以确保过程模型符合建模者的期望，提高过程实施的有效性。针对现有过程验证研究缺乏行为验证的不足，首先，采用通信基础代数ACP对已有软件演化过程元模型进行扩展，提出软件演化过程元模型进程代数，使用进程项指定软件演化过程模型的代数语义，进而在进程代数的统一框架下，基于公理系统，使用等式推理验证软件演化过程的行为是否满足过程规约，建立了支持行为验证的理论基础；其次，针对软件演化过程模型的结构、性质和行为，分别提出了结构合理性验证方法、性质合理性验证方法和行为验证方法；最后，从模型改进的角度，提出了插入操作、删除操作、抽象操作和细化操作，用于修改不能通过验证的过程模型。本课题建立支持软件演化过程行为验证的理论基础、方法和工具原型，为软件过程验证提供了新方法和理论依据。