一种基于遗传算法的概率假设 保证验证方法与实现
    点此下载全文
引用本文:马艳,曹子宁.一种基于遗传算法的概率假设 保证验证方法与实现[J].南京邮电大学学报:自然科学版,2019,39(6):54~61
摘要点击次数: 153
全文下载次数: 79
作者单位
马艳 南京航空航天大学 计算机科学与技术学院江苏南京211106 
曹子宁 南京航空航天大学 计算机科学与技术学院江苏南京211106
南京航空航天大学 高安全系统的软件开发与验证技术工业和信息化部重点实验室江苏南京211106
南京航空航天大学 模式分析与机器智能工业和信息化部重点实验室江苏南京211106
光电控制技术重点实验室河南洛阳471023 
基金项目:国家重点基础研究发展计划(973计划)(2014CB744903)、中国航空科学基金(20150652008,20185152035)、中央高校业务基金(NZ2013306)、国家自然科学基金(61303022,61572253)、江苏省高校自然科学研究重大项目(17KJA520002)和留学人员科技创新择优资助项目
中文摘要:概率假设 保证推理(Probabilistic Assume Guarantee Reasoning)是一种用于缓解随机模型检测中状态空间爆炸的方法,其将整个系统的验证分解为对较小组件的验证,组合较小组件的验证结果以达到对整个系统的验证。针对目前基于学习的概率假设 保证推理过程的缺陷:因学习假设过程中所有中间结果都需要存储而造成很高的空间复杂度,提出一种基于遗传算法(Genetic Algorithm,GA)学习假设的概率假设 保证推理方法,并将其用于组合验证MDP的正则安全性质。遗传算法本质上是一种随机算法,它的正确性通过满足训练集中的所有约束条件保证。该方法不需要记录中间结果,只需记录问题域和训练集的编码。因此,大大降低了产生假设的空间复杂度。实现了该概率假设 保证推理框架的原型工具,并通过领导人选举协议的实例对比了其有效性。
中文关键词:随机模型检测  假设 保证推理  遗传算法  正则安全性
 
Method for genetic algorithm based probabilistic assume guarantee verification and realization
Abstract:The probabilistic assume guarantee reasoning is an efficient method for combating the state space explosion problem in stochastic model checking.It decomposes the verification of a system into its smaller components and composes back the results.Because all the intermediate results need to be stored in the process of learning assumption,the present probabilistic assume guarantee reasoning is in high space complexity.To deal with this,a novel probabilistic assume guarantee reasoning framework by learning assumption is presented based on a genetic algorithm (GA),and is used to verify MDP about the regular safe property.GA is essentially a randomized algorithm,in which intermediate results donot be recorded,only the encoding of the problem domain and the training set need to be memorized.Therefore,it reduces the space complexity of reasoning process.The prototype for the probabilistic assume guarantee reasoning framework is implemented,and results obtained by an example of a leader election protocol are proved to be effective.
keywords:stochastic model checking  assume guarantee reasoning  genetic algorithm  regular safe property
查看全文  查看/发表评论  下载PDF阅读器

你是第2363818访问者
版权所有《南京邮电大学学报(自然科学版)》编辑部
Tel:86-25-85866913 E-mail:xb@njupt.edu.cn
技术支持:本系统由北京勤云科技发展有限公司设计