【摘 要】
：
变更后系统实现的安全性验证是安全攸关系统维护过程中必不可少的环节,也是其面临的主要挑战之一.软件模型检测和程序验证是目前常用的作用于代码层面的自动化安全性验证技术.本文站在系统行为角度,基于形式化方法,提出了一种将变更后系统实现的安全性验证问题归结为一致性测试的方法,尝试通过自动生成的一致性测试用例在系统行为级别上判定系统实现是否安全.为此,首先以时间输入输出自动机及其语义模型为基础,构建了该方法
论文部分内容阅读
变更后系统实现的安全性验证是安全攸关系统维护过程中必不可少的环节,也是其面临的主要挑战之一.软件模型检测和程序验证是目前常用的作用于代码层面的自动化安全性验证技术.本文站在系统行为角度,基于形式化方法,提出了一种将变更后系统实现的安全性验证问题归结为一致性测试的方法,尝试通过自动生成的一致性测试用例在系统行为级别上判定系统实现是否安全.为此,首先以时间输入输出自动机及其语义模型为基础,构建了该方法的证明体系,证明了该方法的正确性;其次,建立了变更后系统实现安全性验证的回归测试生成框架.相对于其它实时
其他文献
标准球面上的预定纯量曲率问题已经得到很好的研究,为此,几种不同的方法发展起来了.它的高维对应的问题即预定Q-曲率问题也吸引了众多人的注意.负梯度流的方法在处理此类问题上似乎十分有效,至少在曲率备选函数是正的情形下是如此的.本文的目的在于指出,对于指数非线性增长的预定Q-曲率问题,Q-曲率备选函数的正性假设是不必要的.
如果两个v阶拉丁方L和M的重叠产生恰好r个不同的有序对,则称L和M是r-正交的.如果L还是M的(i,j,k)-共轭,则称L是(i,j,k)-共轭r-正交的,简记为(i,j,k)-r-COLS(v)((i,j,k)-r-conjugate orthogonal Latin square of order v),其中{i,j,k}={1,2,3}.本文研究(3,2,1)-r-COLS(v)的存在性问题
传统的二维断裂理论忽略了各种断裂参数的三维厚度效应,将其应用到三维结构的损伤容限设计及评定中具有明显的局限性.另一方面,工程中存在的裂纹通常具有复杂的形状,并且无法直接考虑其对应的厚度.因此,工程中通常采用最保守的平面应变断裂韧性或固定的裂纹扩展速率曲线来描述裂纹的扩展和断裂,这无疑会带来巨大的误差.事实上,在含裂纹的三维结构中,裂尖局部场总是呈现出复杂的三维应力状态,而裂尖复杂的三维应力场对结构
New schemes with fractal error compensation for PDE eigenvalue computations SUN JiaChang Abstract With an error compensation term in the fractal Rayleigh quotient of PDE eigen-problems,we propose a ne
利用对称空间的对偶性,本文建立局部强凸对称等仿射球之集与某复空间形式中的极小对称Lagrange子流形之集间的对应关系,在自然定义的等价意义下,这是一一对应关系.作为这种对应关系的直接应用,本文用完全不同的方法重新证明胡泽军等人最近建立的一个重要定理.该定理对具有平行Fubini-Pick形式的局部强凸等仿射球进行了完全分类.
从茎瘤芥胞质雄性不育系(CMS)线粒体中克隆的T基因是一个CMS相关基因,它能够通过选择性剪接产生T1170和T1243两个转录本,而T1243是T基因在转录过程中保留了内含子TinⅡ的产物.本实验室前期的实验结果表明,在模式植物拟南芥中过表达T1243(OE-T1243)后,植株表现出明显的雄性不育表型,而OE-T1170植株的表型与野生型无异,然而这一现象的机制却不明确.本研究通过花药石蜡切片
对比分析2005~2008年五种再分析资料和东南极地区气象站实测的日平均2 m气温,结果表明:五种再分析资料都能够解释超过70%的方差,年均方根误差为3.4~6.9℃.三种NOAA再分析资料NCEP-1,NCEP-2和20CRv2呈现冷偏差(分别为2.5,1.4和1.5℃),ERA Interim和JCDAS呈现暖偏差(分别为1.7和2.0℃).五种再分析气温通常在(南半球)春季适用性强,冬、秋季
利用联合生物加工工艺生产第二代燃料乙醇(纤维素乙醇)是国内外的研究热点.前期的研究结果表明,酿酒酵母分泌或展示非复合型纤维素酶体系的应用效果并不理想,而复合型纤维素酶体系(即纤维小体)因对纤维素的降解能力比非复合型纤维素酶体系更强,所以其在酿酒酵母细胞表面的组装研究受到越来越多的关注.目前,单支架和双支架纤维小体在酵母细胞表面的完全自组装以及多细胞协同参与的非完全自组装均已实现.纤维小体展示型酿酒
演化是计算机软件的固有特性.了解演化规律,可以改进软件演化过程,提高软件质量,降低维护成本.本文定义类依赖图,将软件系统描述为软件网络,基于网络度量验证软件演化规律,并讨论软件演化建模的可行性.首先针对Lehman的8项演化定律,设计3个方面的网络度量:网络规模、网络质量、以及结构控制.然后基于四个开源软件系统构建软件网络,统计网络度量;实证研究表明:支持Lehman的4项演化定律,否定另外3项,
程序理解是一个从计算机程序中获取知识信息的过程,其主要目的是获取软件的各种有关知识以理解开发者的意图,从而支持针对现有或遗产软件系统进行软件评审、错误定位、反向工程、再工程、迁移、维护和复用等软件工程实践.本文提出一种设计模式指导的分簇方法,该方法采用程序中蕴涵的设计模式信息指导开源软件的分簇,运用"分而治之"的策略辅助程序开发者和维护人员快速、方便地理解代码.首先,采用设计模式检测技术从程序代码