基于T3BDD的动态模型检查S

摘要：

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

关键词：组件、Java Beans、形式规范、符号化、模型检查、二叉判定图

所属期刊栏目：10

分类号：TP311(计算技术、计算机技术)

资助基金：中国科学院资助项目;国家自然科学基金

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：1025-1031