基于层次模型的混合系统形式化分析与验证

发布时间：2020-09-03 17:06

　　 随着科技的进步,尤其是电子技术的长足发展,以及社会生产和生活的需求,计算机相关的技术对各种技术领域的涉及程度越来越广泛和深入,这就导致了以连续与离散行为共存为特点的混合系统的广泛使用。我们从形式化地角度来研究混合系统。目前混合系统的形式化分析、验证与模拟方法主要有两类,即演算推演法和混合自动机法,二者的理论都已经比较成熟,都要求将实例空间映射到理论空间,而后应用这些成熟的理论和方法进行分析验证。但是上述两个空间的映射,即建模方法,目前还比较混乱,并没有形成统一的有效框架,还处于具体实例具体分析的手工阶段。 混合系统的研究对象包含控制系统、嵌入式系统和Cyber Physical系统等,这些系统的设计阶段都大量采用了成熟的层次化设计思路,并生成大量的层次化设计文档。那么快速准确地从层次化设计中得到混合系统形式化分析模型,并对此模型进行分析验证的工作就非常具有实际意义。 本文研究将这种工业界常用的层次化设计,直接对应到混合系统形式化分析对象的方法。我们的依据是一种广泛采用的层次化设计概念模型[24],首先研究这种层次化概念模型的符号化表示,即层次化形式模型,而后基于此形式模型,探讨时段演算推演方法及混合自动机方法的语义,将此层次化混合系统形式模型映射为时段公式或混合自动机,最后按照(扩展)时段演算和混合自动机理论进行分析验证,并给出实例来阐述这种方法的可行性。
【学位单位】：兰州大学
【学位级别】：博士
【学位年份】：2011
【中图分类】：O242.1;N94
【部分图文】：

基于层次模型的混合系统形式化分析与个复杂的大问题变成许多简单的小问题，而且形式化的层次模型可混合系统的时间驱动和事件驱动行为。这种层次化分析方法是一种如著名的因特网051模型)，适用性强，分析步骤简单清晰的方法，非际问题的快速刻画。层次化方法己经是工业界广泛采用的设计方法，合系统设计都采用或者可以通过简单变换而对应到这种方法。过对国内外同行相关文献的研读和相关工作的追踪，和对目前可见系统建模方法的比较，我们选取图3.2中的层次化建模方法作为我们，并称图中所示的层次化建模方法为混合系统的层次化概念模型，型列出了一条完整地分层描述混合系统的途径。

图4.2:时间轴上的棍合系统层次化概念模型「加、〕表示时间段上每一个时间点都为真的断言，即描述全状「尸魂等价于了尸一乙由于时间点上的断一言成立.与否不会影响时段演算的结果，所以不将这种断盲一单独列出，仅仅用「1来表示，依据推演时的上下问点断一言。这里我们也不考虑这种断一言的语义。最后，量化的断言口尸和令尸分别表示混合系统‘最终”和“总是”，其语义如下:I江口p卫【乙，e{全V乙，e任!O，co」:11今p卫【乙，。」全日乙，e任【O，oo」:三。.1江p卫【白，e」三。一I江p卫【吞，e」4.3.1基于混合系统层次化形式模型的证明体系

图4.3:比例积分智能控制时水位随时间的曲线使用扩展时段演算推演程控水箱系统4.1可知，系统设计凡咖，5在所有时段上都为真，即「凡咖们来证明三条安全性性质:「凡vbs川井口「0三h。三H八。:t司

【参考文献】

相关期刊论文 前1条

1 李晓山，周巢尘;时段演算综述[J];计算机学报;1994年11期

本文编号：2811712