混成系统是一类兼具离散与连续行为的复杂系统,其离散行为受事件驱动,连续行为随时间变化,在实时控制领域应用广泛。由于实时控制系统广泛应用于安全攸关领域,使用混成自动机进行建模并验证系统安全性成为相关领域的重要研究问题。但是混成系统的验证复杂度极高,即使是线性混成自动机的可达性问题也是一个不可判定的问题。在目前的软硬件技术的限制下,使用混成自动机进行模型检验能够处理的问题规模十分有限。因此,如何控制混成自动机模型检验的复杂度、提高检验效率与可处理问题规模是相关研究热点所在。同时实际系统进行模型验证代价较高,如何将模型检验技术实际运用到真实系统中也是相关领域重点关注问题之一。针对以上的问题,本文从以下方面展开系统研究:·基于面向路径编码的组合线性混成自动机有界可达性技术研究。组合线性混成自动机的有界可达性验证由于具有极高的复杂度,能够处理的问题规模有限,所以如何降低模型检验的复杂度并且提高模型检验的效率这个问题就很重要。本文提出一种基于经典STEP语义的面向路径的有界可达性验证方法,通过插入TAU迁移的方法约减图结构遍历的编码复杂度,并给出TAU迁移导致的路径爆炸问题的解决方案,极大的提高了组合线性混成自动机的模型检验效率。实验证明本文的方法比原先的方法效果更优,核反应堆控制系统模型的21个自动机组成的组合线性混成自动机也能在1s内给出结果,时间效率与能处理问题的规模上都要高于领域内相关工作。·线性混成自动机有界可达性验证全局性质推导研究。线性混成自动机的有界可达性验证验证结果只在一定的步长阈值内有效,其全局性质的归约可满足性结果不可知,如何得到线性混成自动机的全局性质结果受到大量研究者的关注与重视。本文提出一种根据IIS路径片段增量式地构建buchi自动机完成全局性质推导方法,在有界可达性检验的过程中在线地完成全局性质的推导,并能在推导出全局不可达结果后立即停止有界模型检验。本文方法不仅整合了有界可达性验证与全局性质推导,而且提高了线性混成自动机的有界可达性检验的效率,特别在步长阈值设定较大的情况下,本文方法能够显著提升检验效率。·基于混成自动机的事件驱动物联网实时系统验证与修复研究。近年来物联网设备开始实用化,智能家居设备大量出现在用户家庭生活中。智能家居实时系统与用户的人身和财产安全息息相关,其安全性问题十分重要。但是系统中存在系统复杂多变、用户毫无专业知识等问题。针对这些问题,我们提出了一种全自动地基于线性混成自动机模型检验技术的事件驱动物联网实时系统的建模、验证与修复框架。我们通过用户具有的设备与对应的IFTTT规则,自动化的完成线性混成自动机的建模过程。我们使用混成自动机可达性检测工具完成系统安全性检测。我们使用基于分析反例约束的量词消去技术完成系统修复建议的生成。最终我们完成工具原型MenShen,即使46个智能设备与65条用户规则组成的复杂系统也能够迅速给出检验结果,并且得到超过80%的用户满意度。