论文部分内容阅读
模型检验是一种重要的自动验证技术，通过显式状态搜索或隐式不动点计算来验证并发或实时系统的模态/命题性质，以保证通信协议、数字电路等设计的正确性.详细阐述了模型检验技术的发展与研究现状.首先描述了并发系统分别基于自动机理论和符号化的两种主要模型检验策略，并给出解决状态爆炸问题的主要方法；然后介绍了针对实时系统以及面向对象设计的模型检验方法；对每种方法都介绍了相应的典型工具.最后分析了模型检验面临的困难以及今后发展趋势.