关键词：
混成系统
形式化方法
仿真
验证
霍尔逻辑
混成关系
可满足性模理论
摘要：
随着软件、集成电路、网络及通信技术的飞速发展,人类生存的自然物理世界与计算机科学领域之间的联系和相互影响愈加的紧密和重要。混成系统,作为一个融合并体现自然物理世界的连续特性及计算的离散特性的基本模型,在最近三十年间,一直受到来自数学、控制、计算机甚至生物化学等众多学科无数专家学者的研究和关注。目前,形式化方法在混成系统的众多研究理论和方法中占有重要的一席。本文,我们主要研究混成系统的建模、仿真和形式化验证。现有的形式化验证技术无法克服状态空间爆炸问题,当混成系统的规模较大时,验证工具往往无法给出验证结果,从而无法判定模型的正确性和安全性,这使得混成系统的形式化验证理论和方法对工业界的影响相当有限。为了融合现有的仿真和验证技术,我们提出协同验证方法,使仿真与验证的方法和技术相结合,充分发挥仿真技术在大规模复杂系统分析上的优势,基于仿真结果的反馈,对验证模型进行抽象,同时利用验证技术在模型检验方面的优势保障模型的正确性和安全性。另一方面,基于验证结果的反馈,可实现仿真模型的优化和更有效的仿真。如此,通过验证与仿真的相互反馈,逐步实现高效、可信的混成系统设计与开发。此外,混成系统建模语言对于实现形式化方法在工业界的广泛应用也是极其重要的。一个结构良好、使用方便的建模语言往往更易于被工业界的设计和开发人员所接受,从而得以推广和应用。华东师范大学何积丰院士最新提出的混成系统建模语言(在本文中,我们使用HML (Hybrid Modeling Language)表示该建模语言),在语法结构上具有设计良好、语法简单等特性。此外,该建模语言还具有很强的可扩展性,非常适合系统设计和开发人员在实际工作中使用。为了支持HML语言的形式化验证,我们基于混成关系理论给出相应的霍尔逻辑推理规则,并将HML模型转换为SMT (Satisfiability Modulo Theories)公式进行约束求解,以实现混成系统的仿真和自动化验证。下面,我们从三个方面对本论文的主要贡献进行总结：·方法贡献基于对混成系统仿真和验证技术的优势及劣势分析,我们提出反馈演进的混成系统模型设计和分析方法。通过仿真技术,我们可以实现大规模复杂系统的分析,但是仿真无法完全覆盖系统所有可能的状态和执行路径,所以基于仿真的系统设计和开发方法,容易产生遗漏和失误,从而为工业生产和公共安全带来严重的安全隐患。基于形式化验证,我们可以对系统所有可能的状态进行分析和检查,从而能够保证系统的正确性和安全性。不过,形式化验证不能有效地对大规模复杂系统进行分析。因此,整合仿真与验证来对混成系统进行分析是很有必要的。我们提出的反馈演进方法充分利用仿真与验证各自的优势,使二者的分析验证能力得以互补,通过分析验证结果互反馈的方式逐步实现大规模复杂混成系统的可信设计与开发。·理论贡献混成关系理论将混成系统的行为表示为三种系统执行状态下的条件约束,基于离散和连续动态行为的特性,分别对动态行为执行前、执行过程中以及执行结束时所满足的条件进行约定。受混成关系基本思想的启发,我们将混成关系与霍尔逻辑相结合,给出一种新的霍尔逻辑推理规则,以支持混成系统建模语言HML的推理验证。与以往的推理系统不同的是,在微分方程的处理上,我们的推理规则并不依赖于特定的方程或不变式求解技术。在我们的推理系统中,推理规则实现的是一个验证的框架,当我们需要对具体的微分方程进行处理时可以自由地选择数学领域成熟的技术来分析。逻辑规则与数学求解的分离可以极大地简化推理规则的复杂度,并支持规则的可扩展性,使我们更好地专注于模型结构和系统行为验证过程的逻辑部分。·实践贡献本文包含丰富的混成系统案例分析,如：地铁屏蔽门控制、列车防碰撞控制、水箱水位控制、倒立摆控制等等。这些案例分析是对我们提出的理论和方法的检验,能够体现所提出的理论和方法的可行性与有效性。此外,我们还基于混成关系理论的基本思想,提出将基于HML语言建立的混成系统模型转换为SMT公式的方法,并整合SMT求解器dReal的约束求解技术,开发了相应的原型工具,实现了HML模型仿真和验证的自动化。该工作在混成系统开发和验证方面为我们的下一步研究打下了坚实的基础。
欢迎来到三峡大学图书馆！
