一种验证软件演化过程行为的代数推导方法

An algebraic reasoning approach for verifying behavior of software evolution processes

针对现有软件过程验证主要以结构验证和性质验证为主,缺乏行为验证的不足,提出了一种验证软件演化过程行为的代数方法.该方法使用通信进程代数ACP对软件演化过程元模型EPMM进行扩展,提出软件演化过程元模型代数EPMM-A.针对EPMM建模产生的软件演化过程模型,一方面使用EPMM-A形式定义软件演化过程模型的行为规约,另一方面在其公理系统的支持下,基于等式推导验证软件演化过程模型的行为与行为规约是否一致,使行为验证方式从模型推导(非形式化)变为代数推导(形式化).为了说明代数推导的正确性,证明了软件演化过程元模型代数的公理系统具有可靠性.

To solve the lack of behavior verification in existing software process verification due to the main considerations of structure verification and property verification, an algebraic reasoning approach was proposed for verifying behavior of software evolution processes. The software evolution process meta model （EPMM） was extended with algebra of communicating process （ACP） to propose software ew,lu- tion process meta model algebra（EPMM-A）. According to the software evolution process models modeled by EPMM, EPMM-A was used to define behavior specification formally. Based on the axiom system of EPMM-A, equational reasoning was used to verify whether the behavior of software evolution pocess models met the behavior specification. The algebraic reasoning was emphasized to model-based reaso- ning. The results show that the axiom system of EPMM-A is reasonable.