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

Towards an Algebraic Semantics of Software Evolution Process Models

随着大量的软件演化过程模型被软件演化过程元模型建模产生,如何验证过程模型的正确性,是摆在人们面前的一个重要任务.针对软件演化过程元模型,引入进程代数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.