并发和实时系统的模型检验技术

作     者：董威 王戟 齐治昌 DONG Wei;WANG Ji;QI Zhi-Chang

作者机构：国防科学技术大学计算机学院长沙410073 

基　　金：国家自然科学基金项目! (69973 0 5 1) 国家"八六三"高技术研究发展计划基金! (863 -3 0 6-ZT0 6-0 4-1) 霍英东青年教师基金!(710 

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：2001年第38卷第6期

页      码：698-705页

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

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

学科分类：0810[工学-土木类] 0808[工学-自动化类] 0839[0839] 08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 081202[081202] 

核心收录：

馆 藏 号：203100241...