【摘 要】
：
本文应用模型检验方法对软件进行验证要解决软件的无穷状态空间问题，提出的谓词抽象方法将软件无穷的状态空间抽象为基于一组谓词表示的有限状态自动机，抽象过程使用最弱前置条件和定理证明工具直接对软件源代码自动进行，并能保证如果待验证的安全性质在抽象模型中满足，则其在程序中也满足。谓词抽象的精度取决于所选用的谓词集合，验证过程使用了基于反例的抽象精化思想，利用验证产生的伪反例路径推断出新的谓词不断精化模型，
【机 构】
：
国防科技大学计算机学院，湖南长沙410073
论文部分内容阅读
本文应用模型检验方法对软件进行验证要解决软件的无穷状态空间问题，提出的谓词抽象方法将软件无穷的状态空间抽象为基于一组谓词表示的有限状态自动机，抽象过程使用最弱前置条件和定理证明工具直接对软件源代码自动进行，并能保证如果待验证的安全性质在抽象模型中满足，则其在程序中也满足。谓词抽象的精度取决于所选用的谓词集合，验证过程使用了基于反例的抽象精化思想，利用验证产生的伪反例路径推断出新的谓词不断精化模型，从而可以全自动地完成对程序安全性质的验证。
其他文献
随着信息产业的迅猛发展，新的网络应用、网络服务不断出现，但其发展中的潜在危机也日益暴露，如传输速度瓶颈、带宽利用率低下、网络拥塞现象严重等。这些情况让人们意识到传统网络的协议已经不能适应新的网络环境的发展。尽管人们针对新的问题对旧的协议做了很多修改，但是这些修改往往只针对其中的某一个问题或某一方面，而忽略了对其它的问题的考虑。在认真研究网络体系结构特点的基础上，通过对体系结构的扩充，本文提出了一个
基因表达式编程(GEP)是一种用固定长度的线性染色体表示不同大小和形状的非线性实体(表达式树)的新遗传算法。本文提出了表达式树的一种新构造方法，以及相应的新解码方法(GPED)，该方法在评价个体适应度时不必构造和遍历表达式树而直接得到后缀表达式，从而可大大减少演化时间。文中对 GPED 有关的定义和性质作了详细地阐述，并通过实验对 GPED和基本 GEP 解码方法进行了对比研究。最后，基于GPED
GVF Snake 动态轮廓模型是提取图像中物体轮廓的一种有效方法，较好地解决了传统Snake 模型中存在的轮廓线初始化、检测“U 型”物体轮廓等问题。本文在详细分析 GVF Snake 模型的基础上，指出其不足之处，即 GVF Snake 模型不能够逼近“? 型”轮廓。文中通过修改 GVF 力场，对 GVF Snake 模型进行了改进。实验结果表明，新的算法保留了 GVF Snake 模型的所有
该文针对姓名样本库和姓名语料库统计姓氏的各种概率信息，得到了姓氏的三组数据 X(i)、Y(i)、Z(i)，分别表示姓氏的常用程度、姓氏字的常用程度、该姓氏字在真实文本中成为真姓氏的概率。利用这三组数据，我们提出了基于姓氏优先级的中文姓名识别方法。基于本文开发的中文姓名识别系统在实验中召回率和准确率分别为 80.61﹪、89.27﹪，达到了一定的实用性。
目前，多数网上考试系统不能根据每位学生的特定学习情况分别抽取适合不同学生的试卷。传统组卷算法组卷成功率较低，时间和空间开销都比较大。随着在线人数的增多，网络流量会急剧增加。为了解决这些问题，本文提出了一种新的个性化网上考试系统体系结构。在此系统中，首先采用移动agent 技术来降低网络流量和减轻服务器负荷并将不同的考试任务合理地分配给了几个相互合作的agent，使整个考试过程能有条不紊地进行。其次
本文针对现有分布式构件技术的不足，提出了一种利用 Web Service 技术对 Internet 上广泛分布的构件资源进行有效组织的模型，并在此模型基础上，进一步给出了一种构件资源的有效组织机制，最后通过原型系统的验证，证明了该模型及资源组织机制的有效性。
目前基于硬件性能监视计数器的程序性能测试与分析正在逐步成为现代性能分析的基础。同时，为方便用户安全地访问这些底层硬件计数器，可供用户程序调用的接口软件包被大量开发出来，其中适用平台最广泛的 PAPI 软件包得到业内人士的一致好评，并已被集成到很多第三方软件中。目前基于 PAPI 的串行程序性能数据的收集和分析已经取得了很多成果，但是将PAPI集成到并行程序软件中对并行程序的性能行为进行测试与分析的
在数字式温度传感器 DS18B20-PAR 组成的单总线多点测温网络中，多个传感器的地址识别是关键。本文分析了传感器光刻 ROM 地址码识别过程存在的不足，提出通过在测温网络中搭建简单硬件地址译码开关电路和在软件中进行位置编码映射来优化识别过程的方法。在小地理范围的测温网络中，这是一种可行的通过硬件补偿降低软件复杂性的方法。
随着信息技术的迅速发展，需要分析和管理的数据量迅速增大，这种趋势必然地渗透到了聚类分析领域。聚类分析是数据挖掘技术中重要的组成部分，从技术角度讲，它的主要目的是将数据空间中的数据点划分到若干个类中，其中将距离相近的数据点划分到相同的类中，而将距离较远的数据点划分到不同的类中。本文提出一种新颖而高效的聚类算法 SECDU（Self-Expanded Clustering Algorithm base
索引技术是数据库及数据仓库系统中的一项很重要的技术，历来受到学术界的重视。高效的索引机制是保证数据库效率的一个及其重要手段。本文提出了一种基于语义的 Bitmap 索引优化选择算法。该算法通过对 Bitmap 序列做语义分析，根据其数值分布的特点来找到代价最小的索引选择策略。