混成系统有界模型检验优化技术研究

发布时间：2017-12-16 03:28

  本文关键词：混成系统有界模型检验优化技术研究

  更多相关文章： 混成系统 线性混成自动机 非线性混成自动机 有界可达性检验 面向路径可达性检验 基于SAT的路径遍历 Satisfiability Modulo Theories 线性时序逻辑 不可约不可解子集

【摘要】：混成系统是一类包含连续和离散行为的复杂系统,被广泛应用于工业控制系统的建模,混成自动机是当前其主流建模语言,混成自动机的有界模型检验是保障系统可靠性和安全性的重要途径。混成自动机有界模型检验的基本思想是通过SMT (Satisfiability Modulo Theories)技术对系统在阈值内的行为进行编码并求解,以检验系统是否满足相关性质。但是由于这种方法需要提前一次性计算出系统阂值内所有的状态空间,如此高的计算复杂性限制了其能处理的系统规模,难以应用到工业界的实际系统。另一种解决问题的思路是将整个系统的有界模型检验问题分解成系统内各路径的检验问题来控制单次验证的复杂度,在此基础上遍历系统内路径完成整个系统的有界模型检验。尽管这种面向路径的有界模型检验途径有效地提升了可检验的系统规模,但是当面对工业界的大规模系统时仍然需要有效的优化技术进一步控制解决问题的复杂性。本文基于混成系统面向路径的有界模型检验途径,针对有界可达性问题研究相关优化技术,在状态空间约减、组合系统遍历优化、基于局部验证推导全局性质、非线性系统检验等四个方面取得以下结果：·提出了SAT-HS-LP联合反馈制导的状态空间约减方法。首先基于SAT编码模型的离散结构有向图并求解,尽量在早期发现不可行路径；然后针对在路径可达性检验过程中确定的不可行路径,利用不可约不可解子集(Irreducible Infeasible Subset, IIS)技术从中定位出不可行子路径片段,在后续的搜索中只需枚举不包含相关不可行路径片段的路径进行检验,从而约减了状态空间。实验显示,该方法大幅度地提升了面向路径有界可达性检验的性能和规模。·针对组合线性混成系统,提出了一种基于组合IIS路径抽取的遍历优化方法。基于SMT编码模型的离散结构有向图并求解,从而在组合系统的图结构上快速枚举出符合同步语义的路径组；依据组合自动机的同步语义,从不可行路径组里抽取不可行组合路径片段,从而在后续路径遍历过程中规避包含这些片段的路径。实验显示该方法提高了组合系统可达性检验的效率。·提出了一种基于有界可达性检验结果推导出系统全局性质的途径。在有界可达性检验的过程中,会不断地收集到不可行子路径片段,当相关不可行子路径片段积累较多的时候,可能导致程序离散图结构上已经不存在能连通起点至目标点的潜在路径,在此情况下有界不可达性质可以进一步被推广到全局状态空间,并可以通过基于线性时序逻辑(Linear Temporal Logic, LTL)模型检验的方法来完成对该类问题的自动证明。·针对非线性混成自动机,提出了基于路径的有界可达性检验方法及相关优化技术。通过将路径可达性问题转换成一组带量词的非线性约束的可满足性问题,可以调用非线性约束求解器进行判定,在此基础上使用深度优先搜索依次枚举并验证阂值内的候选路径,从而完成有界可达性检验。进一步,提出了一种从非线性约束里抽取IIS的分析算法,可以从不可行的路径里定位出不可行子路径片段以约减状态空间。受限于当前底层支撑工具和非线性约束求解器的能力,所提方法目前仅得到可行性验证,其有效性还有待进一步的验证。
【学位授予单位】：南京大学
【学位级别】：博士
【学位授予年份】：2016
【分类号】：TP301.1

【相似文献】

中国期刊全文数据库 前10条

1 李浪;李仁发;李肯立;姚凤娟;;混成系统研究综述[J];计算机应用研究;2008年08期

2 侯建民,郑滔,樊晓聪,李宣东,郑国梁;线性混成系统的参数分析[J];计算机学报;1999年06期

3 范双南;;基于时间序列分析的混成系统可靠性评价方法[J];福建电脑;2011年03期

4 邹进;林望;罗勇;曾振柄;;基于多面体包含的非线性混成系统可达性分析[J];计算机应用;2013年05期

5 卜磊;解定宝;;混成系统形式化验证[J];软件学报;2014年02期

6 乔磊;齐骥;龚育昌;;一种支持可重构混成系统的操作系统设计与实现[J];计算机学报;2009年05期

7 赵剑;欧阳丹彤;王晓宇;张立明;;混成系统的分布式诊断方法[J];吉林大学学报(工学版);2012年06期

8 肖娟;;混成系统的形式验证[J];长沙通信职业技术学院学报;2008年01期

9 叶林;汤瀑;郭立鹏;张亮;;基于混成系统的物联网服务建模与验证[J];小型微型计算机系统;2013年12期

10 阎安,唐稚松;基于 XYZ/ E的混成系统(英文)[J];软件学报;2000年01期

中国重要会议论文全文数据库 前1条

1 任雁;田婕;孙辉;周永;;混成系统测试研究综述[A];2011年通信与信息技术新进展——第八届中国通信学会学术年会论文集[C];2011年

中国博士学位论文全文数据库 前5条

1 解定宝;混成系统有界模型检验优化技术研究[D];南京大学;2016年

2 林望;基于符号数值混合计算的混成系统可信分析与验证研究[D];华东师范大学;2013年

3 赵剑;混成系统基于模型诊断的若干问题研究[D];吉林大学;2012年

4 孔辉;基于归纳不变式的混成系统安全性验证[D];清华大学;2013年

5 李广元;LTLC：面向实时与混成系统的连续时序逻辑[D];中国科学院软件研究所;2001年

中国硕士学位论文全文数据库 前6条

1 杨阳;基于深度优先搜索的混成系统有界可达性分析[D];南京大学;2013年

2 蒋慧;基于迁移系统语义的线性混成系统分析[D];南京大学;2013年

3 邹进;非线性混成系统的可达性分析[D];温州大学;2013年

4 李倩;基于形式化方法的混成系统安全性检验[D];华东师范大学;2015年

5 钱宇清;Hybrid AADL：混成系统体系结构分析与设计语言[D];华东师范大学;2014年

6 钱磊;信息物理融合系统的形式化建模与讨论[D];华东师范大学;2013年

，

本文编号：1294546