检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

反例引导的C代码空间流模型检测方法

软件学报 2022年第6期33卷 1961-1977页

作者：于银菠刘家佳慕德俊西北工业大学网络空间安全学院陕西西安710072

软件验证一直是确保软件正确性和安全性的热点研究问题.然而,由于程序语言复杂的语法语义特性,应用形式化方法验证程序的正确性存在准确度低和效率差的问题.其中,由指针操作带来的地址空间的状态变化使得现有模型检测方法的检测准确度... 详细信息

软件验证一直是确保软件正确性和安全性的热点研究问题.然而,由于程序语言复杂的语法语义特性,应用形式化方法验证程序的正确性存在准确度低和效率差的问题.其中,由指针操作带来的地址空间的状态变化使得现有模型检测方法的检测准确度难以得到保证.为此,通过结合模型检测与稀疏值流分析方法,设计了一种空间流模型,实现了对C程序在符号变量层面和地址空间层面的状态行为的有效描述,并提出了一种反例引导的抽象细化和稀疏值流强更新算法(CEGAS),实现了C程序指向信息敏感的形式化验证.建立了包含多种指针操作的C代码基准库,并基于该基准库进行了对比实验.实验结果表明:所提出的模型检测算法CEGAS在分析含有多种C代码特性的任务中,与现有模型检测工具相比均能取得突出的结果,其检测准确度为92.9%,每行代码的平均检测时间为2.58 ms,优于现有检测工具.

关键词：软件验证模型检测稀疏值流分析指针分析漏洞检测

在线全文

学校读者我要写书评

暂无评论

模型检测中关键反例的提取算法

哈尔滨工程大学学报 2015年第10期36卷 1404-1408页

作者：郎大鹏黄少滨程媛迟荣华哈尔滨工程大学计算机科学与技术学院黑龙江哈尔滨150001

针对模型检测过程中产生的反例过于复杂和冗长的问题,提出一种基于时态逻辑ACTL*的模型检测关键反例的提取算法。基于存在性抽象框架提出了关键反例的概念,通过采用图论中对节点权重的计算方法,结合抽象技术,重新分析和设计了反例识别... 详细信息

针对模型检测过程中产生的反例过于复杂和冗长的问题,提出一种基于时态逻辑ACTL*的模型检测关键反例的提取算法。基于存在性抽象框架提出了关键反例的概念,通过采用图论中对节点权重的计算方法,结合抽象技术,重新分析和设计了反例识别算法。基于关键反例的识别和抽象,算法大大缩减了反例空间,能够更准确迅速地定位错误。实验显示,在不提高算法复杂性的前提下,通过分析和计算模型中节点权重,构造带有权重的Kripke结构,能够更高效地引导反例精化过程,反例识别效率提升15%,同时为设计开发人员提供关于系统失效的更丰富的关键因素信息。

关键词：关键反例抽象模型检测精化

在线全文

学校读者我要写书评

暂无评论

模型检测中的CTL形式化描述模板

哈尔滨工程大学学报 2013年第4期34卷 483-487页

作者：陈志远黄少滨白玉纪明宇哈尔滨工程大学计算机科学与技术学院黑龙江哈尔滨150001

针对SPS(specification pattern system)和Prospec(property specification)不能将组合命题形式化为模型检测器可以接受的CTL(computation tree logic)公式问题,通过研究SPS和Prospec产生系统性质描述的形式化方法,并对比CTL与FIL(future interval logic)的表达能力以及CTL与LTL(linear temporal logic)两者之间的关系,构造了一类具有较强描述能力的CTL公式模板,并通过重新定义合取逻辑运算符来简化公式.该类模板简洁且易于理解.模板类的正确性证明表示该类模板可以有效地描述系统性质.利用该模板得到的CTL公式可以直接应用到模型检测器中,利于系统性质验证.

关键词：模型检测形式化描述 SPS Prospec CTL 模板

在线全文

学校读者我要写书评

暂无评论

用于验证多智能体系统的APTL模型检测器

软件学报 2019年第2期30卷 231-243页

作者：王海洋段振华田聪西安电子科技大学计算理论与技术研究所陕西西安710071 综合业务网理论及关键技术国家重点实验室(西安电子科技大学) 陕西西安710071

由于经典的线性时序逻辑表达能力有限,设计并开发了基于交替投影时序逻辑(alternating projection temporal logic,简称APTL)的模型检测工具.根据王海洋等人提出的APTL符号模型检测方法,设计并实现了APTL模型检测器MCMAS_APTL.该工具可... 详细信息

由于经典的线性时序逻辑表达能力有限,设计并开发了基于交替投影时序逻辑(alternating projection temporal logic,简称APTL)的模型检测工具.根据王海洋等人提出的APTL符号模型检测方法,设计并实现了APTL模型检测器MCMAS_APTL.该工具可用于多智能体系统(multi-agent system,简称MAS)的性质验证.MCMAS_APTL检查MAS是否满足具体性质的过程如下:首先,用解释系统编程语言(interpreted system programming language,简称ISPL)描述要验证的系统IS,用APTL公式P描述要验证的性质;然后,符号化表示系统IS,并将非P转化为范式;最后,计算所有满足非P的路径的起始状态集合.如果得到的状态集合中包含系统的初始状态,则说明系统不满足公式P;反之,则说明系统满足公式P.详细阐述了实现MCMAS_APTL的过程,并且通过验证机器人足球赛的例子展示了MCMAS_APTL的性能.

关键词：交替投影时序逻辑多智能体系统模型检测

在线全文

学校读者我要写书评

暂无评论

一种命题投影时序逻辑的分布式模型检测方法

西安电子科技大学学报 2020年第4期47卷 39-47页

作者：舒新峰王昌太王燕张丽丽西安邮电大学计算机学院陕西西安710121

为缓解模型检测的状态空间爆炸问题,提出一种基于命题投影时序逻辑的分布式模型检测方法。通过标记范式图技术将命题投影时序逻辑公式描述的待验证性质转换为自动机;根据强连通分量将其状态空间划分为多个子自动机,将各个子自动机与层... 详细信息

为缓解模型检测的状态空间爆炸问题,提出一种基于命题投影时序逻辑的分布式模型检测方法。通过标记范式图技术将命题投影时序逻辑公式描述的待验证性质转换为自动机;根据强连通分量将其状态空间划分为多个子自动机,将各个子自动机与层次语法图描述的待验证系统模型分发至验证服务器集群中,使用动态验证技术进行多机协同完成系统模型检测验证。实验结果表明,该方法和单机模型检测相比验证时间明显降低,且能够验证更复杂的系统。

关键词：命题投影时序逻辑模型检测形式化验证标记范式图分布式计算

使用模型检测方法对Paxos算法进行验证与改进

在线全文

学校读者我要写书评

暂无评论

小型微型计算机系统 2022年第5期43卷 1109-1113页

作者：何东炼杨晋吉赵淦森管金平华南师范大学计算机学院广州510631

因通信的同步问题、网络分区的可靠性问题等,分布式系统难以在通信、分区等环节失效的情况下对特定的状态达成共识.Paxos是近年分布式系统中常见且有效的共识算法,本文通过使用模型检测的方法对Paxos算法进行形式化建模,分析和验证了Pa... 详细信息

因通信的同步问题、网络分区的可靠性问题等,分布式系统难以在通信、分区等环节失效的情况下对特定的状态达成共识.Paxos是近年分布式系统中常见且有效的共识算法,本文通过使用模型检测的方法对Paxos算法进行形式化建模,分析和验证了Paxos作为共识算法所应当满足的性质,结果表明,Paxos算法满足安全性、活性,但执行过程中有发生活锁的可能,并通过模型检测器重现了算法发生活锁时的运行轨迹.最后通过对算法进行改进,以应对现有算法执行过程中可能出现的活锁问题,并通过了模型检测器的验证.

关键词：形式化验证模型检测 Paxos SPIN

基于广义可能性决策过程的可达性问题的模型检测

在线全文

学校读者我要写书评

暂无评论

模糊系统与数学 2022年第5期36卷 95-104页

作者：王军梅李永明陕西师范大学计算机科学学院陕西西安710062

在广义可能性测度下,用广义可能性决策过程(GPDP)建模系统,基于策略的广义可能性线性时序性质的模型检测问题,包括可达性、总是可达性、重复可达性被讨论。本文所获得的结果扩大了经典模型检测的应用范围。

关键词：广义可能性决策过程模型检测策略可达性

在线全文

学校读者我要写书评

暂无评论

基于DNA计算的线性时序逻辑模型检测方法

计算机学报 2016年第12期39卷 2578-2597页

作者：朱维军周清雷张钦宪郑州大学信息工程学院郑州450001 郑州大学基础医学院郑州450001

该文研究基于脱氧核糖核酸(Deoxyribonucleic Acid,DNA)计算的线性时序逻辑(Linear Temporal Logic,LTL)模型检测问题.为此,该文给出了使用粘贴自动机实现LTL模型检测的方法.首先,使用3′-5′型单链DNA分子对LTL公式的有穷状态自动机(Fi... 详细信息

该文研究基于脱氧核糖核酸(Deoxyribonucleic Acid,DNA)计算的线性时序逻辑(Linear Temporal Logic,LTL)模型检测问题.为此,该文给出了使用粘贴自动机实现LTL模型检测的方法.首先,使用3′-5′型单链DNA分子对LTL公式的有穷状态自动机(Finite State Automata,FSA)模型进行编码,从而获得实现公式的粘贴自动机;其次,使用5′-3′型单链DNA分子对系统模型进行编码,从而获得粘贴自动机的输入字符串;最后,对表征粘贴自动机的DNA单链分子和表征输入字符串的DNA单链分子实施一系列生化反应,即可判定系统是否满足公式.分子生物学仿真实验结果表明:给出的DNA编码序列能达到99.9%的碱基配对正确率,且新方法成功地对所有4种LTL基本公式与5种LTL常见公式实施了检测;与之对照,已有的方法只能有效检测1种LTL基本公式与0种LTL常见公式.在此基础上,对本实验给出的DNA编码方案直接作位数扩展即可拥有对任意给定LTL一般公式的(理论)检测能力.

关键词：模型检测脱氧核糖核酸线性时序逻辑粘贴自动机有穷状态自动机 DNA计算

基于启发式on-the-fly的扩展TGBA模型检测算法

在线全文

学校读者我要写书评

暂无评论

计算机学报 2014年第12期37卷 2519-2529页

作者：王曦徐中伟同济大学电子与信息工程学院上海201804 江西理工大学信息工程学院江西赣州341000

以广义Büchi自动机为研究对象,对其作判空检测能为解决系统的状态空间爆炸问题提供有效途径.但广义Büchi自动机难以适用于安全苛求计算机系统中,只需满足某个可接受条件子集便可作出非空性判断,进而能判断出系统的安全性的情形.文中... 详细信息

以广义Büchi自动机为研究对象,对其作判空检测能为解决系统的状态空间爆炸问题提供有效途径.但广义Büchi自动机难以适用于安全苛求计算机系统中,只需满足某个可接受条件子集便可作出非空性判断,进而能判断出系统的安全性的情形.文中提出了基于启发式on-the-fly的扩展TGBA模型检测算法,该算法采用ETGBA模型,通过启发式on-the-fly判空检测方法对ETGBA作判空检测时,加强了对不能构成其可接受运行的结点的处理,节省了内存空间,提高了检测效率,从而能较快地作出非空性判断.通过算法的正确性证明及复杂度分析、实验比较与实例研究验证了所提出算法的正确性与实际可行性.与已有算法相比,该算法的通用性更强,当应用于广义Büchi自动机的判空检测时,其时空性能均优于已有算法.

关键词：模型检测广义Btichi自动机 on-the-fly算法安全性分析