基于SysML活动图的嵌入式实时系统安全性验证方法研究

摘要

嵌入式实时系统在航空航天、核电及交通等安全关键领域中广泛使用，规模变得愈发庞大，体系结构变得更复杂，其故障引起的安全事故有着显著的社会影响，甚至造成灾难性的后果。因此，对嵌入式实时系统设计进行安全性分析与验证成为学术界和工业界亟需攻克的难点。UML(United Modeling Language)常被用来软件设计建模，但在建模能力上不能满足嵌入式实时系统建模需求且缺乏非功能属性建模元素；半形式化的模型在安全性验证上难以被直接使用。
　　针对以上问题，本文提出一种扩展MARTE(Modeling and Analysis of Real-time and Embedded Systems)时钟语义信息到SysML(System Modeling Language)活动图(SysML/MARTE活动图)的嵌入式实时系统安全性验证方法，弥补了UML在针对嵌入式实时系统建模及验证上的不足。主要内容如下：
　　首先，针对嵌入式实时系统，提出使用SysML/MARTE活动图对嵌入式实时系统进行建模，包括采用适合系统建模的SysML活动图构建功能流模型及扩展MARTE时钟语义来构建时间非功能属性。然后，通过基于元模型的模型转换方法将SysML/MARTE活动图转换到时间自动机，包括：(1)针对SysML活动图以及 MARTE时钟等建模元素，分别构建其同构的元模型，并在元模型体系中将 MARTE语义信息添加到 SysML活动图，构建时间自动机的元模型；(2)给出SysML/MARTE活动图和时间自动机的元模型在类型、行为以及时间等元素上的语义映射规则，给出SysML/MARTE活动图嵌套、分支和并发结构到时间自动机的转换规则，将SysML/MARTE活动图模型转换为时间自动机模型；(3)通过语法转换，将时间自动机模型转换为模型检测工具UPPAAL可以直接使用的时间自动机文本。最后，根据嵌入式实时系统设计安全需求，提取CTL(computation temporal logic)规约，在UPPAAL下对转换得到的时间自动机进行安全性分析与验证。

目录

封面

声明

中文摘要

英文摘要

目录

缩略词

第一章 绪论

1.1 课题研究背景及意义

1.2 研究现状及选题依据

1.3 论文组织结构

第二章 面向嵌入式实时系统安全性验证的SysML活动图转换方法

2.1 嵌入式实时系统安全性问题分析

2.2 基于MDA的模型转换方法

2.3 面向嵌入式实时系统安全性验证的SysML活动图转换

2.4 本章小结

第三章 SysML/MARTE活动图元建模与时间自动机元建模

3.1 异构元模型的同构化

3.2 SysML/MARTE活动图元建模

3.3 UPPAAL时间自动机元建模

3.4 本章小结

第四章 SysML/MARTE活动图到时间自动机的转换

4.1 基于AMMA的活动图到时间自动机的元模型转换框架

4.2 SysML/MARTE活动图与时间自动机元模型间语义映射

4.3 SysML/MARTE活动图与时间自动机的结构转换

4.4 时间自动机模型到时间自动机文本的语法转换

4.5 本章小结

第五章 紧急呼叫系统设计安全性验证

5.1 紧急呼叫系统需求描述

5.2 紧急呼叫系统SysML/MARTE活动图建模

5.3 紧急呼叫系统SysML/MARTE活动图到时间自动机转换

5.4 紧急呼叫系统设计的安全性验证与分析

5.5 本章小结

第六章 总结与展望

6.1 论文工作总结

6.2 进一步工作

参考文献

致谢

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