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

Aspect Validation Using Model Checking

机译：使用模型检查进行方面验证

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

摘要

The model checking of applications of aspects is explained, by showing the stages and proof obligations when a collection of generic aspects (called a super-imposition) is combined with a basic program. We assume that both the basic program and the collection of aspects have their own specifications. The Bandera tool for Java programs is used to generate input for model checkers, although any similar tool could be employed. New verification aspects and superimpositions are defined to modularize the proofs, and separate the proof-related code from the program and the aspects. This allows generating and activating a series of model checking tasks automatically each time a superimposition is applied to a basic program, achieving superimposition validation. A case study that monitors and checks an underlying bounded buffer program is presented.
机译：通过显示一组通用方面（称为叠加）与基本程序结合时的阶段和证明义务，说明了方面应用程序的模型检查。我们假设基本程序和方面的集合都有自己的规范。尽管可以使用任何类似的工具，但是Java程序的Bandera工具用于生成模型检查器的输入。定义了新的验证方面和叠加，以对证明进行模块化，并将与证明相关的代码与程序和方面分开。这允许每次将叠加应用于基本程序时自动生成并激活一系列模型检查任务，从而实现叠加验证。提出了监视和检查底层有界缓冲区程序的案例研究。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号