基于FSM的测试用例生成算法

研究了基于FSM模型的测试用例自动生成算法来验证实现的FSM与规格FSM的一致性。基于状态机分解的思想提出了新的用例生成方法,DC-方法。相对其他通用方法而言,它不必依据测试树中所有的子路径集合,从而使得用例集减少,同时减少每次重置到初始态的次数,测试序列的长度也有所减少,节省了测试时间,提高了效率,并且具有良好的扩展性,可以方便应用于包含数据流的测试,只需在搜索到所有的DU-Path后直接经过运算就能得出测试用例。并给出了生成用例方法的正确性证明。     

Efficient distributed SAT and SAT-based distributed Bounded Model Checking

SAT-based Bounded Model Checking (BMC), though a robust and scalable verification approach, still is computationally intensive, requiring large memory and time. Even with the recent development of improved SAT solvers, the memory limitation of a single server rather than time can become a bottleneck for doing deeper BMC search for large designs. Distributing computing requirements of BMC over a network of workstations can overcome the memory limitation of a single server, albeit at increased communication cost. In this paper, we present (a) a method for distributed SAT over a network of workstations using a Master/Client model where each Client workstation has an exclusive partition of the SAT problem and uses knowledge of partition topology to communicate with other Clients, (b) a method for distributing SAT-based BMC using the distributed SAT. For the sake of scalability, at no point in the BMC computation does a single workstation have all the information. We experimented on a network of heterogeneous workstations interconnected with a standard Ethernet LAN. To illustrate, on an industrial design with ∼13 K FFs and ∼0.5 million gates, the non-distributed BMC on a single workstation (with 4 GB memory) ran out of memory after reaching a depth of 120; on the other hand, our SAT-based distributed BMC over 5 similar workstations was able to go up to 323 steps with a communication overhead of only 30%.     

Applying SAT Solving in Classification of Finite Algebras

The classification of mathematical structures plays an important role for research in pure mathematics. It is, however, a meticulous task that can be aided by using automated techniques. Many automated methods concentrate on the quantitative side of classification, like counting isomorphism classes for certain structures with given cardinality. In contrast, we have devised a bootstrapping algorithm that performs qualitative classification by producing classification theorems that describe unique distinguishing properties for isomorphism classes. In order to fully verify the classification it is essential to prove a range of problems, which can become quite challenging for classical automated theorem provers even in the case of relatively small algebraic structures. But since the problems are in a finite domain, employing Boolean satisfiability solving is possible. In this paper we present the application of satisfiability solvers to generate fully verified classification theorems in finite algebra. We explore diverse methods to efficiently encode the arising problems both for Boolean SAT solvers as well as for solvers with built-in equational theory. We give experimental evidence for their effectiveness, which leads to an improvement of the overall bootstrapping algorithm.     

基于SAT的串扰时延故障测试

随着深亚微米技术的不断发展和芯片运行速率的不断提高,串扰噪声问题越来越严重,对串扰时延测试已成为一个迫切的问题。在组合电路的基础上,将SAT（布尔可满足性）方法引入到串扰引起的时延测试中,通过词法分析和语法分析直接提取Verilog（硬件描述语言）源码的形式模型,组合成CNF（合取范式）形式。并在非鲁棒测试条件下,激活串扰时延故障,约简CNF范式表达式,最终输入SAT求解器得到测试矢量。在标准电路 ISCAS’85上进行实验验证,结果表明：该算法对于串扰时延故障的测试矢量产生是有效的。     

Reducing Symmetries to Generate Easier SAT Instances

Finding countermodels is an effective way of disproving false conjectures. In first-order predicate logic, model finding is an undecidable problem. But if a finite model exists, it can be found by exhaustive search. The finite model generation problem in the first-order logic can also be translated to the satisfiability problem in the propositional logic. But a direct translation may not be very efficient. This paper discusses how to take the symmetries into account so as to make the resulting problem easier. A static method for adding constraints is presented, which can be thought of as an approximation of the least number heuristic (LNH). Also described is a dynamic method, which asks a model searcher like SEM to generate a set of partial models, and then gives each partial model to a propositional prover. The two methods are analyzed, and compared with each other.     

基于有限元的衰荡光腔内温度分布仿真

衰荡光腔受温度影响长度变化使腔内光斑模式改变,影响测量精度,为达到衰荡光腔内温度均匀分布,利用仿真平台,对控温箱体内加热片发热功率进行仿真计算.首先设计控温箱体几何模型,确定热传导模型和边界条件,通过有限元分析初步确定控温箱体内温度分布;然后通过参数化扫描和迭代运算,优化控温箱体温度场分布,得到均匀化温度分布所需的各加...     

油藏数值模拟有限元并行计算方法研究

针对目前油藏数值模拟普遍采用的有限差分法计算精度低的问题,提出了兼顾计算精度、计算速度问题的有限元油藏数值模拟方法,即在建立了油藏数值模拟数学模型的基础上通过有限元数值分析方法建立有限元数值模型,但有限元在油藏数值模拟时存在单机计算困难、计算时间长的问题,为此提出了利用区域分解技术的油藏数值模拟并行计算方法,最后将该方法通过实例进行检验,取得了良好的加速比和并行效率。     

Unary Quantifiers on Finite Models

In this paper (except in Section 5) all quantifiers are assumedto be so called simple unaryquantifiers, and all models are assumedto be finite. We give a necessary and sufficientcondition for a quantifier to be definablein terms of monotone quantifiers. For amonotone quantifier we give a necessaryand sufficient condition for beingdefinable in terms of a given set of bounded monotonequantifiers. Finally, we give a necessaryand sufficient condition for a monotonequantifier to be definable in terms of agiven monotone quantifier.Our analysis shows that the quantifierat least one half and its relatives behavedifferently than other monotone quantifiers.     

程序中不可达路径的检测方法

对于大型软件来说,程序中不可达路径的存在增加了软件测试的耗费并严重影响了测试的准确性。通过在已生成的基本路径集中排除不可达路径的影响,有利于结构测试中各阶段的实现。提出了一种利用数据流分析信息检测不可达路径的方法。通过对条件分支相关性的探测进而确定了程序中的不可达路径,并通过适当地选取条件谓词,提高了检测分支的覆盖率。     

销钉连接叶片固有特性分析有限元模型研究

计算销钉连接转子叶片动频需采用有限元接触技术,而非线性接触分析难度和计算量都较大,因此提出两种线性简化工程模型,将求解非线性问题转换为求解线性问题,从而大大降低了分析难度和计算量.经检验其计算结果精度可满足工程分析要求.同时对简化柔度矩阵法及面约束简化模型有限元法计算的动频结果进行了分析,对发动机叶片固有振动特性分析有帮助.     

测点数据生成刀具路径研究

为了提高反求加工的效率，提出由大规模测点数据直接生成粗、精加工刀具路径的算法．粗加工采用层切法分层切削材料，首先构造健壮的数据结构——层切网；然后计算无干涉刀位点，并把整个层切网划分为几个优化的子加工区域；最后应用优化的刀路链接法则得到粗加工刀具路径．精加工由大规模数据点构建三角曲面．为了避免干涉，需计算点、面和边的无干涉刀位点．实验结果表明，粗加工刀具路径算法具有较高的效率，只需要占用较小的内存空间；精加工可以成功地避免干涉并且获得可靠的表面精度．     

复杂网络中最短路径问题的求解算法研究

本文以时间代价作为目标函数,针对复杂网络的优化问题进行研究,给出了目标评价函数模型的建立过程,提出了改进的A＊算法求解复杂网络中最短路径问题的算法,并以城市交通为例,对算法进行了验证,实验结果表明所提出的算法可适用于一般多重图中最短路径问题的快速求解,具有广泛的应用价值。     

基于不完全算法的并行FPGA SAT求解器

可满足性问题是计算机理论与应用的核心问题。在FPGA上提出了一个基于不完全算法的并行求解器pprobSAT+。使用多线程的策略来减少相关组件的等待时间,提高了求解器效率。此外,不同线程采用共用地址和子句信息的数据存储结构,以减少片上存储器的资源开销。当所有数据均存储在FPGA的片上存储器时,pprobSAT+求解器可以达到最佳性能。实验结果表明,相比于单线程的求解器,所提出的pprobSAT+求解器可获得超过2倍的加速比。     

基于AutoCAD AME的有限差分网格划分

为满足工程上一些模拟分析的需要，作者实现了基于Allt。CADAME的有限差分网格划分，并在实际工程分析中得以应用而且取得满意结果。     

基于SAT的多目标故障测试向量动态压缩方法

针对传统的自动测试图形向量生成采用逐个求解单一故障模型导致生成测试向量数据量巨大的缺点, 提出一种基于布尔满足性(boolean satisfiability, SAT)的多目标故障测试向量动态压缩方法, 同时论证多目标故障测试生成问题为布尔满足性问题。该方法将具有鲁棒性的SAT算法嵌入经典的动态压缩流程中, 首先利用经典动态压缩算法求解最小测试向量检测大部分失效故障, 然后采用SAT求解器对未测出的多故障电路进行同一求解和附加约束求解方式, 最终得到故障覆盖率高的测试向量和同一测试最大故障列表。实验数据表明, 在相同电路模型情况下, 此方法求得的测试向量相比经典动态压缩减少高达70%。     

基于加强概率控制策略的SAT局部搜索算法

局部搜索算法是目前求解SAT问题比较有效的方法,而Sattime算法是在SAT国际大赛中获得大奖的一种典型局部搜索算法。在Sattime算法的求解过程中,记录变元翻转事件流数据库,通过数据分析与模式挖掘,发现Sattime算法的局部搜索行为中会出现相邻搜索步选择同一个变元的现象,即所谓的回环现象,从而降低了求解效率。为解决此问题,提出两种概率控制策略：加强子句选择策略和加强变元选择策略,并将这两种策略应用到Sattime算法中,形成新的局部搜索算法Sattime-P。实验结果表明,与Sattime算法相比,改进后的Sattime-P算法求解效率有显著的提升。该方法也对其他局部搜索算法的改进具有参考价值。     

Automated workarounds from Java program specifications based on SAT solving

The failures that bugs in software lead to can sometimes be bypassed by the so-called workarounds: when a (faulty) routine fails, alternative routines that the system offers can be used in place of the failing one, to circumvent the failure. Existing approaches to workaround-based system recovery consider workarounds that are produced from equivalent method sequences, automatically computed from user-provided abstract models, or directly produced from user-provided equivalent sequences of operations. In this paper, we present two techniques for computing workarounds from Java code equipped with formal specifications, that improve previous approaches in two respects. First, the particular state where the failure originated is actively involved in computing workarounds, thus leading to repairs that are more state specific. Second, our techniques automatically compute workarounds on concrete program state characterizations, avoiding abstract software models and user-provided equivalences. The first technique uses SAT solving to compute a sequence of methods that is equivalent to a failing method on a specific failing state, but which can also be generalized to schemas for workaround reuse. The second technique directly exploits SAT to circumvent a failing method, building a state that mimics the (correct) behaviour of a failing routine, from a specific program state too. We perform an experimental evaluation based on case studies involving implementations of collections and a library for date arithmetic, showing that the techniques can effectively compute workarounds from complex contracts in an important number of cases, in time that makes them feasible to be used for run-time repairs. Our results also show that our state-specific workarounds enable us to produce repairs in many cases where previous workaround-based approaches are inapplicable.     

基于几何规划的布尔可满足问题求解方法

布尔可满足问题是计算机科学中诸多领域的重要问题,它的快速求解具有十分重要的意义.将具有实际物理背景的Solar算法中的拟物算法与几何规划相结合,提出并实现了一种布尔可满足性问题的连续求解方法.经实验验证,这种算法对布尔可满足性问题的求解具有一定的实用价值.     

时间依赖的网络中最小时间路径算法

时间依赖的网络与传统网络模型相比更具有现实意义,具有广泛的应用领域,交通网络和通信网络可以抽象为时间依赖的网络模型,当模型中弧的工度是时间依赖的变量,最短路径问题的求解变得非常困难,早期的研究者通过具体的网络实例认识到传统最短路径算法在这种情况下是不正确的,因此给出限制性条件使得传统最短路径算法是有效的。该文从最短路径算法的理论基础入手,从理论上证明了传统最短路径算法,如Dijkstra算法和标号设置算法,在时间依赖的网络上不能有效地求解最短路径问题,并且,在没有任何限制性条件下,给出了时间依赖的网络模型,理论基础,求解最小时间路径的优化条件和SPTDN算法,从理论上证明了SPTDN算法的正确性,算法的实验结果是正确的,最后给出了时间依赖的网络应用实例。