基于T3BDD的动态模型检查*
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

本文研究得到国家自然科学基金和国家863高科技术项目基金资助.


T3BDD Based Dynamic Model Checking
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    Java Beans是一种组件标准.该文定义了JBDL(Java Beans description language)语言,用于描述组件语义约束规范.为了检测Java Beans组件语义约束与其实现之间的一致性,文章给出了一种基于JBDL公式的三值语义和模型的抽象化动态模型检查方法.文章重点介绍了利用T3BDD(3-terminal binary decision diagram)的符号化动态模型检查方法.

    Abstract:

    Java Beans is a standard for software components. For checking the consistency of the Java Beans semantic constraints with its implementation, a formal Java Beans description language (JBDL) and a dynamic model checking method are proposed in this paper. The authors contribute an efficient symbolic model checking approach using T3BDD. The approach is based on three valued semantics for JBDL formulas and a kind of abstract model which is dynamically established and evolved during Bean’s execution.

    参考文献
    相似文献
    引证文献
引用本文

倪 彬,冯玉琳,黄 涛.基于T3BDD的动态模型检查*.软件学报,1999,10(10):1025-1031

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:1998-07-07
  • 最后修改日期:1998-10-19
  • 录用日期:
  • 在线发布日期:
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号