| 摘要 | 第1-8页 |
| Abstract | 第8-17页 |
| 第一章 绪论 | 第17-31页 |
| ·背景及动机 | 第17-23页 |
| ·形式化方法 | 第18-22页 |
| ·混合系统 | 第22-23页 |
| ·相关工作 | 第23-26页 |
| ·混合系统建模 | 第23-24页 |
| ·可达性符号分析 | 第24-25页 |
| ·混合系统推理验证 | 第25页 |
| ·混合系统抽象 | 第25-26页 |
| ·主要贡献 | 第26-28页 |
| ·论文结构 | 第28-31页 |
| 第二章 Event-B语言及Rodin平台 | 第31-43页 |
| ·Event-B | 第31-39页 |
| ·Event-B数学语言 | 第32页 |
| ·环境 | 第32-33页 |
| ·机器 | 第33-35页 |
| ·环境扩展 | 第35-36页 |
| ·机器精化 | 第36-39页 |
| ·形式化开发方法 | 第39页 |
| ·Rodin平台 | 第39-41页 |
| ·主要插件列表 | 第40-41页 |
| ·本章小结 | 第41-43页 |
| 第三章 从需求分析到开发实现 | 第43-65页 |
| ·引言 | 第43-44页 |
| ·形式化开发方法 | 第44-49页 |
| ·需求文档 | 第45页 |
| ·精化策略 | 第45-47页 |
| ·Event-B语言建模及Rodin平台证明 | 第47-49页 |
| ·建模之后 | 第49页 |
| ·工业应用示例 | 第49-63页 |
| ·系统主要目的 | 第50页 |
| ·需求文档 | 第50-56页 |
| ·需求分析 | 第56-57页 |
| ·精化策略 | 第57-60页 |
| ·精化策略的综合分析 | 第60页 |
| ·形式化开发 | 第60-62页 |
| ·证明结果统计 | 第62页 |
| ·实时性及确定性分析 | 第62-63页 |
| ·本章小结 | 第63-65页 |
| 第四章 显式时间方程的混合系统开发 | 第65-93页 |
| ·引言 | 第65页 |
| ·开发方法 | 第65-70页 |
| ·连续行为系统的开发 | 第65-68页 |
| ·Event-B混合系统的开发 | 第68-70页 |
| ·示例 | 第70-92页 |
| ·齿锯 | 第70-73页 |
| ·核反应堆温度控制 | 第73-78页 |
| ·火车控制 | 第78-83页 |
| ·飞机防碰撞 | 第83-92页 |
| ·本章小结 | 第92-93页 |
| 第五章 工业设计模式与互补开发方法 | 第93-141页 |
| ·引言 | 第93-95页 |
| ·方法描述 | 第95-99页 |
| ·“Click”方法及线性混合系统开发的设计模式 | 第95-98页 |
| ·Matlab的辅助运用 | 第98页 |
| ·从证明中发现条件与不变式 | 第98-99页 |
| ·从理想模型精化出传感器与执行器 | 第99页 |
| ·示例 | 第99-123页 |
| ·齿锯示例重塑 | 第100-104页 |
| ·压力机 | 第104-110页 |
| ·进程互斥 | 第110-116页 |
| ·传感器模型 | 第116-122页 |
| ·飞机防碰撞仿真 | 第122-123页 |
| ·水箱控制的工业开发 | 第123-140页 |
| ·需求文档 | 第124-126页 |
| ·初步研究：何时改变水泵状态 | 第126-127页 |
| ·发现问题 | 第127-128页 |
| ·举例说明 | 第128-129页 |
| ·精化策略 | 第129页 |
| ·定义常数和其约束 | 第129-130页 |
| ·初始模型 | 第130-133页 |
| ·初始化 | 第133页 |
| ·第一精化模型 | 第133-136页 |
| ·第二精化模型 | 第136-137页 |
| ·证明 | 第137页 |
| ·示例再观察 | 第137-139页 |
| ·Matlab仿真 | 第139-140页 |
| ·本章小结 | 第140-141页 |
| 第六章 微分方程下的混合系统开发 | 第141-165页 |
| ·引言 | 第141-142页 |
| ·欧拉逼近 | 第142-143页 |
| ·特殊情况的前向欧拉逼近 | 第143-148页 |
| ·证明方法介绍 | 第143-146页 |
| ·示例 | 第146-148页 |
| ·前向欧拉逼近与非标准分析 | 第148-151页 |
| ·证明方法介绍 | 第148-149页 |
| ·示例 | 第149-151页 |
| ·另一特殊情况的前向欧拉逼近 | 第151-157页 |
| ·问题表述 | 第151-152页 |
| ·前向欧拉逼近的研究 | 第152-157页 |
| ·后向欧拉逼近 | 第157-160页 |
| ·同时使用两种欧拉逼近 | 第160-162页 |
| ·The Focus示例 | 第161页 |
| ·该示例的解析解 | 第161-162页 |
| ·该示例的解逼近分析 | 第162页 |
| ·本章小结 | 第162-165页 |
| 第七章 Event-B到Simulink转化的工具实现 | 第165-187页 |
| ·引言 | 第165-166页 |
| ·插件的使用 | 第165-166页 |
| ·本章结构 | 第166页 |
| ·转换的哲学 | 第166-169页 |
| ·优点与缺点 | 第167页 |
| ·主要概念 | 第167-169页 |
| ·过滤器 | 第169-170页 |
| ·数学构造 | 第169-170页 |
| ·Event-B语义 | 第170页 |
| ·离散系统变迁 | 第170-176页 |
| ·常量 | 第171页 |
| ·变量 | 第171-172页 |
| ·事件 | 第172-176页 |
| ·混合系统转换 | 第176-180页 |
| ·时间函数 | 第176-177页 |
| ·Click方法和微分方程 | 第177-180页 |
| ·示例 | 第180-185页 |
| ·本章小结 | 第185-187页 |
| 第八章 总结与展望 | 第187-191页 |
| ·总结 | 第187-188页 |
| ·展望 | 第188-191页 |
| 附录A | 第191-199页 |
| A.1 Event-B事件与Simulink状态变迁的等价性证明 | 第191-194页 |
| A.1.1 等价性问题描述 | 第191-192页 |
| A.1.2 Rodin等价性证明 | 第192-194页 |
| A.2 压力机案例的Rodin最终精化模型 | 第194-199页 |
| A.2.1 环境 | 第194页 |
| A.2.2 最终的精化模型机器 | 第194-199页 |
| 参考文献 | 第199-209页 |
| 致谢 | 第209-211页 |
| 攻读博士学位期间发表论文与参与科研项目情况 | 第211-213页 |