没有合适的资源?快使用搜索试试~ 我知道了~
基于网格的有界模型检验
理论计算机科学电子笔记135(2006)31-46www.elsevier.com/locate/entcs基于网格的有界模型检验苏布拉马尼扬·耶尔德克萨斯大学奥斯汀分校计算机科学系美国贾瓦哈尔·贾因富士通美国实验室公司美国加利福尼亚州森尼韦尔德巴什·萨胡斯坦福大学电气工程系美国E.艾伦·爱默生1德克萨斯大学奥斯汀分校计算机科学系美国摘要在本文中,我们考虑的效果BDD为基础的欠近似的混合方法使用BDD和SAT-BMC错误检测的计算网格上。实验研究了欠近似方法对基于状态空间划分的BMC非传统并行化的影响。这种并行化是通过独立于不同的种子状态执行BMC的多个实例来实现的,这些种子状态是从不同分区中的可达状态中选择的。这些状态分布在状态空间中,并且可能很深。由于所有的处理器都是独立工作的,所以这个方案适合于使用网格状网络进行错误搜索。我们的实验结果表明,改进现有的方法,我们表明,该方法可以有效地利用一个大的网格网络。关键词:BDD,SAT,有界模型检测,并行计算,网格计算1Emerson教授感谢NSF通过拨款CCR-009-8141和CCR-020-5483提供的支持。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2005.10.01732S. Iyer等/理论计算机科学电子笔记135(2006)311介绍形式验证,特别是错误检测,随着设计复杂性的增加而迅速增加核查的主要限制是可用资源的总量、时间以及内存。大多数验证尝试仅使用单个处理器。最近,已经进行了各种尝试来使用并行和分布式方法进行验证。所有这些办法都假定有一个专门的工作站网络来执行核查任务。随着在这里,网格是一个机器网络,这些机器并不专用于特定的计算用途,但可能只在某些时候可用这是一个独特的环境,大规模的并行是可能的,否则闲置的CPU周期,从大量的计算机。这样的处理器甚至可以在地理上不同的位置。网格计算环境中的问题与专用并行计算环境中的问题有很大不同我们考虑两个关键问题。首先,处理器的可用性得不到保证。因此,使用这种框架的任何算法都必须能够承受从某些计算中接收不到结果或仅部分结果其次,由于计算网络不是一直专用于单个任务,因此在网格上调度的任何任务都必须使用非常少的网络带宽。 尽可能地,不同节点上的计算需要彼此独立,只有很少的依赖性。在这种情况下,算法需要仔细设计,以扩展到基于网格的并行网络。我们的工作特别针对如何有效地使用网格进行形式验证的对于不太深的失败属性,Bounded Model Checking(BMC)现在是事实上的标准。为了证明属性正确或发现深层错误,通常选择不同的方法,通常是基于BDD的方法,并且如果可以有效地执行图像计算,则效果良好。由于人们通常不知道一个属性是否是错误的,如果是错误的,它是否是深的,这两个方法都必须在每个属性上运行我们详细介绍了一个实用和高效的基于网格的错误检测方法,旨在自动处理深以及浅的错误。当前的错误检测基于可满足性的有界模型检查(SAT-BMC)能够通过限制探索深度并连续增加此边界来探索更大设计的状态空间[8]。由于在这方面的S. Iyer等/理论计算机科学电子笔记135(2006)3133作为满意度测试的一种艺术,SAT-BMC现在被常规应用于许多工业设计的性能验证过程中的错误检测[9,4,3,1]。基于SAT的BMC方法是用于检测不是很深的错误状态的优选方法然而,当需要分析许多时间框架时,这些技术可能变得相当昂贵。只要图像BDD保持适度小,基于BDD的方法对于那些“深度情况”工作得更好。这些观察结果在最近报道的工业案例研究中得到了验证[1]。因此,这类问题,需要许多步骤的图像分析,以检测错误,但BDD尺寸变大,仍然是一个有吸引力的研究目标。由于在单个CPU上运行的这些技术由于其执行环境的有限计算能力而具有明显的限制,因此研究人员建议采用基于BDD的模型检查以及并行SAT求解器的分布式方法[10,13]。 然而,这些方法仍然是不够的,因为它们本质上是从广度优先搜索的角度分析状态空间。基于BDD的方法还需要以大型BDD的形式在不同处理器之间进行通信,这使得这些方法无法使用大型并行计算环境。我们的方法:Grid-BMC我们定位错误的方法是创建一种方法,该方法可以找到各种可访问的深度可达状态,然后将其用作并行运行许多SAT-BMC实例的种子,以探索与这些种子相邻的状态空间。从这种潜在的深度种子状态开始,多个BMC运行可能能够到达更深的状态,并定位现有方法无法定位的错误分区BDD(POBDD)[21]具有很大的紧凑性潜力,如文献[6,24]中所研究的同时,正如我们后面将要看到的,它们对参数设置的微小变化非常敏感。根据我们的经验观察,我们提出了一种方法,能够系统地检查多个POBDD表示构造和分析独立的不同节点的网格。这导致了状态的多次遍历,通常与标准的BFS探索有很大的不同,并且被发现大大有利于错误检测的过程图1使用两个分区和四个SAT实例形象地展示了这一点。三角形表示使用SAT的搜索,椭圆表示使用BDD的连续图像计算。请注意,从初始状态开始,BMC只能依次进入深度d。相反,在所提出的方法中,BDD到达深度db,并且SAT的许多实例被播种直到那时,这可能对区分深度ds1、ds2. dsn. 因此,委员会认为,34S. Iyer等/理论计算机科学电子笔记135(2006)31POBDDDs2Dsds3BMCds1我ds4DbFig. 1. 从POBDD可达性这可能会导致难以捕获的错误在本文中,我们研究的效果,改变粗糙度的这种下近似用于定位状态使用BDD的可达性。2相关工作这项工作处于两个工作主体的交叉点,即用于智能模拟或有效bug查找的混合技术和最近在并行框架中执行验证的早期工作本文讨论的技术具有使用多个引擎的混合方法的性质因此,他们可以很容易地使用个别技术的改进,如SAT或ATPG引擎[23,20]或BMC配方[8]。因此,与这些技术的详细比较与我们的论文的目标正交,并且没有进一步详细说明。其他混合或并行方法这项工作在两个关键方面不同于其他混合方法。首先,模拟形成了上述许多方法的搜索骨干在硬的、深的错误的情况下,基于模拟的方法可能无法访问搜索空间的感兴趣区域其次,我们的混合方法是以能够生成多个状态遍历的特定目标来制定的,当一起考虑时,可以潜在地覆盖整个状态空间,并且可以独立地并行执行。在[29]中,使用来自目标状态的前像计算来提供用于模拟的放大目标SIVA工具[12]在仿真环境中执行最佳第一搜索,增加了BDD和SAT,当前状态和目标状态之间的汉明距离作为指导成本函数。[19]的方法使用模拟的交错运行,测试生成器,S. Iyer等/理论计算机科学电子笔记135(2006)3135基于BDD的符号仿真和基于SAT的BMC,以最大化一组感兴趣的信号的状态覆盖与上面的“错误搜索”方法相反,另一类技术采用形式引擎的组合,主要用于验证属性(可能是例如,[7,15]使用基于BDD的可达性分析和[16]通过BDD功能分析计算CNF子句来修剪基于SAT的BMC的搜索空间,[22]在结构上将属性检查划分为SAT和BDD解决的部分,[17]使用符号轨迹评估和基于SAT/BDD的模型检查的组合。前面的讨论是在单处理器框架的上下文中进行的典型的混合方法并不自然地适合于并行探索。我们的方法并行执行多个独立的BMC实例,以同时探索状态空间的不同区域这是SAT-BMC的非传统并行化。已经提出了几种其他方法来进行并行验证。Stern和Dill [26]并行化了一个显式的模型检查器。在[27]中,并行化的BDD用于可达性分析。使用并行可达性分析的验证已在[14,18,28]中进行了研究。 我们的工作是不同的其他分布式模型检查方法,面向完整性,而不是错误狩猎。大多数技术,如[18],在很大程度上只是平行化广度优先遍历。因此,它们在达到深层状态方面的局限性仍然是一个严重的障碍。此外,这些技术需要在不同的处理器之间以大型BDD的形式传递消息这会严重限制有效使用的网格大小一种方法,[13]将基于SAT的BMC分布在异构工作站的网络上。他们的算法执行分布式BCP来解决大型SAT问题。类似地,在[10]中讨论了并行多线程SAT求解器3栅格框架我们使用日本富士通实验室有限公司开发的网格中间件CyberGrip [2]来管理网格上的计算资源图2显示了CyberGrip的整体架构。CyberGrip在中央UNIX或Linux服务器上运行,由三个组件组成:有机作业控制器(OJC),网格资源管理器(GRM)和站点资源管理器(SRM)。在网格上执行作业时,CyberGrip的各个组件之间的交互如图3所示。如图4所示,OJC控制如何执行用户提交的作业。GRM为从OJC转移的作业确定最佳计算资源。SRM监视计算资源的状态36S. Iyer等/理论计算机科学电子笔记135(2006)31见图4。 有机作业控制器(OJC)并管理它们之间的通信每个计算资源都有一个SRM每个计算资源都必须有中间件来与其SRM通信并执行作业。当计算资源是Solaris或Linux机器时,可以使用通用批处理系统(如Condor)作为中间件。CyberGrip可以实现用户可以提交作业的环境图二. CyberGrip的架构图三. 在网格S. Iyer等/理论计算机科学电子笔记135(2006)3137虚拟化计算资源不仅包括Solaris和Linux计算机,还包括Windows计算机,以通过中央服务器的Web门户在线使用。用户可以这样做,而不需要知道各个计算机的性能和其他特性。OJC还具有图5所示的动态作业控制功能。此函数图五.动态作业控制当在初始作业进入时不能静态地决定要执行的作业数量并且要执行的作业数量动态地变化时传统上,由于难以自动执行动态作业控制,操作员通常采取两种方法之一:1.执行所有已提交的作业,而不考虑需要执行哪些作业,或者2.基于先前执行的作业的执行结果来单独地决定是否执行每个作业。这两种方法都是非常不明智的。因此,通过自动化这些决策,OJC显著提高了作业执行的效率。这对于我们使用网格是至关重要的4基于欠近似的Grid-BMC如前所述,我们的论文专门针对必须探索深度状态的问题基于SAT的BMC对它可以探索的状态深度有限制,因为它是基于显式展开多个时间帧的,38S. Iyer等/理论计算机科学电子笔记135(2006)31将编号设置为可疑错误路径的长度BDD针对可达性计算连续图像计算,并且可以深入,只要转移关系的大小是可管理的并且连续图像的大小是小不幸的是,这样的图像通常会在非常小的深度上变大,BDD无法取得进一步的进展。即使BDD在大小上没有表现出戏剧性的爆炸,计算的图像集的大小也会稳定地增长,直到它们如此之大以至于计算需要不切实际的长时间。因此,对于较小的深度,SAT可能能够进一步进行,因为它不存储状态集合,而是仅计算路径。我们在下面提出了一种探索深层状态的方法4.1关键思想:网格BMC在本节中,我们将描述用于执行深度状态空间遍历的欠近似算法欠近似在两个不同的地方执行-查找深层状态:我们通过划分转换关系以及计算的状态集来执行状态空间的遍历,以便BDD和相关计算保持易处理。当BDD的大小不再是可管理的,我们执行连续的下近似。在在图像计算的每一步中,我们使用实际状态集的子集。这种大规模的欠近似可能导致连续遍历,而不是总是导致更深的状态。这种近似的质量可以进一步提高,特别是在设计者的输入下,例如通过使用引导遍历[25,5]。欠近似允许对BDD的大小进行一些控制,否则BDD会表现出戏剧性的爆炸。我们发现,上述简单的方法是相当有效的,并在本文中详细研究并行种子SAT:为了确定SAT的初始种子状态,大量的分区是非常迅速地探索下近似,并产生深状态写在定期的间隔,作为CNF条款。目前,我们在固定数量后创建一个新的种子图像计算,比方说,在每5个图像之后。为了做到这一点,拍摄可达状态的快照,并使用这些状态的子集来播种SAT求解器。选择少量的状态而不是所有的状态是至关重要的,否则SAT求解器会因为得到大量的子句而阻塞SAT求解器实例从由此获得的种子执行类似BMC的算法。通过从状态遍历的各个点开始进行多个BMC运行,我们可以确保至少一个BMC执行子集从深状态开始然后,这些可以探索使用传统SAT-BMC方法无法探索的区域由于所有BMC运行都可以S. Iyer等/理论计算机科学电子笔记135(2006)3139因此这导致了并行化BMC的非传统方法通常,我们执行SAT-BMC到一个小的深度,可以在几分钟内使用zchaSATSAT求解器计算。请注意,必须分别运行这些SAT实例,而不是从它们的联合运行单个SAT实例原因是来自状态空间的不同部分的种子状态可能非常不相似,并且如果它们在生成SAT的子句时被组合在一起,则SAT求解器的效率可能急剧降低近似度:每个分区可以被认为是一个自动在探索国家方面自动选择可达-分区的局部化沿这些方向的广度优先搜索在这种探索中的欠近似是简单地通过从每个图像计算期间发现的新状态集合中挑选几个随机状态来执行的。所产生的BDD的大小通过使用欠近似来减小,尽管以信息丢失为代价。以这种方式保持BDD大小较小允许在选定的“方向”上进行更深入的探索如果任何特定的局部BFS遍历将其引导到与设计中的错误相对应的方向,则从相应的种子开始的BMC可以证明比从原始初始状态开始的经典BMC更有效。请注意,在深入与探索所有方向之间存在权衡4.2网格的逼近和使用在近似程度和所需CPU数量之间存在明显的权衡如果选择许多状态作为种子状态,则其相应地对应于利用BMC在许多方向上同时搜索然而,相应的BMC运行可能会变慢.为了解决这个难题,我们提出了以下方法。网格BMC首先将网格划分为多个子网格。一个子网格使用严重的下近似去很深。其他的运行POBDD和BMC具有不同程度的近似。然后,我们将监视是否出现以下任何一种情况(a) 虽然使用了更复杂的种子,但BMC运行时间不会受到不利影响;(b)虽然使用了不太复杂的种子,但网格中的节点数量很快就会用完。在这种情况下,算法自动切换到使用较大数量的最小项作为主子网格上BMC的种子否则,我们继续使用具有较少最小项的较不复杂的种子为了在近似水平之间切换,取消具有较高近似的运行,并且网格上的相应节点被释放用于使用较低近似的运行(使用更多数量的最小项40S. Iyer等/理论计算机科学电子笔记135(2006)31作为BMC的种子以及POBDD图像计算的边界我们用不同的欠近似在BMC运行中划分网格问题是如何动态地决定哪个子网格表现出次优行为,以便可以取消其给定的运行并释放相应的运行的质量可以通过以下三种消耗的资源来表示。任何一个子网格中的资源的不成比例的大值都应该导致运行被中止,并且子网格中的节点被释放。(a) POBDD时间:如果在一个子网格中,BDD大小(分别为时间)与其他子网格中的BDD大小(时间)相比开始显著增加,则它指示运行受到次优变量顺序或量化时间表的因此,图像计算的每一步的时间都是次优运行的良好过滤器(b) BMC时间/时间帧的比率:有时可以看到,从某些种子开始的BMC运行开始消耗不成比例的大量时间,并且变得不切实际地慢。这通常发生在用作初始种子状态的状态的数量变得非常大时。可以保持平均运行时间/时间帧的比率,并且当在一个网格中显著超过该数字时,则中止子网格上的对应运行。(c) 使用的CPU数量-在极端条件下,这应该用作标记给定子网格上的运行次优的另一种度量。对于更大的欠近似(种子中的状态更少),使用更大数量的CPU会降低其吸引力。这是因为当初始种子状态集较小时,每个BMC运行都从遍历的末端开始,方向非常窄。因此,大量CPU的使用潜在地指示大量不成功的BMC运行,这又意味着起始种子状态不是好的选择,并且可能不在对应于错误的区域中4.3Grid-BMC算法划分网格:创建多个子网格以动态确定良好的近似阈值,以便检测是否存在错误。在每个子栅格上,执行以下操作:(i) 分区到达:在可达性中使用状态分区来获得探索状态空间的不同和发散路径。(ii) 近似分区到达:目标深空穿越-从每个前层,选择新到达状态的欠近似来进行下一个图像计算。(iii) 生成种子:每隔一段时间,只要超过一个阈值,就存储一个种子-一些可达到的状态。S. Iyer等/理论计算机科学电子笔记135(2006)3141(iv)启动种子SAT:从每个种子,将其作为初始状态传递给SAT解算器的新实例。(v) 并行运行:当网格上的节点可用时,以较小的深度运行基于SAT的BMC的所有实例。(vi) 中止子网格:如果该子网格中每个时间帧的BDD图像时间和SAT-BMC时间不成比例地大于其他子网格,则中止在该子网格上运行。终止条件:允许BDD和SAT探索继续在所有子网格上进行,直到发现错误或达到超时5结果我们现在提出的实验结果,证明了我们的方法的有效性。实验在一个计算机网格上运行,其中包括多达100个运行Linux的独立Xeon CPU(范围从1.5GHz到2.3 GHz)。如前所述,我们使用了由日本Fujitsu Labs Limited开发的内部网格中间件(CyberGrip)来提交和控制网格上执行的作业我们的程序是在VIS-2.0上实现的,并使用CUDD BDD包和zcha作为SAT求解器。POBDD算法在单个处理器上运行,但生成的CNF文件被传输到网格上的不同节点,在这些节点上并行执行BMC运行。我们无法准确测量传输文件所需的时间,但根据我们的经验,这是非常小的。基准:我们使用了9个电路和属性,b 1,. b 9,在各种工业电路的验证过程中获得。这些属性中的一些是深层次的,对SAT-BMC以及基于模拟的方法。因此,它们形成了判断我们方法的有效性的良好基准5.1实验详情模拟:首先,我们使用VIS-2.0软件包进行基于随机模拟的实验。 模拟进行了两次,第一次到5,000步,然后到100,000步,但它无法在基准测试中的任何电路中找到错误。然后,我们使用模拟来寻找深层状态并从那里播种BMC这与[19]的方法类似,只是我们使用不同的随机种子每个模拟深度。对于每个电路,我们运行仿真,从2,000到10,000的步长为1,000。当达到深度时,我们选择在模拟结束时达到的状态,并从那里播种SAT。为了限制数据量,在表1中示出了针对深度2k、4k、6k、8k和10k的结果 我们发现模拟,即使它在周期性42S. Iyer等/理论计算机科学电子笔记135(2006)31CktNum.闩锁误差深度模拟接种BMC的运行时间(秒)2k4k6k8k10kSIMBMCSIMBMCSIMBMCSIMBMCSIMBMCB112559222152520748151566663196B27085181172110532964511055118B366232133325195382325025863258B46659272211262747602442562239632060B51703665310479232067160515611822173523332493B620129629487921509125839617563462423313B712360892T/O1305T/O2951T/O2694T/O3515T/OB816923105T/O122T/O193T/O361T/O476T/OB914827106T/O130T/O295T/O256T/O462T/O“T/O” is a timeout of 2表1从模拟到不同深度的BMC播种运行时间CktNum.闩锁误差深度时间(秒)网格#CPU使用BDDPOBDDBMCSIMSIM+BMCGrid-BMC(pickOne)种子坐总B11255973.2T/ONB16771761838B270853.42T/ONB115972612340B366231.91.3T/ONB2681122B466591.91.3T/ONB3097122282408B517036T/OT/OT/ONB27582736639B62012931482857T/ONB1407156201763B712360258976T/ONBT/O3542946414B816923T/OT/OT/ONBT/O1985525328B914827T/OT/OT/ONBT/O2801580186070“T/O”表2各种方法所用时间的比较(以秒为单位)每1000步的深度无法在基准测试中的任何电路中找到任何bug。Grid-BMC:接下来,在表2中,我们比较了以下方法:基于BDD的可达性(VIS-2.0和CUDD); POBDD; BMC(使用SAT求解器zCha);随机模拟到5,000步;模拟到5,000步+SAT求解器的应用。并将该方法与运行Grid-BMC,其具有用于基于POBDD的种子生成的10分钟初始阶段和用于SAT的2小时在Grid BMC的情况下,有许多种子状态,因此该表显示了基于POBDD的可达性发现“最佳”种子状态所需的时间以及SAT求解器从那里找到bug所需的最后一列显示网格中实际使用了多少CPU我们允许每个方法运行,直到超过2小时的时间所有方法的结果见表2。Grid-BMC通过在每个图像和每个种子中仅选择一个状态来使用严重的欠近似请注意,Grid-BMC是唯一能够找到b8和b 9中错误的方法S. Iyer等/理论计算机科学电子笔记135(2006)3143CktpickTwopickThreepickFive种子坐总CPU数量种子坐总CPU数量种子坐总CPU数量B1183954131618555173644730234914B245029479101975224974424624B3134215637298B4185055232123624647211931633515B5252833359241783195268010624B6154241789324193436191242154B7333623956234348953239571681128B8167719427931041973917988B988745833213422345768727021848889表3通过放松近似的严重性来评估性能(以秒为单位的时间)5.2分析我们的研究结果显示了两个关键思想之间积极协同作用的有力证据具体而言,从表2中,我们注意到:• Grid-BMC通常比单独的BDD或POBDD更快地发现错误• Grid-BMC在BMC超时的电路上发现错误• 基于BDD的SAT求解器的播种工作良好,并且通常比使用随机模拟的播种更有效,随机模拟被广泛接受为工业设计的最佳策略之一• 在每一个例子中,Grid-BMC都优于BMC、随机模拟以及两者的结合;无论是在更快地发现错误方面,还是在发现其他方法找不到的错误方面。• 在BDD友好的示例中,Grid-BMC的性能优于其他BMC技术。对于某些电路,例如b1、b2、b3和b4,可以在POBDD阶段本身中检测到错误。在检测到错误时,尚未完成任何已启动的BMC运行。因此,这些条目不需要grid-BMC,但我们显示它,以便我们可以在进一步的表格中分析近似的效果5.3欠逼近效应表3显示了放松近似的效果,通过在每一步选择更多的状态(称之为m)。在我们的实验运行中,我们为每个电路改变m从1到5。表4示出了通过在每一步连续使用10个、20个、然后50个状态来上述结果可以在并行运行两个或多个配置的上下文中查看(从概念上讲,每个配置都可以被视为44S. Iyer等/理论计算机科学电子笔记135(2006)31CktpickTenpickTwentypickFifty种子坐总CPU数量种子坐总CPU数量种子坐总CPU数量B122340662928197567752715554670114B24087248044841031872065945101018B313421453114153B48362370964474535486136617B5256994691911821412718331020B6150231736155271824157442014B74371175482967981094261761222139810B8828416616114381525124301544B9145698843281751213138828112977298834表4通过大幅放松近似的严重性来评估性能(以秒为单位的时间)(say,m= 1和m= 5)。 我们建议自动决定更好的配置。我们的决策方法需要监控每个子网格,相应的BDD图像时间,和每个时间帧的BMC-SAT时间。如果这些运行时变得不成比例地大,那么给定的配置就显示出次优性。注意,由于欠近似被放松,但是每个时间帧的对应BDD图像时间和BMC-SAT时间不成比例地增加,则更准确的近似开始产生更快的错误检测。这在逻辑上是可以预期的,因为当我们放松近似的严重性这种方法的实用性在几乎所有情况下都得到了这里给出的实验结果的例如,条目b9在网格上需要1860秒,m= 1。当m从1逐渐增加到5时,运行时间按比例减少,4. 同样的观察结果也适用于电路b86分析和结论Grid-BMC用于错误检测是一种实用有效的方法。它在开销和并行化基于SAT的BMC的替代方式方面在计算上是在网络上传递的唯一数据是在开始时,之后不需要同步,直到终止。这种并行化根本没有相互依赖性,因此可以非常有效地利用大型网格中的多个处理器,而不会在处理器之间产生通信开销。该方法有效地利用了基于符号BDD的搜索和SAT的优点,并克服了它们各自的局限性。例如,如果存在大量的分区或者如果某些分区是困难的,则在它们之间执行交叉映像可能是困难的,并且这可能是获得错误的瓶颈。这可以通过基于SAT的 BMC来克服,S. Iyer等/理论计算机科学电子笔记135(2006)3145是 虽然一个非常大的网格(100个节点)是可行的,但在实验中只使用了少量的CPU这表明,提高结果质量的范围和通过进一步研究解决更大问题的可能性引用[1] Amla,N.,R.库尔尚湾McMillan和R. Medel,有界模型检验的不同技术的实验分析,在:TACAS,计算机科学讲义2619(2003),第100页。34比48[2] Asato , A. 和 Y. Kadooka , Grid Middleware for E-economically Utilizing ComputingResources:CyberGRIP,in:Fujitsu Scienti fic and Technical Journal,2004.[3] Biere,A.,E.克拉克河Raimi和Y. Zhu,使用无BDD的符号模型检查的PowerPC微处理器的安全特性,在:Proc. of Computer Aided Verification,Lecture Notes in Computer Science1633(1999),pp. 60比71[4] Bjesse,P.,T. Leonard和A. Mokkedem,Finding Bugs in an Alpha Microprocessor UsingSatifiability Solvers,in:Proc. of Computer Aided Verification,Lecture Notes in ComputerScience2102(2001),pp. 454-464.[5] 布洛姆河,K. Ravi和F. Somenzi,CTL模型检查的符号引导搜索,在:设计自动化会议论文集。,2000,pp. 29比34[6] 博利格湾和I. Wegener,Partitioned BDD vs. other BDD models,in:Proc. of the Intl. 1997年,逻辑综合研讨会。[7] Cabodi,G.,S. Nocco和S. Quer,通过基于BDD的近似遍历改进基于SAT的有界模型检测,在:欧洲设计自动化和测试程序,2003年,第10页。898-903[8] Clarke , E. , A. 比 耶 河 Raimi 和 Y.Zhu , Bounded Model Checking Using SatifiabilitySolving,Formal Methods in System Design19(2001),pp.7[9] Copti,F.,L.菲克斯河Fraer,E. Giunchiglia,G. Kamhi,A. Tacchella和M. Y. Vardi,Benefits of Bounded Model Checking in an Industrial Settings,Proc. 计算机辅助验证,2001,pp。436-453[10] 费尔德曼,Y.,N. Dershowitz和Z. Hanna,并行多线程满意度求解器:设计与实现,在:并行和分布式方法验证研讨会,2004年。[11] 福斯特岛和C. Kesselman,“网格:新计算基础设施的蓝图”。摩根·考夫曼,2003。[12] Ganai,M.,A. Aziz和A.陈建民,以电脑模拟为例,第36届设计自动化研讨会论文集,1999年,页.385-390.[13] Ganai,M. K.,A.古普塔角,巴西-地Yang和P. Ashar,有效的分布式SAT和基于SAT的分布式有界模型检测,在:Proc.of CHARME,2003,pp. 334-347[14] Garavel,H.,R.马提斯库和我陈文生,基于状态空间的并行模型检测方法,2001年第8届国际软件模型检测研讨会论文集,第10页。217-234[15] 古普塔,A.,M.加奈角Wang, Z. Yang和P. Ashar,抽象和BDDs补充日基于SAT的BMC在Di Ver,在:J. Warren A. Hunt和F. Somenzi,editors,Proc. of the 15 Conf.on Computer-Aided Verification,Lecture Notes in Computer Science2725(2003),pp. 206-209.46S. Iyer等/理论计算机科学电子笔记135(2006)31[16] 古普塔,A.,M.加奈角Wang, Z.杨和P.Ashar,从BDD学习基于SAT的有界模型检测,在:第40届设计自动化会议论文集。,2003,pp. 824-829[17] Hazelhurst,S.,O. Weissberg,G. Kamhi和L. Fix,一种混合验证方法:获取日深入到设计,在:Proc.的39设计自动化会议,2002年,页。111-116[18] Heyman,T.,D.盖斯特岛Grumberg和A.李文,大规模并行电路可达性分析中的可扩展性问题。Grumberg ,editor ,Proc. of Computer Aided Verification,Lecture Notes in ComputerScience1855(2000),pp. 20-35[19] 霍,P. - H、T.希普尔湾Harer,J. Kukula,R.陈志荣,应用计算机辅助设计与仿真技术之研究,国立成功大学机械工程研究所硕士论文,2000年。120-126.[20] 伊耶尔,M。K.,G. Parthasarathy和K.- T.郑志荣,一种快速顺序SAT引擎,于:IEEE/ACM计算机辅助设计国际会议论文集,2003年,第10页。320-325[21] Jain,J.,布尔函数的分析,博士论文。电气和计算机工程,德克萨斯大学奥斯汀分校(1993年)。[22] Kuehlmann , A. , V. Paruthi , F. Krohm 和 M. K. Ganai , Robust Boolean ReasoningforEquivalence Checking and Functional Property Verification , IEEE Trans. on CAD21(2002),pp. 公元1377-1394年。[23] Moskewicz,M.,C. Madigan,Y.赵湖,加-地Zhang和S. Malik,Cha Cha:工程日SAT求解器,在:38设计自动化会议的程序,2001年,第530-535[24] Narayan,A.,J. Jain,M. Fujita和A. Sangiovanni-Vincentelli,分块ROBDDs-一个紧凑的,规范的和E可操作的布尔函数表示,在:Proc. of the Intl。计算机辅助设计,1996年,pp。547-554[25] Ravi,K.和F. Somenzi,加速符号遍历的提示。,in:Proc. of CHARME,1999,pp. 250-264。[26] 斯特恩大学和D. L. Dill,将Murphy验证器简化,在:Proc.计算机辅助验证,计算机科学讲义1254(1997),pp.256-267.[27] Stornetta,T. 和F. 布鲁尔, 执行 的 一个 等效平行线 BDD包,在:第33届设计自动化年会论文集(1996年),pp。第641-644页。[28] 扬湾,澳-地和D. R. O’Hallaron, 145-156[29] 杨角,澳-地H.和D. Dill,状态空间的引导搜索验证,在:第35届设计自动化会议,1998年,页。599-604
下载后可阅读完整内容,剩余1页未读,立即下载
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![application/x-rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![application/x-rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)