摘要
针对模型检验算法在工程应用中面临的形式语言局限性和状态空间爆炸的危机,提出了基于断言的形式验证解决方案。通过对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.
出处
《航天控制》
CSCD
北大核心
2007年第3期79-83,共5页
Aerospace Control
关键词
验证
断言
形式验证
模型检验
Verification
Assertion
Formal verification
Model checking
