检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

嵌入偏序约简的状态事件线性时序逻辑验证

计算机学报 2019年第10期42卷 2145-2159页

作者：谢健阚双龙黄志球王飞杨志斌李伟湋南京航空航天大学计算机科学与技术学院南京210016 南京航空航天大学航天学院南京210016

模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状... 详细信息

模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状态事件线性时序逻辑(State/Event Linear Temporal Logic,SE-LTL)给出了一种简洁和直接的方式表达包含状态和事件的系统属性.在SE-LTL中,状态和事件都可以作为原子命题.基于自动机理论的线性时序逻辑(Linear Temporal Logic,LTL)模型检验可以被用来对SE-LTL属性进行验证.然而SE-LTL属性在经典的stutter等价(stutter-equivalent)下无法保持,所以最有效的并发程序状态约简技术:偏序约简技术(Partial Order Reduction,POR)不能直接应用于SE-LTL的验证.该文提出一种新的方法利用已有的偏序约简技术对SE-LTL验证过程的状态空间进行约简.该方法分为两个部分:第一个部分是针对SE-LTL不带NEXT算子的约简方法;第二部分则是带NEXT算子的约简方法.第一部分的主要思想是从一个Büchi自动机(Automata,BA)中抽取出“状态部分”.“状态部分”的含义是该部分只与系统的状态相关.基于“状态部分”,给出关于BA和标签Kripke结构(Labeled Kripke Structure)的同步乘,并在同步乘的构造过程中嵌入偏序约简技术,从而约简同步乘的状态空间,即该文的约简技术是on-the-fly的.嵌入的偏序约简在已有的偏序约简基础上,面向SE-LTL公式中的事件引入新的可见操作的识别方法.为了能够将偏序约简技术应用到所有的SE-LTL公式,该文同时给出验证SE-LTL带NEXT算子的偏序约简算法.NEXT算子是偏序约简的另一个主要障碍.该部分是文中的第二部分工作.该部分的技术依然是on-the-fly的,并且需要与状态部分的识别相结合.通过将该文技术实现到SPIN模型检验器中对已有的模型进行验证.Spin是针对LTL的并发程序模型检验器.实现部分包括SE-LTL到BA的转化,以及on-the-fly的模型验证过程.实验的过程主要针对三个模型集:生产消费者模型,哲学家就餐问题以及公共对象请求代理体系结构中的GIOP协议.验证结果表明,对比完全基于状态的模型检验和不带偏序约简的状态事件模型检验,该文的方法具有更好的效率,并且能够被应用于状态事件系统,特别是安全有关嵌入式系统的验证.

关键词：偏序约简状态事件线性时序逻辑模型检验同步乘标签Kripke结构

在线全文

学校读者我要写书评

暂无评论

基于偏序约简程序可达图的并发程序切片方法

计算机学报 2014年第3期37卷 568-579页

作者：戚晓芳徐晓晶江振亮汪鹏东南大学计算机科学与工程学院南京211189 东南大学计算机网络和信息集成教育部重点实验室南京211189 IBM中国系统与科技实验室上海201203

并发程序切片是一种重要的并发程序分析手段.基于程序可达图可构造以程序状态和语句二元组为节点的、依赖关系具有可传递性的并发程序依赖图,解决依赖关系的不可传递性问题,提高切片精度.程序可达图通过交织执行模拟并发活动,分析代价较... 详细信息

并发程序切片是一种重要的并发程序分析手段.基于程序可达图可构造以程序状态和语句二元组为节点的、依赖关系具有可传递性的并发程序依赖图,解决依赖关系的不可传递性问题,提高切片精度.程序可达图通过交织执行模拟并发活动,分析代价较高.偏序约简是一种十分有效的并发系统状态空间约简技术,约简的并发系统状态空间包含所有的并发程序执行代表.为提高效率,该文将偏序约简技术扩展到程序可达图的约简中,在偏序约简理论的基础上,证明了基于未约简和约简的并发程序可达图构造的并发程序依赖图在进行切片计算时是等价的.实验结果表明,采用偏序约简技术使基于程序可达图的并发程序切片方法在保证切片精度不受损失的前提下显著提高切片效率.与其它高精度切片方法相比,基于约简程序可达图的切片方法的精度更高,在大多数情况下,切片效率也有一定提高.

关键词：并发程序程序切片依赖性分析可达性分析偏序约简程序分析软件测试中图法

在线全文

学校读者我要写书评

暂无评论

基于偏序约简的智能电网大数据处理

农村电气化 2017年第9期 36-37页

作者：王庆斌柳军停石亮缘广东电网有限责任公司云浮供电局广东云浮527300

以电力系统数据的多维度以及空间混乱等特征为基础,创建了一类基于偏序约简的大数据属性约简预处理方法。此种方法主要应用了MapReduce的可并行化特征,结合并发事件之间的独立性,能够适应电力大数据的发展需求与约简要求。研究过程中以... 详细信息

以电力系统数据的多维度以及空间混乱等特征为基础,创建了一类基于偏序约简的大数据属性约简预处理方法。此种方法主要应用了MapReduce的可并行化特征,结合并发事件之间的独立性,能够适应电力大数据的发展需求与约简要求。研究过程中以某某区域电力系统的变压器故障诊断数据等为例,在Hadoop的作用下实行模拟与仿真,结果表明偏序方法可适合应用于大数据的约简运算中,时间性能较佳,操作便利。

关键词：智能电网大数据偏序约简数据预处理

在线全文

学校读者我要写书评

暂无评论

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

软件学报 2023年第7期34卷 3064-3079页

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

模型检测是一种基于状态空间搜索的自动化验证方法,可以有效地提升程序的质量.然而,由于并发程序中线程调度的不确定性以及数据同步的复杂性,对该类程序验证时存在更为严重的状态空间爆炸问题.目前,大多采用基于独立性分析的偏序约简技... 详细信息

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

关键词：约束依赖图偏序约简并发程序模型检测工具

在线全文

学校读者我要写书评

暂无评论

电力系统大数据属性约简研究

电力系统大数据属性约简研究

作者：焦谱华北电力大学

学位级别：硕士

伴随着工业及社会信息化程度的增强,各个领域的自动化程度越来越高,大规模及超大规模海量数据应运而生,呈现出大数据特征。这些海量数据在提升行业发展动力的同时,也带来了巨大的挑战性问题—数据可用性。为了从海量数据中甄别无用信息... 详细信息

伴随着工业及社会信息化程度的增强,各个领域的自动化程度越来越高,大规模及超大规模海量数据应运而生,呈现出大数据特征。这些海量数据在提升行业发展动力的同时,也带来了巨大的挑战性问题—数据可用性。为了从海量数据中甄别无用信息、挖掘出有益于相关领域发展的有价值信息,就需要对其进行数据分析。数据预处理技术可以极大地减少分析数据时的数据处理量,提高数据分析处理的效率,而属性约简在数据预处理中是一个比较重要的环节。又因为电力系统的运行与监测环节所产生的数据类型多、数量大,呈现出大数据的特征,故需要对这类数据进行有效地属性约简才能适当使用。现有的基于现代启发式优化技术如遗传算法的约简方法存在覆盖面较窄、算法复杂度高等缺点,无法有效应用于电力大数据处理领域。本文分析非并行化属性约简算法、并行化属性约简算法的国内外研究现状,首先对现有的并行化属性约简算法进行了性能分析,其存在算法复杂度偏高,约简信息易丢失等问题,而传统的非并行化属性约简算法又同时存在内存瓶颈难题,无法约简海量数据。然后结合电力系统大数据的特征,着眼于并发事件间的独立性,综合利用MapReduce的可并行化优点及偏序算法的可并行性,给出了电力大数据偏序约简的形式化描述。最后给出了电力系统属性偏序约简的算法设计,并根据电力数据集中决策属性不同取值个数多少的实际情况分别给出了两种约简方案,方案1,如果决策属性的取值种类较多,则可以选择算法1和算法2;方案2,如果决策属性的取值种类较少,则可以选择算法1和算法3;但是,为了提高数据预处理的效率,在决策属性值种类较多的情况下,也可以选择算法1和算法3。本文分别以某光伏发电系统监测数据、变压器故障诊断数据和智能变电站通信系统实时性与可靠性预测数据为例,对属性约简进行模拟计算,并通过Hadoop平台进行测试,表明所提出的电力大数据属性约简方法性能优良。验证了本文提出的偏序约简算法不但解决了启发式属性约简算法所引起的决策表信息丢失问题,还略过了启发式属性约简算法的求核过程,具有性能上的优越性。

关键词：电力系统智能电网大数据 MapReduce 偏序约简