检索结果-南通市图书馆

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

反例引导的抽象精化优化技术研究

反例引导的抽象精化优化技术研究

作者：刘林武南京航空航天大学

学位级别：硕士

模型检测最主要的瓶颈是状态空间的爆炸,这就导致早期的模型检测主要用于小型系统的验证。为解决这个问题,偏序约简、有序二叉决策图、抽象等方法被提出。在上述方法中,抽象技术是重要的方法之一。抽象技术是对大型软件系统进行验证的... 详细信息

模型检测最主要的瓶颈是状态空间的爆炸,这就导致早期的模型检测主要用于小型系统的验证。为解决这个问题,偏序约简、有序二叉决策图、抽象等方法被提出。在上述方法中,抽象技术是重要的方法之一。抽象技术是对大型软件系统进行验证的一种有效方法,但其中一个重大的障碍就是对系统的抽象会引入具体系统中本不存在的行为,即可能会引入虚假反例。因此,需要根据反例对抽象模型进行精化,本文的主要研究内容如下:(1)采用动态的抽象精化过程,通过对抽象模型进行精化来消除虚假反例。传统的反例引导的抽象精化方法通过改变可见变量集来分割失效状态,造成其它非失效状态也受影响。本文给出了一种新的划分失效状态的方法:增加布尔变量法。该办法的优点是在抽象精化时,只对失效状态进行重新分割,其他非失效状态不受影响。本文还给出一种新的寻找失效状态的方法,该方法只根据抽象状态的前驱和后继状态来判定其是否为失效状态。对于含有无穷循环的反例,此方法可以避免循环展开时的多项式时间问题。同时,给出并行计算失效状态的方法,快速定位失效状态。最后,综合以上方法,给出了一个反例引导的抽象精化框架。(2)采用静态的抽象精化过程,不对抽象模型进行精化,而是借用一系列精细程度不同的抽象模型和启发式算法来消除虚假反例。本章给出一种静态抽象精化方法,直接对反例进行精化,以判定其是否为虚假反例。该方法将一系列抽象模型作为输入,采用启发式算法,来验证系统的安全属性。从原始模型中提取启发式信息,使用启发式搜索算法,模型检测器可以避免搜索整个状态空间,大大减少空间和时间开销。(3)给出了一种基于权重大小来选择虚假反例的方法。传统的反例引导的抽象精化方法没有考虑到反例的权重。不同的反例路径对抽象精化的影响不同,如果一个反例路径中含有高权重抽象状态,那么该反例的重要性超过其他反例。本文基于此,给出了关键反例的概念,然后借鉴图论中对节点权重的计算方法并将其与抽象技术相结合,重新分析并给出了关键反例识别算法,提高了寻找反例和反例精化的效率。论文从三个方面对反例引导的抽象精化进行优化。第一方面采用动态的精化方法,通过对抽象模型精化来消除虚假反例。第二方面,采用静态的精化方法,不对抽象模型进行精化,而是通过预构建的一系列抽象模型来消除虚假反例。第三方面着眼于寻找权重更大的反例,以提高模型检测效率。第一、二方面讲的是如何从动态静态两种角度来消除虚假反例。第三方面讲的是如何高效地选择虚假反例。

关键词：抽象精化模型检测虚假反例关键路径失效状态

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于内核调试与抽象精化的操作系统实验设计

计算机教育 2019年第8期 14-17页

作者：文艳军罗宇李姗姗刘江潮国防科技大学计算机学院

针对如何分解操作系统内核实验难度的问题,提出一种基于内核调试和抽象精化思想的实验设计方法,该方法聚焦几条内核执行路径,通过调试观察该路径在不同抽象程度的表现,从高层抽象开始,逐步加入更多的观察细节,直至完整的复杂底层状态,... 详细信息

针对如何分解操作系统内核实验难度的问题,提出一种基于内核调试和抽象精化思想的实验设计方法,该方法聚焦几条内核执行路径,通过调试观察该路径在不同抽象程度的表现,从高层抽象开始,逐步加入更多的观察细节,直至完整的复杂底层状态,最后在分析和理解的基础上对内核进行改写。

关键词：操作系统内核调试内核执行路径抽象精化

基于谓词抽象与精化技术的Web服务验证研究

在线全文

学校读者我要写书评

暂无评论

基于谓词抽象与精化技术的Web服务验证研究

作者：任强苏州大学

学位级别：硕士

面向服务体系结构（SOA）是继面向对象、基于构件开发之后的一种新型软件开发、部署和集成模式,为软件开发提供了灵活的设计和开发方案。Web服务作为SOA的一种实现方法,突破了传统的分布式计算模型在通信、应用范围等方面的限制,通过服... 详细信息

面向服务体系结构（SOA）是继面向对象、基于构件开发之后的一种新型软件开发、部署和集成模式,为软件开发提供了灵活的设计和开发方案。Web服务作为SOA的一种实现方法,突破了传统的分布式计算模型在通信、应用范围等方面的限制,通过服务组合的方式,灵活、快速构建的网络应用已经渗透到国民经济的许多关键行业。在现有的Web服务验证方法中,模型检测因其自动化程度高、能够提供反例路径等优势,得到了广泛应用。但在模型检测过程中,会因系统规模庞大而导致状态爆炸问题,如何选取合适的方法缓解状态爆炸已成为服务验证领域的一个研究热点。本文在传统的模型检测方法中引入谓词抽象和精化技术,提出一种用于Web服务验证的抽象精化验证框架,用以验证Web服务内部流程逻辑的安全性和组合服务间的兼容性。主要工作如下:（1）使用Kripke结构对Web服务建模,通过分解待验证性质得到原子命题从而获取谓词公式集合,使用谓词抽象技术建立Web服务的抽象模型,再将各抽象模型组合得到待验证系统的组合抽象模型。（2）给出抽象模型到Promela语言的转换规则,使用模型检测工具Spin验证模型是否满足待验证性质,如果不满足,则给出反例。将得到的反例在Web服务上做投影操作,进行反例确认,对产生伪反例的Web服务抽象模型进行精化,生成新的组合抽象模型,再次对性质进行验证。（3）基于上述两方面工作,提出Web服务抽象精化验证框架,并通过实例说明其在缓解状态爆炸方面的可行性。

关键词： Web服务谓词抽象模型检测 Spin 抽象精化

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于CEGAR的Web应用验证

计算机学报 2014年第4期37卷 976-992页

作者：高洪皓缪淮扣曾红卫上海大学计算机工程与科学学院上海 200444 上海大学计算中心上海 200444 上海市计算机软件评测重点实验室上海 201114

Web应用导航行为的建模和验证是可信Web工程研究的重点和难点.在深入分析用户和Web浏览器交互行为的基础上,文中引入On-the-fly策略并基于反例引导的抽象精化验证方法 CEGAR对Web应用的导航行为进行建模和验证.在On-the-fly导航模型展... 详细信息

Web应用导航行为的建模和验证是可信Web工程研究的重点和难点.在深入分析用户和Web浏览器交互行为的基础上,文中引入On-the-fly策略并基于反例引导的抽象精化验证方法 CEGAR对Web应用的导航行为进行建模和验证.在On-the-fly导航模型展开的过程中,根据检验性质采用增量式状态抽象方法构造Web应用导航抽象模型,通过确认抽象反例来识别伪反例,借助等价类精化方法消除抽象模型上的伪反例.这一方法可有效地缓解Web应用验证过程中出现的状态爆炸问题.

关键词： Web应用导航模型抽象精化模型检验伪反例

变量极小不可满足在模型检测中的应用(英文)

在线全文

学校读者我要写书评

暂无评论

软件学报 2008年第1期19卷 39-47页

作者：陈振宇陶志红 KLEINE BURNING Hans 王立福东南大学计算机科学与工程学院江苏南京210096 北京大学软件与微电子学院北京100871 Department of Computer Science University of Paderborn Paderborn 33095 Germany

提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动... 详细信息

提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然VMU的判定问题和极小不可满足(MU)一样难,即DP完全的,该案例研究表明,在变量抽象精化过程中,VMU比MU更为有效.

关键词：极小不可满足抽象精化模型检测

在线全文

学校读者我要写书评

暂无评论

基于CEGAR的C程序空指针解引用检测

计算机研究与发展 2016年第1期53卷 155-164页

作者：段钊田聪段振华西安电子科技大学计算机理论与技术研究所西安710071

随着计算机软件规模和复杂度的日益增长,软件系统的可靠性和安全性倍受关注.空指针解引用是程序中常见的一类错误.提出了一种基于反例制导抽象精化CEGAR的C程序空指针解引用检测方法.该方法首先使用线性时序逻辑描述空指针解引用问题,... 详细信息

随着计算机软件规模和复杂度的日益增长,软件系统的可靠性和安全性倍受关注.空指针解引用是程序中常见的一类错误.提出了一种基于反例制导抽象精化CEGAR的C程序空指针解引用检测方法.该方法首先使用线性时序逻辑描述空指针解引用问题,然后通过抽象精化的方法检测待测程序中是否含有空指针解引用错误.为了达到完全自动验证的目标,同时针对空指针解引用问题,研究了该类性质的时序逻辑表达方法,并自动从程序中针对所有的指针变量,形成相应的时序逻辑公式.实验结果表明,所提出的方法在大规模C程序的空指针解引用检测方面有着重要的实际应用价值.

关键词：模型检测抽象精化空指针解引用’ 程序验证时序逻辑

在线全文

学校读者我要写书评

暂无评论

采用CPAChecker的动态程序验证

西安电子科技大学学报 2019年第1期46卷 33-38页

作者：段钊刘锟龙西安电子科技大学计算机学院陕西西安710071 合肥工业大学电气与自动化工程学院安徽合肥230009

针对模型检测中状态空间爆炸问题,在CPAChecker的抽象谓词检测方法的基础上,提出了一种基于动态执行的检测方法.首先,根据程序的控制流程图,对程序进行静态检测。在静态检测的过程中,根据分支语句的确定性,利用动态执行的方法来加快检... 详细信息

针对模型检测中状态空间爆炸问题,在CPAChecker的抽象谓词检测方法的基础上,提出了一种基于动态执行的检测方法.首先,根据程序的控制流程图,对程序进行静态检测。在静态检测的过程中,根据分支语句的确定性,利用动态执行的方法来加快检测的过程。其中,抽象检测可以有效地限制系统模型的规模,动态执行不仅可以有效地减少静态检测导致的误判,而且有助于引导构建精确的系统模型,降低虚假反例的数量和不必要的反例分析和精化。实验数据显示,这种算法明显提高了传统的反例引导谓词抽象精化算法的检测效率和准确率。

关键词：模型检测抽象精化动态执行程序验证状态空间爆炸

在线全文

学校读者我要写书评

暂无评论

模型检验中抽象技术研究综述

计算机工程与应用 2006年第33期42卷 15-19页

作者：屈婉霞李暾郭阳杨晓东国防科学技术大学计算机学院长沙410073

在模型检验中,抽象技术是解决状态空间爆炸问题的有效方法之一。论文描述了模型检验对抽象模型的基本要求,给出了抽象模型的定义及其评价指标,对抽象技术和自动化的抽象精化技术的主要方法及其研究进展作了比较深入、全面的综述,并讨论... 详细信息

在模型检验中,抽象技术是解决状态空间爆炸问题的有效方法之一。论文描述了模型检验对抽象模型的基本要求,给出了抽象模型的定义及其评价指标,对抽象技术和自动化的抽象精化技术的主要方法及其研究进展作了比较深入、全面的综述,并讨论了抽象技术今后的发展方向。

关键词：模型检验谓词抽象抽象精化反例插值

在线全文

学校读者我要写书评

暂无评论

代码/需求行为差异检测

计算机应用研究 2016年第7期33卷 2056-2062页

作者：刘智萍黄箐江西科技学院信息工程学院南昌330098 武汉大学计算机学院武汉430072

为解决软件开发后期(维护/演化)程序代码与需求模型不一致的问题,面向逆向需求工程,重点研究检测变更代码与原始需求模型之间行为差异的算法:首先沿用模型/代码转换技术,分析模型/代码比较原理,设计比早期连续型单向串行检测算法快2N(N... 详细信息

为解决软件开发后期(维护/演化)程序代码与需求模型不一致的问题,面向逆向需求工程,重点研究检测变更代码与原始需求模型之间行为差异的算法:首先沿用模型/代码转换技术,分析模型/代码比较原理,设计比早期连续型单向串行检测算法快2N(N为路径数)倍的离散型双向并行检测算法;然后采用该算法开发图形化需求/代码比较工具RCCT,并将其集成进综合需求建模系统(RMTS),使动画建模、特性检测、模型转换、需求/代码差异检测等功能融为一体;最后通过电子转账案例演示该工具的使用方法,并编写测试程序证明离散型双向并行算法不但比原始算法高效,而且更加可靠。

关键词：逆向需求工程需求代码比较行为一致抽象精化双向并行