-
公开(公告)号：US20100083233A1
公开(公告)日：2010-04-01
申请号：US12239526
申请日：2008-09-26
申请人： Dries Vanoverberghe , Nikolai Tillmann , Jonathan Paul de Halleux , Nikolaj S. Bjorner , Wolfram Schulte
发明人： Dries Vanoverberghe , Nikolai Tillmann , Jonathan Paul de Halleux , Nikolaj S. Bjorner , Wolfram Schulte
IPC分类号： G06F9/44
CPC分类号： G06F11/3612 , G06F11/3684 , G06F11/3692
摘要： An extension of symbolic execution for programs involving contracts with quantifiers over large and potentially unbounded domains is described. Symbolic execution is used to generate, from a program, concrete test cases that exhibit mismatches between the program code and its contracts with quantifiers. Quantifiers are instantiated using symbolic values encountered during a set of exhibited runs. In this setting, quantifier instantiation is limited to values supplied to or produced by a symbolic execution. Quantifier instantiation is controlled by performing a matching algorithm that uses run-time values of input and program variables in order to guide and limit the set of quantifier instantiations. With a sufficient set of instances, test cases are derived that directly witness limitations of the auxiliary assertions.
摘要翻译： 描述了涉及与大型和潜在无界域上的量词相关联的程序的符号执行的扩展。 符号执行用于从程序生成具有程序代码与其与量词的合同之间不匹配的具体测试用例。 使用在一组展示的运行中遇到的符号值来实例化量词。 在此设置中，量化器实例化被限制为提供给或由符号执行产生的值。 量化器实例化是通过执行使用输入和程序变量的运行时值的匹配算法来控制的，以引导和限制一组量词实例。 使用足够的一组实例，导出直接看到辅助断言的限制的测试用例。
-
公开(公告)号：US08387021B2
公开(公告)日：2013-02-26
申请号：US12239526
申请日：2008-09-26
申请人： Dries Vanoverberghe , Nikolai Tillmann , Jonathan Paul de Halleux , Nikolaj S Bjorner , Wolfram Schulte
发明人： Dries Vanoverberghe , Nikolai Tillmann , Jonathan Paul de Halleux , Nikolaj S Bjorner , Wolfram Schulte
IPC分类号： G06F9/44
CPC分类号： G06F11/3612 , G06F11/3684 , G06F11/3692
摘要： An extension of symbolic execution for programs involving contracts with quantifiers over large and potentially unbounded domains is described. Symbolic execution is used to generate, from a program, concrete test cases that exhibit mismatches between the program code and its contracts with quantifiers. Quantifiers are instantiated using symbolic values encountered during a set of exhibited runs. In this setting, quantifier instantiation is limited to values supplied to or produced by a symbolic execution. Quantifier instantiation is controlled by performing a matching algorithm that uses run-time values of input and program variables in order to guide and limit the set of quantifier instantiations. With a sufficient set of instances, test cases are derived that directly witness limitations of the auxiliary assertions.
摘要翻译： 描述了涉及与大型和潜在无界域上的量词相关联的程序的符号执行的扩展。 符号执行用于从程序生成具有程序代码与其与量词的合同之间不匹配的具体测试用例。 使用在一组展示的运行中遇到的符号值来实例化量词。 在此设置中，量化器实例化被限制为提供给或由符号执行产生的值。 量化器实例化是通过执行使用输入和程序变量的运行时值的匹配算法来控制的，以引导和限制一组量词实例。 使用足够的一组实例，导出直接看到辅助断言的限制的测试用例。
-
公开(公告)号：US07681180B2
公开(公告)日：2010-03-16
申请号：US11759144
申请日：2007-06-06
CPC分类号： G06F11/3688
摘要： In one embodiment a computer system automatically generates unit tests. The computer system accesses a parameterized unit test that provides a base outline from which one or more unit tests are automatically generated, generates input parameter values for a unit of software code, automatically generates a unit test configured to assess the functionality of the unit of software code, and receives test results from a software testing program and provides feedback to a user. In other embodiments, a computer system automatically maintains a unit test database. The computer system receives a unit test at a unit test database, assigns a test identity to the received unit test, determines that the test identity assigned to the received unit test is unique when compared to other unit tests, determines that the received unit test has different functionality coverage characteristics, and adds the received unit test to the unit test database.
摘要翻译： 在一个实施例中，计算机系统自动生成单元测试。 计算机系统访问参数化单元测试，该测试提供一个基本概要，从该自动生成一个或多个单元测试，生成软件代码单元的输入参数值，自动生成单元测试，用于评估软件单元的功能 代码，并从软件测试程序接收测试结果，并向用户提供反馈。 在其他实施例中，计算机系统自动维护单元测试数据库。 计算机系统在单元测试数据库中接收单元测试，为接收到的单元测试分配测试身份，确定与其他单元测试相比，分配给接收单元测试的测试身份是唯一的，确定接收单元测试具有 不同的功能覆盖特性，并将接收到的单元测试添加到单元测试数据库。
-
公开(公告)号：US20080313602A1
公开(公告)日：2008-12-18
申请号：US11763312
申请日：2007-06-14
IPC分类号： G06F9/44
CPC分类号： G06F11/3688 , G06F11/3636
摘要： In one embodiment, a computer system determines that a previously run test scenario configured to test a software program has failed to produce an expected result due to one or more semantic errors, generates error trace code configured to monitor the called component, processes the test scenario using the error trace code, and analyzes error trace information to determine the point at which the semantic error occurs in the called component. In an alternative embodiment, a computer system detects a semantic error in a software component of a software program, constructs an error condition that may include source code representing a minimum condition under which the error occurs, generates an object invariant based on the error condition that represents an opposite condition to that represented by the error condition, and automatically generates source code change recommendations using the object invariant that prevent the semantic error from reoccurring in subsequent test scenarios.
摘要翻译： 在一个实施例中，计算机系统确定配置成测试软件程序的先前运行的测试场景由于一个或多个语义错误而未能产生预期结果，生成被配置为监视被调用组件的错误跟踪代码，处理测试场景 使用错误跟踪代码，并分析错误跟踪信息以确定在被调用组件中发生语义错误的点。 在替代实施例中，计算机系统检测软件程序的软件组件中的语义错误，构建可以包括表示发生错误的最小条件的源代码的错误条件，基于错误条件生成对象不变量， 表示与由错误条件表示的相反的条件，并使用防止在后续测试场景中重现的语义错误的对象不变量自动生成源代码更改建议。
-
公开(公告)号：US07882495B2
公开(公告)日：2011-02-01
申请号：US11763312
申请日：2007-06-14
IPC分类号： G06F9/44
CPC分类号： G06F11/3688 , G06F11/3636
摘要： In one embodiment, a computer system determines that a previously run test scenario configured to test a software program has failed to produce an expected result due to one or more semantic errors, generates error trace code configured to monitor the called component, processes the test scenario using the error trace code, and analyzes error trace information to determine the point at which the semantic error occurs in the called component. In an alternative embodiment, a computer system detects a semantic error in a software component of a software program, constructs an error condition that may include source code representing a minimum condition under which the error occurs, generates an object invariant based on the error condition that represents an opposite condition to that represented by the error condition, and automatically generates source code change recommendations using the object invariant that prevent the semantic error from reoccurring in subsequent test scenarios.
摘要翻译： 在一个实施例中，计算机系统确定配置成测试软件程序的先前运行的测试场景由于一个或多个语义错误而未能产生预期结果，生成被配置为监视被调用组件的错误跟踪代码，处理测试场景 使用错误跟踪代码，并分析错误跟踪信息以确定在被调用组件中发生语义错误的点。 在替代实施例中，计算机系统检测软件程序的软件组件中的语义错误，构建可以包括表示发生错误的最小条件的源代码的错误条件，基于错误条件生成对象不变量， 表示与由错误条件表示的相反的条件，并使用防止在后续测试场景中重现的语义错误的对象不变量自动生成源代码更改建议。
-
公开(公告)号：US20080307264A1
公开(公告)日：2008-12-11
申请号：US11759144
申请日：2007-06-06
IPC分类号： G06F11/00
CPC分类号： G06F11/3688
摘要： In one embodiment a computer system automatically generates unit tests. The computer system accesses a parameterized unit test that provides a base outline from which one or more unit tests are automatically generated, generates input parameter values for a unit of software code, automatically generates a unit test configured to assess the functionality of the unit of software code, and receives test results from a software testing program and provides feedback to a user. In other embodiments, a computer system automatically maintains a unit test database. The computer system receives a unit test at a unit test database, assigns a test identity to the received unit test, determines that the test identity assigned to the received unit test is unique when compared to other unit tests, determines that the received unit test has different functionality coverage characteristics, and adds the received unit test to the unit test database.
摘要翻译： 在一个实施例中，计算机系统自动生成单元测试。 计算机系统访问参数化单元测试，该测试提供一个基本概要，从该自动生成一个或多个单元测试，生成软件代码单元的输入参数值，自动生成单元测试，用于评估软件单元的功能 代码，并从软件测试程序接收测试结果，并向用户提供反馈。 在其他实施例中，计算机系统自动维护单元测试数据库。 计算机系统在单元测试数据库中接收单元测试，为接收到的单元测试分配测试身份，确定与其他单元测试相比，分配给接收单元测试的测试身份是唯一的，确定接收单元测试具有 不同的功能覆盖特性，并将接收到的单元测试添加到单元测试数据库。
-
公开(公告)号：US08473895B2
公开(公告)日：2013-06-25
申请号：US12795669
申请日：2010-06-08
IPC分类号： G06F9/44
CPC分类号： G06F17/5045 , G06F2217/08
摘要： A design space exploration (DSE) system automatically discovers viable solutions within a design space. The DSE system operates by creating or receiving a design specification that is described using a design language. The design specification contains a collection of constraints that an acceptable architecture is expected to satisfy. The DSE system then symbolically executes the design specification to provide a logical formula. The DSE system then interacts with a theorem prover module to identify one or more solutions to the formula. Finally, the DSE system converts the solutions into a user-interpretable form (e.g., expressed in the format of the modeling language) for viewing by a user. Each solution pertains to an architecture that satisfies the collection of constraints. The DSE system ensures that the solutions are diverse by disfavoring any solution that is deemed similar to any solution that has been previously encountered.
摘要翻译： 设计空间探索（DSE）系统在设计空间内自动发现可行的解决方案。 DSE系统通过创建或接收使用设计语言描述的设计规范进行操作。 设计规范包含可接受架构预期满足的约束集合。 DSE系统然后象征性地执行设计规范以提供逻辑公式。 然后，DSE系统与定理证明器模块进行交互，以识别公式的一个或多个解决方案。 最后，DSE系统将解决方案转换成用户可解释的形式（例如，以建模语言的格式表示），以供用户观看。 每个解决方案都涉及满足约束集合的体系结构。 DSE系统确保解决方案是多样的，因为不满意任何与以前遇到过的解决方案相似的解决方案。
-
公开(公告)号：US20110302550A1
公开(公告)日：2011-12-08
申请号：US12795669
申请日：2010-06-08
IPC分类号： G06F9/44
CPC分类号： G06F17/5045 , G06F2217/08
摘要： A design space exploration (DSE) system automatically discovers viable solutions within a design space. The DSE system operates by creating or receiving a design specification that is described using a design language. The design specification contains a collection of constraints that an acceptable architecture is expected to satisfy. The DSE system then symbolically executes the design specification to provide a logical formula. The DSE system then interacts with a theorem prover module to identify one or more solutions to the formula. Finally, the DSE system converts the solutions into a user-interpretable form (e.g., expressed in the format of the modeling language) for viewing by a user. Each solution pertains to an architecture that satisfies the collection of constraints. The DSE system ensures that the solutions are diverse by disfavoring any solution that is deemed similar to any solution that has been previously encountered.
摘要翻译： 设计空间探索（DSE）系统在设计空间内自动发现可行的解决方案。 DSE系统通过创建或接收使用设计语言描述的设计规范进行操作。 设计规范包含可接受架构预期满足的约束集合。 DSE系统然后象征性地执行设计规范以提供逻辑公式。 然后，DSE系统与定理证明器模块进行交互，以识别公式的一个或多个解决方案。 最后，DSE系统将解决方案转换成用户可解释的形式（例如，以建模语言的格式表示），以供用户观看。 每个解决方案都涉及满足约束集合的体系结构。 DSE系统确保解决方案是多样的，因为不满意任何与以前遇到过的解决方案相似的解决方案。
-
公开(公告)号：US08468505B2
公开(公告)日：2013-06-18
申请号：US12551345
申请日：2009-08-31
IPC分类号： G06F9/45
CPC分类号： G06F9/463
摘要： A state component saves a present state of a program or model. This state component can be invoked by the program or model itself, thereby making state a first-class citizen. As the state of the program evolves from the saved state, the saved state remains for reflection and recall, for example, for testing, verification, transaction processing, etc. Using a state reference token, the saved state of the program or model can be accessed by the program or model. For example, the program or model by utilizing a state component, can return itself to the saved state. After returning to the saved state, a second execution path can be introduced without requiring re-execution of the actions leading to the saved state. In another example, the state space of an executing model is saved in order to generate inputs required to exercise a program or model.
-
10.发明授权公开(公告)号：US07747985B2
公开(公告)日：2010-06-29
申请号：US11085624
申请日：2005-03-18
申请人： Colin L. Campbell , Lev Borisovich Nachmanson , Margus Veanes , Michael Barnett , Nikolai Tillmann , Wolfgang Grieskamp , Wolfram Schulte
发明人： Colin L. Campbell , Lev Borisovich Nachmanson , Margus Veanes , Michael Barnett , Nikolai Tillmann , Wolfgang Grieskamp , Wolfram Schulte
IPC分类号： G06F9/44
CPC分类号： G06F11/36
摘要： Techniques and tools for testing multi-threaded or distributed software systems are described. For example, a multi-threaded system is instrumented and executed to produce logs of events that are performed by each of its agents. The agent logs contain a totally ordered series of events per agent, as well as information about accesses to resources shared between the agents. With this information, a partial ordering of the events performed by all the agents is described for the execution. The agent logs are then multiplexed into one or more serialized event orderings, which can then be compared to a specification of the system in a conformance testing engine.
摘要翻译： 描述了用于测试多线程或分布式软件系统的技术和工具。 例如，多线程系统被检测和执行以产生由其每个代理执行的事件的日志。 代理日志包含每个代理的完全有序的事件序列，以及有关访问代理之间共享的资源的信息。 利用该信息，描述所有代理执行的事件的部分排序用于执行。 代理日志然后被复用到一个或多个序列化的事件顺序中，然后可以将其与在一致性测试引擎中的系统的规范进行比较。
-
-
-
-
-
-
-
-
-
搜索结果
76 条记录 (耗时 0.029 秒)
