Robbins algebra: Conditions that make a near-boolean algebra boolean

Some problems posed years ago remain challenging today. In particular, the Robbins problem, which is still open and which is the focus of attention in this paper, offers interesting challenges for attack with the assistance of an automated reasoning program; for the study presented here, we used the program OTTER. For example, when one submits this problem, which asks for a proof that every Robbins algebra is a Boolean algebra, a large number of deduced clauses results. One must, therefore, consider the possibility that there exists a Robbins algebra that is not Boolean; such an algebra would have to be infinite. One can instead search for properties that, if adjoined to those of a Robbins algebra, guarantee that the algebra is Boolean. Here we present a number of such properties, and we show how an automated reasoning program was used to obtain the corresponding proofs. Additional properties have been identified, and we include here examples of using such a program to check that the corresponding hand-proofs are correct. We present the appropriate input for many of the examples and also include the resulting proofs in clause notation.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

ClassBench: a Framework for Automated Class Testing

In contrast to the explosion of activity in object-oriented design and programming, little attention has been given to object testing. We present a novel approach to automated testing designed especially for collection classes. In the ClassBench methodology, a testgraph partially models the states and transitions of the Class-Under-Test (CUT) state/transition graph. To determine the expected behavior for the test cases generated from the testgraph, the tester develops an oracle class, providing essentially the same operations as the CUT but supporting only the testgraph states and transitions. Surprisingly thorough testing is achievable with simple testgraphs and oracles. The ClassBench framework supports the tester by providing a testgraph editor, automated testgraph traversal, and a variety of utility classes. Test suites can be easily configured for regression testing–where many test cases are run–and debugging–where a few test cases are selected to isolate the bug. We present the ClassBench methodology and framework in detail, illustrated on both simple examples and on test suites from commercial collection class libraries. © 1997 John Wiley & Sons, Ltd.     

自动化测试浅析

本文阐述了自动化测试的概念及实现自动化测试的方法,并介绍了主流自动化测试软件及其自动化测试框架的构造,最后简单介绍了用自动化测试脚本语言Tcl实现一硬件系统中主备板间的自动切换的测试事例。     

自动化测试浅析

本文阐述了自动化测试的概念及实现自动化测试的方法，并介绍了主流自动化测试软件及其自动化测试框架的构造，最后简单介绍了用自动化测试脚本语言Tcl实现一硬件系统中主备板间的自动切换的测试事例。     

一种烟叶大中叶率自动检测的有效方法

给出了烟叶大中叶率自动检测设备的基本原理结构；并对如何自动检测烟叶大中叶率这一核心问题，提出了一种方法并详加阐述。该方法运用图像处理技术，分析出传送带上摊薄后的烟叶的边缘，并对边缘进行分析，从而迅速准确地得到大中叶率。为了验证方法的正确性，已研制出相应的自动检测设备，实际的运行结果表明该方法的应用效果令人满意，解决了烟草行业如何高效自动检测大中叶率这一难题。     

基于TestQuest的软件测试自动化方法研究

随着软件开发规模的增大以及复杂程度的增加,自动化测试工具在提高软件测试的效率及准确度上越来越重要,而现有的软件测试存在自动化程度不高、测试过程不完善等问题,针对此问题展开了软件测试自动化的研究。在分析了软件自动化测试的重要性及软件自动化测试的周期、技术的基础上,提出了基于TestQuest测试工具的一套软件测试自动化方法和测试流程,最后针对“虚拟维修训练系统”具体结合工具展开实例验证。     

A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers

Because of the inherent NP-completeness of SAT, many SAT problems currently cannot be solved in a reasonable time. Usually, in order to tackle a new class of SAT problems, new ad hoc algorithms must be designed. Another way to solve a new problem is to use a generic solver and employ parallelism to reduce the solve time. In this paper we propose a parallelization scheme for a class of SAT solvers based on the DPLL procedure. The scheme uses a dynamic load-balancing mechanism based on work-stealing techniques to deal with the irregularity of SAT problems. We parallelize Satz, one of the best generic SAT solvers, with our scheme to obtain a parallel solver called PSatz. The first experimental results on random 3-SAT problems and a set of well-known structured problems show the efficiency of PSatz. PSatz is freely available and runs on any networked workstations under Unix/Linux.     

Optimality strategy of a sealed-offer simultaneous bargaining protocol

Alternating-offer bargaining protocol is the most predominant way for solving bilateral bargaining problem.However,alternating-offer may consume much time and cause a low effciency in some cases.Especially, a deadlock in which both negotiators are unwilling to concede or refuse to disclose more information may arise. Then mediation is required.This paper presents an agent-based sealed-offer simultaneous bargaining protocol by introducing a nonbiased mediator.The information of both agents is considered comp...     

CSCW协同建组自动协商模型研究

文章提出了支持协同工作组建立的自动协商模型,定义了agent协商协议、协商算法和协商agent用于产生及评估offer、counter-offer的效益决策函数,分析了算法时间耗用,与现有协商模型和协商建组FITS/CL框架进行对比,验证了该模型在支持用户参加多个协同组、进行多协商方面的优势,解决了组建立中的群体决策问题,对探索自动建组方式进行有益尝试。     

Oto,a generic and extensible tool for marking programming assignments

Marking programming assignments in programming courses involves a lot of work: each program must be tested, the source code must be read and evaluated, etc. With the large classes encountered nowadays, the feedback provided to students through marking is thus rather limited, and often late. Tools providing support for marking programming assignments do exist, ranging from support for administrative aspects through automation of program testing or support for source code evaluation based on metrics. In this paper, we introduce a tool, called Oto, that provides support for submission and marking of assignments. Oto aims at reducing the workload associated with the marking task. Oto also aims at providing timely feedback to the students, including feedback before the final submission. Furthermore, the tool has been designed to be generic and extensible, so that the marking process for a specific assignment can easily be customized and the tool can be extended with various marking components (modules) that allows it to deal with various aspects of marking (testing, style, structure, etc.) and with programs written in various programming languages. Copyright © 2007 John Wiley & Sons, Ltd.     

FAST: a framework for automating statistics-based testing

To achieve software quality, testing is an essential component in all software development. It involves the execution of a deterministic software system with test data and a comparison of the results with the expected output, which must satisfy the users' requirements. This accounts for over 25% of the cost of a software development. Therefore, automation has considerable potential. The quality programming introduced by Cho can automatically generate data for testing, based on a so-called SIAD tree which is used to represent the hierarchical and network relation between input elements and also incorporates rules into the tree for using the inputs. However, it lacks a clear framework which would show how automated testing can be achieved. To address this problem, we present a Framework for Automating Statistics-based Testing (FAST), which is an extension of the testing concept in quality programming to achieve automated testing. In FAST, we propose a SOAD tree, which is similar to the structure of the SIAD tree, to describe the syntactic structure of the product unit and its defectiveness. Based on this tool, the inspection of test results can be automatically achieved by lexical and syntax analysis. The implementation of automated software testing or Command File Interpreter (CFI) software which incorporates the framework is also described.     

A Milestone Reached and a Secret Revealed

In this special issue of the Journal of Automated Reasoning, this article sets the stage for the succeeding articles, all of which focus on finding proofs of theorems of formal logic and on the various methodologies that were employed. The proofs that are offered mark an important milestone for automated reasoning and for logic, for each of them is indeed new. One key question this article answers is why an automated reasoning program was able to find proofs that had eluded some of the finest mathematicians and logicians for many, many decades.     

一类根式不等式的有理化算法与机器证明

文中讨论了一类根式不等式的有理等价问题.证明了这类根式不等式可等价转化为一组有理不等式.建立了一个算法RFD,并用Maple编程实现.对一个给定的这类根式不等式,RFD可自动快速地产生一组有理等价不等式.将RFD算法和差分代换方法相结合,给出了一大类具有相当难度的几何不等式的机器证明.此前该课题仅有的工作是杨路关于二次根式的结果.     

Recognizing the agent''s goals incrementally:planning graph as a basis

Plan recognition, the inverse problem of plan synthesis, is important wherever a system is expected to produce a kind of cooperative or competitive behavior. Most plan recognizers, however, suffer the problem of acquisition and hand-coding a larger plan library. This paper is aims to show that modern planning techniques can help build plan recognition systems without suffering such problems. Specifically, we show that the planning graph, which is an important component of the classical planning system Graph-plan, can be used as an implicit, dynamic planning library to represent actions, plans and goals. We also show that modern plan generating technology can be used to find valid plans in this framework. In this sense, this method can be regarded as a bridge that connects these two research fields. Empirical and theoretical results also show that the method is efficient and scalable.     

A Polynomial Algorithm for Computing Elementary Siphons in a Class of Petri Nets

A set of elementary siphons plays a key role in the development of deadlock prevention policies for automated manufacturing systems. This paper addresses the computation problem for elementary siphons in a subclass of Petri nets which are basic systems of simple sequential processes with resources (BS³PR) and can model many automated manufacturing systems. An algorithm for enumerating elementary siphons is established by the one‐to‐one relationship between maximal perfect resource‐transition circuits (MPCs) and strict minimal siphons. A set of MPCs is first computed, followed by a set of elementary siphons in a BS³PR. The presented algorithm is proved to have polynomial‐time complexity. An example is used to illustrate the algorithm.     

软件回归测试中的自动测试生成方法

软件回归测试一般使用现有的测试用例集进行测试,如何有效利用这些用例成为回归测试的关键。研究自动对现有测试用例集的扩展,包括自动改变测试用例的执行顺序、自动进行测试用例数目的增减等,提出基于现有测试用例随机生成新的测试用例集的方法。实验证明,该方法生成的测试文件能在原有环境下成功执行,能实现自动测试范围的扩大或缩小,以及测试时间的增加或减少,为软件回归测试提供了有用的自动化工具。     

More efficient automatic repair of large-scale programs using weak recompilation

Automatically repairing a bug can be a time-consuming process especially for large-scale programs owing to the significant amount of time spent recompiling and reinstalling the patched program.To reduce this time overhead and speed up the repair process,in this paper we present a recompilation technique called weak recompilation.In weak recompilation,we assume that a program consists of a set of components,and for each candidate patch only the altered components are recompiled to a shared library.The original program is then dynamically updated by a function indirection mechanism.The advantage of weak recompilation is that redundant recompilation cost can be avoided,and while the reinstallation cost is completely eliminated as the original executable program is not modified at all.For maximum applicability of weak recompilation we created WAutoRepair,a scalable system for fixing bugs with high efficiency in large-scale C programs.The experiments on real bugs in widely used programs show that our repair system significantly outperforms Genprog,a wellknown approach to automatic program repair.For the wireshark program containing over 2 million lines of code,WAutoRepair is over 128 times faster in terms of recompilation cost than Genprog.     

基于MAS的多AGV自动化立体仓库系统设计

结合多台AGV的烟叶配方自动化立体仓库系统的设计,在Multi—Agent系统（MAS）和智能AGV的相关研究的基础上,探讨了在自动化立体仓库系统中应用AGV作为执行智能体实现多智能体协作的自动化仓库系统。采用MAS方法建立了自动化仓库系统模型,并详述了规划Agent和AGV—Agent的实现。该系统的设计提高了企业生产效率,对相关实际应用具有重要意义。     

一类构造性几何不等式的机器证明

阐述了一个基于胞腔分解的不等式证明算法．据此算法编制的Maple通用程序能有效地处理含有根式的不等式型定理,对于Bottema等所著《几何不等式》一书中的大部分不等式定理的验证尤其高效．     

Informational Logic as a Tool for Automated Reasoning

A logical entropy-based Informational Logic is presented which provides new tools for probabilistic automated reasoning and knowledge representation. Applications in automated theorem proving are examined, and a decision theory for probabilistic theorems is proposed.