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

1、基于组合不可行路径的组合线性混成自动机可达性验证研究信息物理系统广泛应用于平安攸关领域 , 因此要保证其正确性与平安性至关 重要。混成自动机是一种既包含了离散的状态转移 , 又存在连续变量变化的形式 化建模语言。其中离散的逻辑跳转与连续的变量变化混合的特性使得其可以用于对信息 物理系统建模与验证。然而正因为离散跳转与连续行为的交织 , 使得其状态空间 极为复杂 , 即便是对混成自动机平安性问题的可达性问题的验证也异常困难。在实际的信息物理系统中 , 由于不同组件通信协作行为的大量存在 , 组合混 成自动机才能满足其建模需求。 组合混成自动机由多个单一混成自动机通过同步 行为协作构成 , 其行为

2、比单一混成自动机更为复杂。目前的研究工作能解决的组合混成自动机验证问题的规模极为有限。 因此如 何提高组合混成自动机可达性验证规模 , 提升验证效率是十分值得关注与研究的 课题。本文针对组合混成自动机的子类组合线性混成自动机的可达性验证进 行了系统化研究 , 研究内容包括 :1. 基于混合语义的组合线性混成自动机有界可 达性验证。本文工作提出了一种基于混合语义的组合线性混成自动机有界可达性 验证方法。该方法采用传统交替语义枚举候选路径 , 浅同步语义验证路径行为。通过将组合自动机的离散图结构编码为 SAT问题的方式寻路,接下来通过将候选路径行 为编码为线性约束问题求解的方式来验证路径的可达性。

3、为了更进一步地缩减状态空间 , 约减遍历的路径数 , 本文给出了在浅同步语 义下一致 , 而在传统交替语义下不同的三种非典型路径的定义 , 同时给出了在路 径遍历阶段躲避非典型路径的编码方法。 2. 基于多重 IIS 的组合线性混成自动机 面向路径可达性验证加速。IIS 加速技术可以用于加速对组合线性混成自动机验证的加速。然而 , 不同 的 IIS 路径对于路径的约减能力大相径庭。为了利用 IIS 加速技术约减更多的路径 , 本文提出了一种基于共享事件分割 的多重 IIS 加速技术。该方法在 IIS 获取阶段采用多重 IIS 技术, 从一个不可解 的约束集提取出多个 IIS 路径组。接下来,

4、为了将提取的 IIS 路径锁定在更精确的范围内 ,提出了一种基于共 享事件分割的 IIS 定位方法。根据共享事件的位置分割路径 , 在不同的子路径上 进一步求解 IIS 。我们实现了该方法并在业内广泛使用的例子上进行了实验。实验结果说明 , 采用这一系列的优化后验证效率与处理问题的规模得到了极大的提升 , 表现优于 领域内相关工具。3. 基于组合不可行路径的组合线性混成自动机全局性质推导。 上述方法在组 合线性混成自动机的有界可达性验证上取得了一定的进展 , 但实际应用中往往需 要验证系统的全局性质。因此本文提出了一种基于组合不可行路径的组合线性混成自动机全局性质推导方法。该方法设计了一种针对组合不可行路径的LTL约束编码方式，同时提出了一种非典型路径躲避规那么的 LTL约束编码方法。但这样生成的LTL逻辑约束尤其冗杂,即便是一个只有3,4个自动机的组合 系统,生成的LTL逻辑约束也超过了求解器的求解范围。针对这一问题，本文提出 了一种LTL约束本地化的方法,极大地缩减了 LTL约束,扩展了全局验证的问题