软件模型代数性质的程序化验证

Program Verification of Software Model's Algebraic Properties

软件模型代数的思想是通过引入进程代数来对软件体系结构进行建模。它将构件解释为变量,将连接子抽象为代数运算,并针对软件的特性建立了软件体系结构代数模型。在代数模型的基础上,讨论分析获得一系列能指导软件演化的代数性质。但是,上述研究都只对模型的代数性质进行了理论证明,实际上并无程序能够证明这些代数性质的正确性,同时也未给出这些性质的应用方法,使其缺乏可操作性。采用程序化验证的方法对代数性质进行了验证,并对这些性质的应用算法进行了研究,进一步丰富了软件的建模理论,也使得软件演化从理论研究转化为实际应用成为可能。

Software model algebra is introduced to model software architecture by process algebra.It explains components as variables,abstracts connector as algebra operation,and builds the algebraic model of software architecture according to software features.Based on the discussion about algebraic model,we got a series of algebraic properties to guide software evolution.However,these studies have only theoretically proved the algebraic properties of the mode,no program can actually prove the correctness of these algebraic properties,and they did not give the property applications,making them lack maneuverability.This paper researched the algebraic properties of algorithms,did program verification,further enriched the software model,and also made it possible to change software evolution from theory into practical applications.