| 摘要 | 第6-8页 |
| ABSTRACT | 第8-10页 |
| 第一章 引言 | 第18-40页 |
| 1.1 研究背景 | 第18-20页 |
| 1.1.1 信息物理融合系统 | 第18-19页 |
| 1.1.2 信息物理融合系统的建模、分析和验证面临的挑战 | 第19-20页 |
| 1.2 相关工作 | 第20-32页 |
| 1.2.1 模型驱动工程 | 第20-22页 |
| 1.2.2 形式化方法 | 第22-27页 |
| 1.2.3 调度理论 | 第27-28页 |
| 1.2.4 相关工作比较 | 第28-32页 |
| 1.3 本文的研究动机和主要工作 | 第32-38页 |
| 1.3.1 本文工作的研究动机 | 第32-36页 |
| 1.3.2 本文的主要工作 | 第36-38页 |
| 1.4 论文结构 | 第38-40页 |
| 第二章 工作基础 | 第40-48页 |
| 2.1 标签信号模型 | 第40-41页 |
| 2.2 超稠密时间 | 第41-42页 |
| 2.3 时钟约束语言—CCSL | 第42-45页 |
| 2.4 本章小结 | 第45-48页 |
| 第三章 扩展的时钟约束语言——eCCSL | 第48-68页 |
| 3.1 eCCSL的语法 | 第48-51页 |
| 3.1.1 时钟终结扩展—eCCSL_ct | 第48-50页 |
| 3.1.2 物理时间扩展—eCCSL_ct_p | 第50-51页 |
| 3.2 eCCSL的操作语义 | 第51-65页 |
| 3.2.1 eCCSL_ct的操作语义 | 第51-59页 |
| 3.2.2 eCCSL_ct_p的操作语义 | 第59-61页 |
| 3.2.3 语义的正确性 | 第61-65页 |
| 3.3 示例—对数字滤波器建模 | 第65-66页 |
| 3.4 本章小结 | 第66-68页 |
| 第四章 eCCSL规约的形式化验证 | 第68-92页 |
| 4.1 验证要检查的属性 | 第68-70页 |
| 4.2 eCCSL_ct规约的验证 | 第70-77页 |
| 4.2.1 eCCSL_ct规约到Promela模型的转换 | 第70-76页 |
| 4.2.2 期待属性的LTL表达模式 | 第76-77页 |
| 4.3 eCCSL_ct_p规约的验证 | 第77-83页 |
| 4.3.1 eCCSL_ct-p规约到UPPAAL时间自动机的转换 | 第77-82页 |
| 4.3.2 期待属性的TCTL表达模式 | 第82-83页 |
| 4.4 验证方法的正确性 | 第83-88页 |
| 4.4.1 带检测点的标号迁移系统 | 第83-85页 |
| 4.4.2 正确性证明 | 第85-88页 |
| 4.5 示例—数字滤波器的eCCSL规约的验证 | 第88-90页 |
| 4.6 本章小结 | 第90-92页 |
| 第五章 eCCSL规约的调度分析 | 第92-128页 |
| 5.1 调度分析要解决的问题 | 第92-98页 |
| 5.1.1 非实时任务调度 | 第92-95页 |
| 5.1.2 实时任务调度 | 第95-98页 |
| 5.2 eCCSL_ct规约的调度分析 | 第98-120页 |
| 5.2.1 调度问题的形式化定义 | 第99-101页 |
| 5.2.2 调度类别及调度时间不敏感性的判定 | 第101-104页 |
| 5.2.3 错误选择探查算法 | 第104-112页 |
| 5.2.4 可采纳调度的识别和状态空间的约简 | 第112-120页 |
| 5.3 eCCSL_ct_p规约的调度分析 | 第120-124页 |
| 5.3.1 可采纳调度和可调度性的识别 | 第121-122页 |
| 5.3.2 调度成功率和调度错失率的判断 | 第122-123页 |
| 5.3.3 调度平均响应时间的判断 | 第123-124页 |
| 5.4 示例—数字滤波器的eCCSL规约的调度分析 | 第124页 |
| 5.5 本章小结 | 第124-128页 |
| 第六章 信号约束语言SCML | 第128-166页 |
| 6.1 信号约束语言SCML | 第128-154页 |
| 6.1.1 SCML设计动机 | 第128-130页 |
| 6.1.2 SCML信号及其分类 | 第130-132页 |
| 6.1.3 SCML信号约束 | 第132-139页 |
| 6.1.4 SCML语义 | 第139-154页 |
| 6.2 基于SCML的建模方法 | 第154-159页 |
| 6.3 SCML规约的形式化验证和调度分析 | 第159-162页 |
| 6.3.1 待检查属性的识别 | 第160-161页 |
| 6.3.2 eCCSL规约的抽取 | 第161-162页 |
| 6.4 本章小结 | 第162-166页 |
| 第七章 案例研究-智能交通控制系统在道口问题上的应用 | 第166-188页 |
| 7.1 案例的建模 | 第166-180页 |
| 7.2 案例规约的分析和验证 | 第180-185页 |
| 7.3 本章小结 | 第185-188页 |
| 第八章 总结与展望 | 第188-192页 |
| 8.1 本文工作总结 | 第188-190页 |
| 8.2 下一步工作 | 第190-192页 |
| 附录A 时钟约束的Promela转换及转换的基于检测点的互模拟关系 | 第192-212页 |
| 附录B 时钟约束的NuSMV转换 | 第212-218页 |
| 附录C 定理5.4的证明 | 第218-222页 |
| 附录D 时钟约束限定的时刻依赖关系 | 第222-226页 |
| 参考文献 | 第226-234页 |
| 攻读博士学位期间发表论文和参与科研情况 | 第234-236页 |
| 致谢 | 第236页 |
