基于T3BDD的动态模型检查S

摘要

cqvip:ＪａｖａＢｅａｕｓ是一种组件标准．该文定义了ＪＢＤＬ（ＪａｖａＢｅａｎｓｄｅｓｃｒｉｐｔｉｏｎｌａｎｇｕａｇｅ）语言，用于描述组件语义约束规范．为了检测ＪａｖａＢｅａｎｓ组件语义约束与其实现之间的一致性，文章给出了一种基于Ｔ3ＢＤＬ公式的三值语义和模型的抽象化动态模型检查方法、文章重点介绍了利用ＴＢＤＤ（３－ｔｅｒｍｉｎａｌｂｉｎａｒｙｄｅｃｉｓｉｏｎｄｉａｇｒａｍ）的符号化动态模型检查方法．