一种基于模型检验程序分析技术的前端工具研究

来源 :计算机科学 | 被引量 : 0次 | 上传用户:zero_ak47
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
提出了一种用模型检验技术对程序进行分析的方法,其主要思想是将C/C++源代码转换为与控制流图等价的Kripke结构,用CTL公式描述待验证的源程序性质,使用NuSMV模型检验工具实施具体的程序分析。基于这一思想,设计并实现了一个自动将C/C+ }源代码转换为NuSMV输入的工具。所做的实验验证表明,该方法能够有效地对程序进行分析。
其他文献
近年来,随着基础央行信息化进程的不断加快,信息技术在人民银行得到了广泛运用,目前已投入使用80多个业务系统,涉及货币政策、宏观调控、金融稳定、金融服务、办公自动化等各个领
氯气是一种有毒有害气体,在生产和生活中,准确测量空气中的氯气体积分数尤为重要。介绍了一种用半导体型氯气敏感探头和由其组成的变送电路来测量氯气体积分数的新方法。通过运用对数、反对数放大器和同相、反相放大器把类似于双对数关系的体积分数—电阻值输出转换为具有线性关系的体积分数—电压值输出,实现了氯气传感器信号的线性化处理。
一、引言在我国,票据一般指汇票、支票及本票的统称。本文所指的票据是更广义的票据。包括各种有价证券和凭证,如支票、保险单、发票、提货单等金融行业中需要电子化的各种凭证
颈动脉狭窄是导致缺血性脑卒中的重要原因,早发现和早治疗可显著降低其致死率和致残率。磁共振血管成像以无创、无辐射、软组织分辨率高等特点而在颈动脉狭窄评估方面具有重
目的探讨外固定支架联合克氏针固定对桡骨远端骨折患者的临床应用效果。方法回顾性分析2018-06—2019-11间杞县人民医院采用外固定架联合克氏针固定的43例桡骨远端骨折患者的
协作式频谱感知在提高认知无线电网络频谱感知性能的同时,也带来额外的通信开销。针对此问题,提出了一种基于流水线架构的协作式频谱感知方法,并给出了与之相配合的快速数据融合
为了求解数独难题,首先将其转化成一个组合优化问题。然后,提出一个在编码、初始化、交又、变异、局部搜索等方面具有特点的遗传算法来求解它。实验结果表明,对于所有难度等级的
通过将AES算法模块化、运算一般化,给出了类AES算法的统一框架。在此框架下不仅可以同时实现AES的加密、解密,而且可以通过外部参数动态设定分组算法,使得密码算法的使用更加灵
从经济影响角度着手,运用主成分分析、相关性分析、综合评价等方法,分别构建主成分、基于阿尔蒙法的滞后分布、区域经济引力、断裂点范围等模型,研究上海在长三角经济圈的影响力
密码体制的完善保密性是衡量保密系统安全性的重要方法。通过深入分析密码体制的明文空间、密文空间、密钥空间及密钥概率之间的关系,给出并证明了两个特殊密码体制具有完善保