基于断言的形式验证方法应用研究  

Research on the Application of Assertion-Based Formal Verification

作　　者：王青[1] 杨孟飞[2] 

机构地区：[1]北京控制工程研究所,北京100080 [2]中国空间技术研究院,北京100094

出　　处：《航天控制》2007年第3期79-83,共5页Aerospace Control

摘　　要：针对模型检验算法在工程应用中面临的形式语言局限性和状态空间爆炸的危机,提出了基于断言的形式验证解决方案。通过对DW8051_timer模块的实际验证,说明了该方法可以简化模型检验算法在工程实践中的应用,并且与传统仿真方法相比,它能在一定程度上缓解航天领域数字系统设计中的验证困境。In view of the limitation of the formal language and the crisis of the state space explosion of the model checking algorithm in applications, an assertion-based formal verification strategy which can solve these problems effectively is presented in this paper. The experiment results of DW8051_timer demonstrate that this strategy can simplify the application of model checking algorithm in engineering. Compared with the conventional simulation verification, this method also mitigates the verification difficulty in the spaceflight digital system design.

关 键 词：验证 断言 形式验证 模型检验 

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