首页 | 本学科首页   官方微博 | 高级检索  
     

并发和实时系统的模型检验技术
引用本文:董威,王戟,齐治昌.并发和实时系统的模型检验技术[J].计算机研究与发展,2001,38(6):698-705.
作者姓名:董威  王戟  齐治昌
作者单位:国防科学技术大学计算机学院
基金项目:国家自然科学基金项目! (69973 0 5 1),国家“八六三”高技术研究发展计划基金! (863 -3 0 6-ZT0 6-0 4-1),霍英东青年教师基金!(710
摘    要:模型检验是一种重要的自动验证技术,通过显式状态搜索或隐式不动点计算来验证并发或实时系统的模态/命题性质,以保证通信协议、数字电路等设计的正确性。详细阐述了模型检验技术的发展与研究现状。首先描述了并发系统分别基于自动机理论和符号化的两种主要模型检验策略,并给出解决状态爆炸问题的主要方法;然后介绍了针对实时系统以及面向对象设计的模型检验方法;对每种方法都介绍了相应的典型工具,最后分析了模型检验面临的困难以及今后的发展趋势。

关 键 词:模型检验  形式化验证  并发系统  实时系统  自动机理论  软件工程

MODEL CHECKING FOR CONCURRENT AND REAL-TIME SYSTEMS
DONG Wei,WANG Ji,QI Zhi-Chang.MODEL CHECKING FOR CONCURRENT AND REAL-TIME SYSTEMS[J].Journal of Computer Research and Development,2001,38(6):698-705.
Authors:DONG Wei  WANG Ji  QI Zhi-Chang
Abstract:Model checking is an important technology of automatic verification. It verifies the modal/proposition properties of concurrent or real-time systems through explicit state exploration or implicit fixpoint computation. It can ensure the correctness of critical application such as communication protocol and digital circuit. In this paper, the development and state-of-art of model checking are expatiated. Two main tactics separately based on automata theory and symbolic structure for concurrent systems are described and the methods to solve state explosion problem are given. Then the methods of model checking for real-time systems and object-oriented designs are introduced. The corresponding known tools for every method are also presented. Finally, the difficulties faced by model checking and its developing trend are analyzed.
Keywords:model checking  formal verification  concurrent  real-time  automata  statecharts
本文献已被 CNKI 维普 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号