一种软件演化过程模型的代数语义  

Towards an Algebraic Semantics of Software Evolution Process Models

作　　者：代飞[1,2] 李彤[1,2] 谢仲文[1] 于倩[1,2] 卢萍[1] 郁涌[1,2] 赵娜[1,2] 

机构地区：[1]云南大学软件学院,云南昆明650091 [2]云南省软件工程重点实验室(云南大学),云南昆明650091

出　　处：《软件学报》2012年第4期846-863,共18页Journal of Software

基　　金：国家自然科学基金(60963007);云南省软件工程重点实验室开放基金(2010KS01;2011SE04)

摘　　要：随着大量的软件演化过程模型被软件演化过程元模型建模产生,如何验证过程模型的正确性,是摆在人们面前的一个重要任务.针对软件演化过程元模型,引入进程代数ACP(algebra of communicating processes)对其扩展,提出软件演化过程元模型代数,使用进程项指定软件演化过程模型的代数语义,在进程代数的统一框架下,基于等式推理验证软件演化过程模型的行为,使行为验证方式从模型推导变为代数推导.这种方法充分结合了Petri网和ACP的长处,可以有效地支持软件演化过程的形式验证.As a number of software evolution process models increased, as modeled by EPMM （software evolution process meta model）, verifying the correctness of these models becomes the important. This paper extends EPMM with ACP （algebra of communicating processes） and proposes EPMM-A （software evolution meta model- algebra）. In order to discuss behavior verification in the unified framework of EPMM-A, a process term is used to define an algebraic semantics of a software evolution process model. Based on equational reasoning of EPMM-A, behavior verification of a software evolution process model emphasizes algebraic reasoning as opposed to model- based reasoning. This method combines the advantages of both Petri nets and ACP, which can effectively support software evolution process formal verification.

关 键 词：软件演化过程 过程验证 代数语义 PETRI网 ACP(algebra of COMMUNICATING processes) 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]