嵌入式周期控制系统的建模与分析

1、C 易发表用yiT论女第表匸冢嵌入式周期控制系统的建模与分析【摘要】 ： 嵌入式周期控制系统广泛应用于汽车电子，航空电子等安全 攸关的嵌入式领域一般来说，这些控制系统都具有周期性行为，它们 的共同特点是：(1)以模式为基础一个周期控制系统由一组模式组成，系统处于一个模式表示系统处于一个特定的状态每个模式或是包含若干子模式，或是周期性地进行控制计算.(2)面向计算在一个模式中, 周期控制系统会执行包含复杂的计算过程的控制算法例如，在特点的模式下，一个汽车电子控制系统可以需要处理大量的即时数据，以便确定车辆的位置和姿态.(3)周期性周期控制系统是一个反应式系统，可 能会连续运行很长一段时间每个模式

2、的行为由其自身的周期决定因 此，大部分的计算任务都是在一个周期内完成的.如果没有发生模式切 换，那么这些计算任务还将在下一个周期再次执行在周期结束时，如果满足特定的条件，系统将从当前模式转入其它模式.尽管这类系统被广泛地应用于航天/航空，汽车电子等安全攸关 的嵌入式领域，但是工业界仍然缺少一种针对这一领域的形式化建模 语言我们曾对现有的建模语言做过广泛的调研，这些语言或是较为复 杂,使用门槛较高，或是过于通用,难以处理这类系统的特征因此，我们 根据领域工程师的需求，设计了 SPARDL 建模框架.该框架主要包括两 个部分，第一部分是作为建模标记的模式图(ModeDiagram),第二部分是规范

3、语言 SPRL.模式图是以经典的状态图(Statecharts)56 为基础，增加了支持周期 控制系统建模的特殊领域需求的建模标记.模式图的核心部分是一组模式.每个模式都有特点的周期长度.不同的模式的周期可以不同在 周期结束时,如果满足一定的条件，将发生模式切换允许模式嵌套，也 允许模式-子模式之间发生切换.与其它建模语言相比，SPARDL 的特 色之一是模式之间的迁移条件是可以涉及历史状态的时序表达式.模式图的结构是层次化的，分为模式-控制流-模块三个层次一个 模式既可以包含若干子模式，也可以包含一个控制流控制流是特定的 控制算法，计算任务的封装.控制流的细节在控制流层面表述允许在 控制流中

4、调用模块，模块的细节在模式层展示.为了支持模式图的形式化推理,SPARDL 框架还包括基于区段演算 42的规范语言该语言适于描述领域工程师关心的时序性质.SPARDL 模型的正确性取决于它的模式图是否满足规范yiT论女第表站冢SPARDL 模型可能涉及到复杂的非线性运算，因此，完整的验证是不可 行的为了解决这个问题，本文利用概率模型检查技术125,126验证SPARDL 模型.试验结果表明，本文的方法学能够发现真实系统中的设 计错误.本文主要有下列贡献：提出了新的形式化建模框架 SPARDL，该框架的主要目的是为嵌 入式周期控制程序提供一套清晰而准确的建模机制.通过两种方式研究了 SPARDL

5、 的形式化语义，一是将 SPARDL 模 型解释为价格时间自动机(Priced Timed Automata)，二是在迁移系统上 定义它的操作语义在操作语义的基础上讨论了 SPARDL 的类型安全, 互模拟，等价等问题.在形式化语义的基础上，实现了 SPARDL 的仿真并扩展了最初的 操作语义,提出了 SPARDL 的概率语义.根据新的概率语义，开发了以 仿真为基础的概率模型检查，用于验证 SPARDL 模型是否满足各种时.由于序性质.在真实的案例中试用了 SPARDL 眶架,发现了一个控制系统中的 两个真实的缺陷试用结果充分说明了 SPARDL 的有效性.【关键词】：嵌入式周期控制系统形式化

6、方法语义验证【学位授予单位】：华东师范大学【学位级别】：博士【学位授予年份】：2012【分类号】：TP368.1;TP273【目录】:摘要 7-8Abstract8-13 第一章 绪论 13-29 1.1 嵌入式周期控制系统的特征与问题 13-18 1.2 软件建模，分析与验证方法 概述18-251.3 本文的选题和主要工作 25-29 第二章 SPARDL 的框架 29-492.1 建模语言 29-39 2.2 规范描述语言 39-48 2.3 本章小结 48-49 第三章 SPARDL 的时间自动机模型 49-733.1 价格时间自动机 49-58 3.2 NPTA 的概率模型检查 58-

7、623.3 模 式图到PTA 的映射 62-723.4 本章小结 72-73 第四章 SPARDL 的语义73-99 4.1 操作语义 73-82 4.2 类型规则 82-89 4.3 SPARDL 的互模 拟89-98 4.4本章小结98-99第五章模型仿真99-109 5.1方法概 述99-101 5.2模式图 101-105 5.3 控制流 105-107 5.4 本 章 小 结 107-109 第六章 概率模型检查 109-1236.1 概 率语义 109-1186.2 验证区间时序逻辑 118-120 6.3 本章小结 120-123 第七章 实 现与试验 123-1317.1 SP

8、ARDL 工具链的实现 123-1257.2 使用SPARDL建模125-127 7.3概率模型检查127-130 7.4 本 章 小 结 130-131第八章 结束语 131-1358.1 相关工作比较 131-134 8.2进一步的工作 134-135 附录 A 语法定义 135-139 A.1 一些基本元素 的产生式 135-137A.2 模式图的产生式 137-138 A.3 区间时序逻辑公式的产生式 138-139 附录 B 正文中定理的证明 139-145B.1定理 4.2.4 的证明 139-140 B.2 定理 4.2 .5 的证明 140 B.3 定 理 4.2.6 的证明 140-141 B.4 定理 4 .2.7 的证明 141 B.