论文部分内容阅读
本文在EPMM的基础上,建立了以CCS为主要形式工具的软件演化过程的元模型CEPMM,它以任务不可分割为前提,支持软件演化过程全局层、过程层和活动层的形式建模与验证。本文致力于基于CEPMM建立的软件演化过程的建模,性质验证及性能评价,论文的主要工作如下。(1)在全局层和过程层,提出了EPMM白盒方法建模与CEPMM建模的转化准则,在活动层,本文定义一种AML(Activity Modelling Language)非形式化规约语言,对活动建立非形式描述,同时给出了根据AML非形式规约借助于进程二叉树为活动的建模方法。(2)本文提出对模型的进行局部范围内的性质验证,为此定义了待验证的对象和DFA子活动概念,通过模型分解来挖掘模型中性质分析验证的对象。(3)对基于CEPMM建立的软件演化过程模型的结构合理性进行验证,即对模型的安全性与可达性进行验证。本文引入正则表达式来描述验证的性质,并分别针对模型的安全性和可达性的提出了正则表达式描述的方法,最后使用标号迁移系统LTS方法结合有限自动机提出有效的安全性与可达性验证方法。在模型验证中,借鉴CRA组合可达性分析的思想,为模型挑选安全性验证对象和可达性验证对象,对该模型安全性验证对象的集合下的划分中每个划分块的哈斯图,从哈斯图的极小元开始验证,对模型中安全性验证对象逐层进行验证,该方法在大大缩减状态空间的前提下,可以及时准确得定位模型中的问题使建模者能及时对模型进行改进,对可达性验证对象的集合下的划分中每个划分块的哈斯图每个划分块的最大元进行验证。(4)资源与软件演化过程性能密切相关,为此本文对软件演化过程涉及到资源进行分析,为资源进行分类,并根据每类资源的特点对其属性进行分析。(5)本文对软件演化过程的性能分析,为了支持软件演化过程进行性能评价,将进程代数CCS扩展了时间概率成本进程代数TCPCCS, TCPCCS支持软件演化过程时间、概率以及成本的分析,分析的结果可以作为决策的参考依据。