• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Symposium on Verification: Theory and Practice; 20030629-20030704; Taormina; IT >Unit Checking: Symbolic Model Checking for a Unit of Code
【24h】

Unit Checking: Symbolic Model Checking for a Unit of Code

机译：单位检查：代码单位的符号模型检查

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We present a symbolic model checking approach that allows verifying a unit of code, e.g., a single procedure or a collection of procedures that interact with each other. We allow temporal specification that make assertions about both the program counters and the program variables. We decompose the verification into two parts: (1) a search that is based on the temporal behavior of the program counters, and (2) the formulation and refutation of a path condition, which inherits conditions on the program variables from the temporal specification. This verification approach is modular, as there is no requirement that all the involved procedures are provided. Furthermore, we do not require that the code is based on a finite domain. The presented approach can also be used for automating the generation of test cases for unit testing.
机译：我们提出一种符号模型检查方法，该方法允许验证代码单元，例如，单个过程或相互交互的过程的集合。我们允许对程序计数器和程序变量都进行断言的时间指定。我们将验证分解为两部分：（1）基于程序计数器的时间行为的搜索；（2）路径条件的公式化和反驳，该路径条件继承了时间规范中程序变量的条件。这种验证方法是模块化的，因为不要求提供所有涉及的过程。此外，我们不要求代码基于有限域。所提出的方法还可以用于自动生成用于单元测试的测试用例。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号