【作者】 何安平；

【导师】 李廉；

【作者基本信息】 兰州大学 ， 应用数学， 2011， 博士

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

【Abstract】 The evolution of electronics, as well as the requirements of human activities, makes computer related technologies involving in each field of engineering, widely and deeply, e.g., the reason of why the hybrid systems, characterized by both discrete and continuous behaviors, are common now. We study the hybrid system in a formal way. The formal methods of hybrid system contain formal analysis, formal verification and validation, all of which are based on calculus and hybrid automata generally. The theories of these calculus or automata are well-studied and extended, but modeling is now a challenge.Control system, embedded system and cyber physical system belong to hy-brid systems, each of them adopts hierarchical methodology while designing. Then it is basic and significant to quickly generate the accurate formal model from these hierarchical designs.In this thesis, we try to find a direct theoretical way that maps the hierar-chical designs into the formal model of hybrid system, e.g., with a widely used hierarchical design model[24], we symbolize the hierarchical design and get the hierarchial formal model. Then we study the semantics of both duration calculus and hybrid automata based on the hierarchical formal model, and then study the way of analysis and validation with some practical case studies.更多还原