基于CDFG和OVL的系统验证性质分类  

Property Classification for System Verification on CDFG Structure

作　　者：朱明[1] 边计年[1] 吴为民[1] 

机构地区：[1]清华大学计算机系设计自动化实验室,北京100084

出　　处：《计算机工程》2005年第10期48-50,共3页Computer Engineering

基　　金：国家自然科学基金资助项目(60273011);国家"863"高技术研究发展计划基金资助项目(2003AA115110)

摘　　要：在数据控制流图(CDFG)结构的基础上,结合模拟验证和模型检测的优点,对需要验证的系统性质进行分类,采用不同的验证方法,提高验证的能力。通过对OVL语言和CTL描述进行改进,针对模拟验证、CDFG图匹配、模型检测3种方法设计相应的性质,实验结果表明这种分治验证策略有助于提高系统验证的效率和规模。Based on the advantages of simulation and formal verification with CDFG structure, classified properties are proposed to activate their good qualities respectively. Improving on OVL assertions and CTL properties, three kinds of properties are defined and verified, and the experimental results demonstrate the scheme improves the verification efficiency and scale.

关 键 词：模拟 形式验证 性质 模型检测 数据控制流图 

分 类 号：TP391.9[自动化与计算机技术—计算机应用技术]