论文部分内容阅读
本论文的研究工作主要包含了以下几个方面：1)提出了软件演化过程模型验证语言CEPDL (Concise Evolution Process Description Language);2)证明了白盒建模软件演化过程模型的结构优良性；3)利用CEPDL语言对软件过程模型进行了动态性质验证；4)构建了软件演化过程模型行为图的行为规约并且利用CEPDL语言对软件演化过程模型进行了行为验证。CEPDL语言是在文献[3]中所提出的软件演化过程元模型EPMM (Software Evolution Process Meta-Model)基础上发展而来的。文献[3]基于基本Petri网,扩展了面向对象技术和Hoare逻辑,提出了EPMM,有效的解决了软件演化过程的形式建模问题,但是,描述EPMM的语言EPDL只能对软件演化过程模型进行描述,不能描述过程模型的性质。CEPDL语言增加了基于线性时序逻辑的性质描述模块,可以充分的描述模型的性质规约,从而使得验证人员能够使用模型检测方法对软件演化过程模型的性质规约进行验证。给出了白盒建模的软件演化过程模型的关联矩阵描述以及细化操作的关联矩阵表示方法。利用关联矩阵证明了通过白盒建模的软件演化过程模型具有有界性、守恒性等等Petri网的经典结构性质。利用CEPDL语言对软件演化过程模型的进行了动态性质验证。传统的性质验证方法只能验证情态与情态之间的动态性质。本文采用了符号化模型检测的方法,提出了新的验证方法,给出了条件间强可达性等描述条件与条件之间的动态性质的定义,并且实现了这些动态性质的验证。利用CEPDL语言对软件演化过程模型进行了行为验证。现有的软件演化过程模型的验证方法缺乏对行为的验证,无法保证过程模型的行为与过程规约一致,代提出了对EPMM手动的行为验证,验证人员需要有强大的理论知识背景,手动的计算出过程模型的行为与规约的一致性,在工业界实现困难,使得其应用受到了很大限制。本文采用符号化模型检测的方法,建立行为图,基于线性时序逻辑对软件演化过程模型的行为进行规约,应用CEPDL模型验证语言对行为图和行为规约进行了描述,完成了软件演化过程的模型验证工具SEPMC(Software EvolutionProcess Model Checking),实现了对软件演化过程模型行为验证的自动化。