面向同步语言的多时钟嵌入式系统行为分析方法研究

摘要

随着安全关键嵌入式系统广泛运用在航空航天，交通运输，核电核能等领域，软件安全越来越多的影响人们的生命和财产安全。与此同时，此类软件对系统效率，资源利用，响应时间，多时钟属性和安全相关性质等有着更高的要求。如何对此类系统进行设计与分析，成为学术界和工业界的热点研究问题。随着系统的复杂性不断增加，对于具有多时钟性质的此类系统需求日益增加。同步语言SIGNAL是一种声明式数据流同步设计语言，多时钟的同步语言SIGNAL适合建模具有多时钟性质的嵌入式反应系统，丰富的表达能力也给此类系统行为的安全性验证带来了困难。基于形式化方法的仿真和检测分析能够为软件的开发与验证提供严格保障。
　　本文基于形式化的方法，考虑多时钟嵌入式反应系统，针对 SIGNAL模型难以在设计阶段发现系统缺陷的问题，本文提出的方法可以分别从仿真验证和有界性检测两个侧面对系统进行分析，以达到在系统设计的初期，发现系统中存在的危险，并反馈给系统设计者。论文主要研究内容包括：
　　（1）提出基于CCSL时钟限制规约的SINGAL模型的时序行为仿真分析方法。首先，我们将源模型SIGNAL设计的多时钟嵌入式系统模型转换至CCSL时钟模型，利用CCSL的可执行语义，对系统的时序行为进行仿真。此外，还可加入硬件执行平台信息，给出软硬件仿真结果。
　　（2）提出基于标记迁移系统的SIGNAL模型的有界性检测分析方法。设计了SIGNAL模型中操作结构的状态变迁语义系统，基于此系统构建系统行为的状态自动机。针对多时钟系统所关心的有界性问题，我们给出了基于标记迁移系统的有界性检测算法。
　　（3）最后使用本文提出的分析方法对一个自动驾驶系统的控制模块进行案例分析，从SIGNAL系统建模开始，分别从仿真分析和有界性检测两个侧面，找出系统中存在的安全性隐患，说明了本文方法的有效性和可行性。

目录

声明

缩略词

第一章 绪论

1.1 课题研究背景

1.2 研究现状及选题依据

1.3论文组织结构

第二章 同步语言的多时钟系统仿真与检测分析方法概述

2.1 嵌入式反应系统中的时间建模原理

2.2 同步语言SIGNAL模型

2.3 基于形式化的系统分析方法

2.4 面向SIGNAL的多时钟系统行为仿真与检测分析框架

2.5 本章小结

第三章 基于CCSL的系统行为仿真分析方法

3.1 CCSL的时钟模型建模方法

3.2 SIGNAL抽象时钟的提取与转换

3.3 基于CCSL的仿真工具及分析方法

3.4 本章小结

第四章 基于标记迁移系统的有界性检测分析方法

4.1 基于状态语义的标记迁移系统

4.2 SIGNAL时间模型的状态语义

4.3 多时钟系统行为的有界性分析

4.4 本章小结

第五章 案例分析

5.1 系统概述

5.2 系统行为建模

5.3 系统行为的验证分析

5.4 本章小结

第六章 总结与展望

6.1 论文工作总结

6.2 未来工作展望

参考文献

致谢

在学期间的研究成果及发表的学术论文