基于组合不可行路径的组合线性混成自动机可达性验证研究

发布时间：2021-10-13 13:56

　　信息物理系统广泛应用于安全攸关领域,因此要保证其正确性与安全性至关重要。混成自动机是一种既包含了离散的状态转移,又存在连续变量变化的形式化建模语言。其中离散的逻辑跳转与连续的变量变化混合的特性使得其可以用于对信息物理系统建模与验证。然而正因为离散跳转与连续行为的交织,使得其状态空间极为复杂,即便是对混成自动机安全性问题的可达性问题的验证也异常困难。在实际的信息物理系统中,由于不同组件通信协作行为的大量存在,组合混成自动机才能满足其建模需求。组合混成自动机由多个单一混成自动机通过同步行为协作构成,其行为比单一混成自动机更为复杂。目前的研究工作能解决的组合混成自动机验证问题的规模极为有限。因此如何提高组合混成自动机可达性验证规模,提升验证效率是十分值得关注与研究的课题。本文针对组合混成自动机的子类——组合线性混成自动机的可达性验证进行了系统化研究,研究内容包括:1.基于混合语义的组合线性混成自动机有界可达性验证。本文工作提出了一种基于混合语义的组合线性混成自动机有界可达性验证方法。该方法采用传统交替语义枚举候选路径,浅同步语义验证路径行为。通过将组合自动机的离散图结构编码为SAT问题的方式... 

【文章来源】：南京大学江苏省 211工程院校 985工程院校 教育部直属院校

【文章页数】：79 页

【学位级别】：硕士

【部分图文】：

图４－８：?ＦＤＤ［实验数据??

在?ＦＤＤ丨和?Ｒｉｎｇ－Ｓｈａｐｅ?Ｆｉｓｃｈｅｒ?的不可达版本中，ＢＡＣＨ－ｓｔｅｐ?与?ＢＡＣＨ－??ｍｕｌｔｉｐｌｅ?能处?理的问?题?规模相?Ｍ?。?ｆｒ：?ＦＤ［）Ｉ?模型上?ｍｕｌｔｉｐｌｅ?幣体?能在?更短的??时间内完成验证，原因在于精确定位的１ＩＳ能帮助约减吏多的路径，节约验证??时间。在Ｒｉｎｇ－Ｓｈａｐｅ?Ｆｉｓｃｈｅｒ上验证时间基本持平，分析发现，该模型在图结构??

在?ＦＤＤ丨和?Ｒｉｎｇ－Ｓｈａｐｅ?Ｆｉｓｃｈｅｒ?的不可达版本中，ＢＡＣＨ－ｓｔｅｐ?与?ＢＡＣＨ－??ｍｕｌｔｉｐｌｅ?能处?理的问?题?规模相?Ｍ?。?ｆｒ：?ＦＤ［）Ｉ?模型上?ｍｕｌｔｉｐｌｅ?幣体?能在?更短的??时间内完成验证，原因在于精确定位的１ＩＳ能帮助约减吏多的路径，节约验证??时间。在Ｒｉｎｇ－Ｓｈａｐｅ?Ｆｉｓｃｈｅｒ上验证时间基本持平，分析发现，该模型在图结构??

【参考文献】：
期刊论文
[1]基于组合IIS路径抽取的组合线性混成系统有界可达性分析优化[J]. 解定宝,周岳翔,卜磊,王林章,李宣东.  中国科学:信息科学. 2017(03)
[2]混成系统形式化验证[J]. 卜磊,解定宝.  软件学报. 2014(02)

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



本文编号：3434802