-
题名基于抽象和组合方法的网络协议验证
- 1
-
-
作者
陈道喜
张广泉
徐成凯
陈国彬
-
机构
苏州技师学院
苏州大学计算机科学与技术学院
重庆工商大学融智学院
-
出处
《计算机科学》
CSCD
北大核心
2015年第7期118-121,共4页
-
基金
江苏省自然科学基金(BK2011281)
苏州市应用基础研究计划(SYG201241)
+1 种基金
江苏省普通高校研究生科研创新计划(CXLX13_820)
重庆市教委科学技术研究项目(KJ133103)资助
-
文摘
由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的LTL性质,建立各个通信主体的Kripke结构,再对该Kripke结构进行抽象;然后组合抽象模型;最后运用Spin对组合抽象模型进行检验。为验证该方法的有效性,对NSPK协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。
-
关键词
KRIPKE结构
状态爆炸
组合抽象模型
LTL模型检测
-
Keywords
Kripke structure
State explosion
Composition abstraction model
LTL model checking
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名基于层次组合抽象的智能系统形式化验证
- 2
-
-
作者
周益龙
韩斌
-
机构
江苏科技大学计算机学院
-
出处
《计算机与数字工程》
2019年第8期1917-1920,1984,共5页
-
文摘
论文针对智能系统提出了一种形式化建模和验证的方法:首先,采用层次化的思想将智能系统分为应用层、系统层和设备层,综合系统功能需求和硬件模块分别建立各层的Kripke结构模型;然后,根据组合模型规则将层次模型进行组合,经过抽象处理后得到系统组合抽象模型。最后,以能源共享系统为例,用CSP#描述系统模型、LTL描述系统性质,利用PAT工具完成系统模型的自动验证。实验结果表明,该方法综合考虑了系统各个主体的行为,能够有效找出智能系统中的设计缺陷,并且可以缓解模型检测中的状态空间爆炸问题。
-
关键词
形式化方法
智能系统
组合抽象模型
模型检测
-
Keywords
formal method
smart system
combination abstract model
model checking
-
分类号
TP18
[自动化与计算机技术—控制理论与控制工程]
-
