程序断言动态检测工具的设计与实现*

重点研究了断言的动态检测方法与检测过程,并在关系数据库理论的基础上实现了交互式的断言动态检测工具,即TDDPA。该工具具有动态检测程序断言等功能,并通过将运行轨迹收集到数据库中来实现检测到的各种断言形式分析,说明了TDDPA总体设计结构及实现过程。结果证明TDDPA能更方便有效地发现程序中所蕴涵的断言。     

Floyd不变式断言法在程序设计教学中的应用

《程序设计》是计算机专业学生的必修课程,教师非常重视对学生程序设计能力的培养.然而现有的程序设计教材未阐明程序和给定问题之间的关系,导致学生无法理解程序设计的本质.文章提出采用Floyd不变式断言法分析程序,并通过两个实例进行说明.教学实践证明,采用这种方法有助于学生理解程序.     

基于Kripke结构的程序正确性证明

为了方便证明程序的正确性,引入了Kripke结构,提出基于Kripke结构的程序正确性证明。重新定义了适合证明的Kripke结构,并描述了将程序流程图转换为Kripke结构状态图的方法。给出了证明程序正确性的相关定理和基于Kripke结构的程序正确性证明方法。证明方法为:首先,把程序流程图转换为状态图;然后,根据状态之间的转移关系列出每个状态下的状态谓词;最后,证明每个状态谓词为真。根据状态谓词进行证明,能够反映出程序执行的状态。用该方法对一个实例进行了完整的证明。     

基于语法树和程序正确性验证研究

提出了一种新的基于语法树的程序正确性验证方法(TM方法)在理论和算法上对方法的实现进行了初步探讨,并结合XML技术提出了一套实现这一方法的切实可行的解决方案.     

基于安全断言标记语言实现单点登陆

单点登录(single sign-on,SSO)作为一种为解决传统认证机制所存在的问题而提出的技术,已成为分布式系统研究的热点之一.对当前流行的安全断言标记语言(SAML)提供的两种单点登陆模型Artifact和Post进行介绍分析,指出它们存在的不足.针对其局限性,引入了凭证和准凭证的概念,提出了一种改进的基于SAML的单点登陆模型并以实现.最后对该模型的性能进行了分析.     

一种基于程序正确性证明理论的程序开发方法

程序的形式推导方法是一种基于程序正确性证明理论的程序开发方法,它使得程序的开发和证明同时进行,程序开发完成的同时其正确性亦得以保 证,以两个问题的程序开发为例说明了程序的形式推导方法的使用。     

基于WSE安全断言实现Web服务身份验证

随着Web服务在分布式系统中的广泛应用,安全问题日益突出.文章描述了使用UsernameForCertificateAssertion安全断言对Web服务进行身份验证的实现方法,并给出了一个利用WSE实现Web服务身份验证的说明性实例.     

基于简化Trace的动态隐式断言执行

分支指令与分支预测失败限制了处理器发掘指令级并行(ILP)的潜力.通过If-conversion或Predicated执行将程序中的控制相关转化为数据相关,能较好地降低分支预测开销.提出一种基于简化Trace结构的动态隐式断言执行机制(Dynamic Implicit Predication,DIP),而早期的相关研究主要集中于由编译器显式为宽发射处理器产生静态Predicated指令.无需编译器或者其他二进制工具的帮助,DIP可以在程序运行过程中识别可以进行断言变换的指令片断,完成指令转换与优化,并在以后的执行中使用优化后的指令Trace.基于SPEC2000模拟测试表明DIP可以有效避免错误的分支预测,提高并行度,单个程序的IPC平均提高10.3%,基准程序的平均加速比可达7.59%.     

基于断言的形式验证方法研究与应用

随着设计规模的不断扩大和设计复杂度的不断提高。功能验证已经成为数字系统设计开发过程中的制约瓶颈。目前，利用传统的仿真方法并不能有效解决这一困境，而形式验证则是改善该状况的有效途径。本文针对形式验证中模型检验算法在工程实践中遇到的形式语言局限性和状态空间爆炸危机的问题，提出了基于断言的形式验证解决策略，并以DW8051-timer模块为例，利用该方法对它的RTL级设计进行了实际的功能验证。     

基于契约的程序动态分析技术研究

在当今信息社会中，程序质量是一个具有重要意义的热点问题．基于契约的程序设计是提高程序质量的重要且有效的技术，但是形式化契约的制定是一件十分困难的工作．因此软件质量保证问题一直是令人困扰的难题．本文介绍契约式程序设计的基本概念与方法，并在此基础上，提出利用契约进行程序动态分析的主要思路及其基本过程并给出简单实例，从一种新的维度来思考保障软件质量的方法。     

基于VHDL语言的IP核验证

探讨了IP核的验证与测试的方法及其和VHDL语言在IC设计中的应用,并给出了其在RISC8框架CPU核中的下载实例。     

基于合约的似然程序不变量动态发现

本文主要讨论基于合约的似然程序不变量的内涵,以及通过程序断言动态生成技术来发现程序不变量的意义。在此主要描述基于合约的似然程序不变量发现的基本理论模型以及该模型与动态不变量检测工具Daikon实体模型的比较,进一步论述程序断言动态生成技术。通过精确的程序断言动态生成,可以分析程序各变量之间的关联属性,以完成不变量的检测。从而有助于设计高质量的程序架构以及规范化的程序代码.     

一个基于Mathematica平台的程序安全性自动验证工具

程序安全性验证是程序验证的重要部分。基于不变式生成,将程序的安全性验证转化为验证不变式集合是否蕴含表示安全性的逻辑公式。针对简化的C程序,结合验证工具Theorema,在Mathematica平台上实现一个对程序安全性进行自动验证的工具。实验结果表明,该验证工具能够自动验证只含数值变量的C程序。     

基于样本程序的自动化测试工具

为提升基于样本程序的行业软件质量,在分析样本程序内容和领域数据的基础上,提出一种自动化测试工具。通过分析样本程序中规范化的骨架注释,利用规则库提取出自动化测试所需的元素定位参数和业务流程标识,并从领域数据中抽取出业务数据。在此基础上,应用代码引擎自动生成测试脚本。实验结果表明,该测试工具可快速测试和修改基于样本程序的行业软件的业务流程,与通用的QTP测试工具相比,其测试效率和脚本正确率较高。     

.NET验证机制在Web表单验证中的应用研究

随着信息技术快速发展信息产品日新月异,计算机应用在各行各业不断深入。随之产生庞大数据的有效性和安全性在网络应用系统中显得非常重要。为了使数据能够被合法访问并且不对数据产生破坏性,必须采取有效的防范措施。该文就是从用户角度去设计和理解用户的使用动机,选择有效的数据验证方式防止数据遭受毁灭性破坏。     

PROPER:一个概率程序终止性与正确性分析工具

概率程序将概率推理模型与图灵完备的编程语言相结合,统一了对计算和不确定性知识的形式化描述,能够有效地处理复杂的关系模型和不确定性问题.提供了一种用于分析仿射概率程序的工具PROPER.一方面,它有助于定性和定量地分析仿射概率程序的终止性,可以验证该概率程序是否以概率1终止,估计期望终止时间的上限,并计算步数N,使得N步后给定程序的终止概率呈指数下降;另一方面,它可以估计一个断言成立的概率区间,这有助于分析变量不确定性对概率程序结果的影响.通过实验表明,PROPER对分析各种仿射概率程序是有效的.     

使用手机一次性密码更安全的验证身份

越来越多的安全事件,大都是由于密码被盗造成,这也阻碍了网络银行和在线交易的发展。因此,不少国家甚至已经立法规定网上银行、金融机构等需向其用户加强网上安全保护,例如提供双因素认证服务等。     

基于约束依赖图的并发程序模型检测工具

模型检测是一种基于状态空间搜索的自动化验证方法,可以有效地提升程序的质量.然而,由于并发程序中线程调度的不确定性以及数据同步的复杂性,对该类程序验证时存在更为严重的状态空间爆炸问题.目前,大多采用基于独立性分析的偏序约简技术缩小并发程序探索空间.针对粗糙的独立性分析会显著增加需探索的等价类路径问题,开发了一款可细化线程迁移依赖性分析的并发程序模型检测工具CDG4CPV.首先,构造了待验证可达性性质对应的规约自动机;随后,根据线程迁移边的类型和共享变量访问信息构建约束依赖图;最后,利用约束依赖图剪裁控制流图在展开过程中的独立可执行分支.在SV-COMP 2022竞赛的并发程序数据集上进行了对比实验,并对工具的效率进行比较分析.实验结果表明,该工具可以有效地提升并发程序模型检测的效率.特别是,与基于BDD的程序分析算法相比,该工具可使探索状态数目平均减少91.38%,使时间和空间开销分别平均降低86.25%和69.80%.     

研究生入学考试信息验证核对系统

为杜绝考试作弊现象并减轻考后统计工作的压力,设计并实现研究生入学考试信息验证核对系统。系统采用二代身份证读卡器,SQL Server数据库,VS集成开发环境进行开发,主要有进场读卡、信息统计、设置等3个功能模块。详细介绍了实时读卡的2种方法：实时监测数据文件和实时监测机具接口的方法,使用了多线程、非托管等技术。系统简单实用,已连续2年应用在研究生入学考试中,有广阔的应用前景和一定的研究价值。