|
|||||
|
|
| 基于断言的形式验证方法应用研究 | |
| 引用本文： | 王青,杨孟飞. 基于断言的形式验证方法应用研究[J]. 航天控制, 2007, 25(3): 79-83 |
| 作者姓名： | 王青 杨孟飞 |
| 作者单位： | 北京控制工程研究所,北京,100080;中国空间技术研究院,北京,100094 |
| 摘 要： | 针对模型检验算法在工程应用中面临的形式语言局限性和状态空间爆炸的危机,提出了基于断言的形式验证解决方案。通过对DW8051_timer模块的实际验证,说明了该方法可以简化模型检验算法在工程实践中的应用,并且与传统仿真方法相比,它能在一定程度上缓解航天领域数字系统设计中的验证困境。 |
| 关 键 词： | 验证 断言 形式验证 模型检验 |
| 文章编号： | 1006-3242(2007)03-0079-05 |
| 修稿时间： | 2006-10-19 |
Research on the Application of Assertion-Based Formal Verification |
|
| Wang Qing,Yang Mengfei. Research on the Application of Assertion-Based Formal Verification[J]. Aerospace Control, 2007, 25(3): 79-83 | |
| Authors: | Wang Qing Yang Mengfei |
| Abstract: | 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. |
| Keywords: | Verification Assertion Formal verification Model checking |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |