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

项目名称： 软件演化过程的行为验证研究

项目编号： No.61262024

项目类型： 地区科学基金项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 李彤

作者单位： 云南大学

项目金额： 43万元

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

中文关键词： 软件演化过程；过程验证；行为验证；Petri 网；ACP

英文摘要： 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

英文关键词： software evolution processes；process verification；behavior verification；Petri Nets；ACP