基于并行环境的模型检查技术研究与实现

分享到

【作者】岳香芬
【刊名】太原师范学院学报(自然科学版)
【作者单位】太原师范学院网络中心
【年份】2012
【卷号】第2期
【页码】95-98
【ISSN】1672-2027
【关键词】模型检查时间自动机可达性分析 MPI
【摘要】针对实时系统模型检查中的突出问题:状态组合爆炸,提出一种基于并行环境的实时系统模型检查技术,用邻接表存储时钟带,用C++和MPI设计并实现了一个并行实时系统模型检查器———PRAModelChecker,选择一个典型的实例对PRAModelChecker的性能进行分析.实验表明,随着系统复杂性的增加,不但能提高工作效率,而且能处理的系统规模可伸缩,从而为从根本上解决状态组合爆炸问题提供了一种新的途径.
【文献类型】期刊