论文摘要
混成系统以核心控制器的形式广泛出现于航天运输、机械控制等安全攸关领域。因此,通过形式化验证对相关系统的质量保障进行研究十分重要。混成自动机是混成系统主要设计建模语言,因此现有研究主要集中于混成自动机安全性验证。然而由于混成自动机中连续行为与离散行为交织,导致混成自动机的验证复杂度很高,现有工作仍无法对大规模系统进行验证,即使是线性混成自动机(LHA)的可达性问题也被证明不可判定。与之相比,迁移系统是一种描述系统行为在状态与状态间跳转的离散系统。迁移系统领域的形式化验证研究相当成熟,目前已有很多成熟的技术和工具可以对大规模迁移系统进行分析与验证。事实上,所有形式化模型的行为状态序列本质上是状态间的迁移过程。因此,本文试图给出LHA到与其等价的线性迁移系统(LTS)的构造方法,然后利用LTS的已有工作进行分析,以期实现对大规模LHA进行多种问题验证的目标。具体来说,本文工作如下：·提出了LHA的等价LTS构造方法,并对两者等价性给出形式化证明。该等价构造方法通过引入时间变量t与节点上的自循环迁移来描述系统任意时刻的行为,并成功消除传统迁移系统表达中所包含的存在量词、全称量词。·在上述等价性构造的基础上,基于LTS上的成熟技术,从安全性验证、活性验证和稳定性分析三个方向展开对LHA的验证探索。其中：。安全性验证从判定LTS的可达性角度开展,选择面向迁移系统的模型检验工具ARMC对LHA分析。实验表明：在大规模线性混成自动机的安全性验证上,本文方法无论从可验证系统规模还是同一问题的验证效率上都大幅领先现有技术。o活性验证是LHA验证的一大难题,目前尚无相关工作展开。本文从判定LTS的可终止性角度开展,选择面向迁移系统的可终止性判定工具ARMC,成功高效地判定了LHA系统的可终止性。此工作是相关领域的一个突破性尝试。o稳定性分析主要从LTS的不变式生成角度开展,并使用了LTS上基于抽象解释和基于约束求解两套经典不变式生成框架,分别选择工具Interproc和InvGen进行分析,并依据所生成的不变式对原LHA进行自动反馈精化。实验表明,此方法可以挖掘出原模型中大量隐藏信息,从而对系统进行精化并加速后续验证的展开。