公开(公告)号：US07058910B2

公开(公告)日：2006-06-06

申请号：US10180043

申请日：2002-06-27

申请人： Ramesh Bharadwaj ,  Steve Sims

发明人： Ramesh Bharadwaj ,  Steve Sims

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： An invariant checking method and apparatus using binary decision diagrams (BDDs) in combination with constraint solvers for determining whether a system property is an invariant of a system description. The invariant checking method receives system descriptions and system properties and transforms them into a model formula. Specific variables are eliminated from the model formula and a corresponding output formula is generated. The output formula is transformed into a logic formula by substituting a new logic variable for each integer constraint in the output formula. A constrained BDD is constructed from the logic formula. The constrained BDD uses a heuristic algorithm to order the logic variables in the paths leading to true or false. A constraint solver is applied to the integer constraints that correspond to the occurrences of logic variables in the BDD paths, which determines whether the system property is or is not an invariant of the system description.

摘要翻译： 使用二进制决策图（BDD）与约束求解器结合的用于确定系统属性是否是系统描述的不变性的不变检查方法和装置。 不变检查方法接收系统描述和系统属性，并将其转换为模型公式。 从模型公式中消除具体变量，并生成相应的输出公式。 通过为输出公式中的每个整数约束替换新的逻辑变量，将输出公式转换为逻辑公式。 受限BDD由逻辑公式构成。 受限制的BDD使用启发式算法来排序导致true或false的路径中的逻辑变量。 约束求解器被应用于对应于BDD路径中的逻辑变量的出现的整数约束，其确定系统属性是否是系统描述的不变量。

公开(公告)号：US06745757B2

公开(公告)日：2004-06-08

申请号：US09770768

申请日：2001-01-25

申请人： Steve Sims

发明人： Steve Sims

IPC分类号： F41B520

CPC分类号： F41B5/1426

摘要： An accessory for modifying the decay pattern of vibrations set up in an implement to which the accessory is attached, and the combination of a decay pattern modifying accessory and an implement. Methods of manufacturing decay pattern modifying accessories are also disclosed.

摘要翻译： 用于修改在附件附接的工具中设置的振动的衰减模式的附件，以及衰减模式修改附件和工具的组合。 还公开了制造衰减图案修改附件的方法。

公开(公告)号：US20050160321A1

公开(公告)日：2005-07-21

申请号：US10499583

申请日：2002-12-19

申请人： Rance Cleaveland ,  Steve Sims ,  David Hansel

发明人： Rance Cleaveland ,  Steve Sims ,  David Hansel

IPC分类号： G06F11/00 ,  G06F11/36

CPC分类号： G06F11/3684

摘要： A method for generating test cases for software and a test case generator comprising a simulator that drives software under test from one input state to the next. The simulator is constrained by predetermined criteria to visit states that meet the criteria thus preserving computer resources. The states reached by the simulator are tested.

摘要翻译： 一种用于生成用于软件的测试用例和测试用例发生器的方法，包括将一个测试中的软件从一个输入状态驱动到下一个的模拟器。 模拟器受到预定标准的约束，以访问满足标准的状态，从而保留计算机资源。 测试模拟器达到的状态。