实时信息物理系统的实时性分析与验证
| 摘要 | 第1-6页 |
| Abstract | 第6-8页 |
| 目录 | 第8-16页 |
| 第一章 绪论 | 第16-19页 |
| ·课题的背景及意义 | 第16页 |
| ·课题国内外相关研究工作 | 第16-17页 |
| ·课题研究主要内容及组织形式 | 第17-19页 |
| ·论文的主要内容 | 第17-18页 |
| ·论文的组织形式 | 第18-19页 |
| 第二章 背景知识的介绍 | 第19-24页 |
| ·实时信息物理融合系统 | 第19-21页 |
| ·信息物理融合系统 | 第19-20页 |
| ·实时系统 | 第20-21页 |
| ·相关时间概念 | 第21-24页 |
| 第三章 基于MARTE的时间建模 | 第24-32页 |
| ·MARTE中的时间模型 | 第24-28页 |
| ·MARTE中的分配模型 | 第28-30页 |
| ·精密计时的时钟实例 | 第30-31页 |
| ·小结 | 第31-32页 |
| 第四章 时间逻辑 | 第32-39页 |
| ·经典时钟逻辑 | 第32-34页 |
| ·时钟逻辑基础实体 | 第34页 |
| ·区间时序逻辑 | 第34-36页 |
| ·命题区间时序逻辑 | 第35-36页 |
| ·一阶区间时序逻辑 | 第36页 |
| ·时间的通信序列语言(TCSP) | 第36-39页 |
| ·TCSP中的语法 | 第36-37页 |
| ·TCSP中的语义和证明规则 | 第37-39页 |
| 第五章 混合自动机 | 第39-52页 |
| ·建模混合系统 | 第39-46页 |
| ·混合轨迹 | 第39-40页 |
| ·混合自动机 | 第40-44页 |
| ·混合系统的实例 | 第44-46页 |
| ·验证过程 | 第46-52页 |
| ·验证方法 | 第47-49页 |
| ·实例验证 | 第49-52页 |
| 第六章 时钟同步 | 第52-61页 |
| ·时钟内部同步 | 第54-59页 |
| ·时钟外部同步 | 第59-61页 |
| 第七章 最坏执行时间分析 | 第61-95页 |
| ·任务交互 | 第61-64页 |
| ·天花板优先协议 | 第62-63页 |
| ·即时天花板优先协议ICPP | 第63-64页 |
| ·最坏情况执行时间 | 第64-65页 |
| ·基于测量的方法 | 第64-65页 |
| ·静态方法 | 第65页 |
| ·静态分析 | 第65-70页 |
| ·控制流图CFG | 第66-67页 |
| ·晶格理论 | 第67页 |
| ·抽象解释 | 第67-70页 |
| ·模型检测 | 第70-78页 |
| ·时间自动机 | 第71-73页 |
| ·树逻辑的定时计算(TCTL) | 第73-75页 |
| ·TCTL模型检验 | 第75-76页 |
| ·UPPAAL中的模型检验 | 第76-78页 |
| ·时序异常 | 第78-83页 |
| ·形式化定义 | 第79-81页 |
| ·异常减少的方法 | 第81-83页 |
| ·利用UPPAAL进行WCET分析 | 第83-95页 |
| ·初始化UPPAAL模型 | 第83-89页 |
| ·分离程序和抽象硬件的模型 | 第89-93页 |
| ·生成程序模型 | 第93-95页 |
| 第八章 基于自动机的调度分析 | 第95-103页 |
| ·相关的工作 | 第95-96页 |
| ·自动机基本概念 | 第96-98页 |
| ·任务模型 | 第96-97页 |
| ·外界自动机 | 第97-98页 |
| ·动作自动机 | 第98页 |
| ·编码调度 | 第98-103页 |
| ·任务建模 | 第99页 |
| ·动作自动机的可判定性 | 第99-103页 |
| 第九章 离散世界和连续世界的联系 | 第103-113页 |
| ·时钟定义 | 第103-108页 |
| ·时钟定义 | 第103-105页 |
| ·时钟操作 | 第105-108页 |
| ·局部时钟和全局时钟 | 第108-110页 |
| ·局部时钟 | 第108-109页 |
| ·全局时钟 | 第109-110页 |
| ·离散变量和连续变量 | 第110-112页 |
| ·离散变量 | 第110-111页 |
| ·连续变量 | 第111-112页 |
| ·连结机制 | 第112-113页 |
| ·分配 | 第112页 |
| ·微分方程 | 第112页 |
| ·参数的修改 | 第112-113页 |
| 第十章 铁道路口系统例子 | 第113-119页 |
| ·系统需求 | 第113-114页 |
| ·系统描述 | 第114-118页 |
| ·系统验证 | 第118-119页 |
| 总结与展望 | 第119-121页 |
| 参考文献 | 第121-128页 |
| 攻读学位期间发表的论文 | 第128-130页 |
| 致谢 | 第130页 |
