模型驱动的嵌入式系统设计安全性验证方法研究

摘要

近年来在安全关键应用领域中（如：航空、交通、核电站等）嵌入式系统及软件的规模增大以及系统复杂度的迅速增加带来了嵌入式系统及软件安全性保障方面的重要挑战；与此同时，模型驱动的系统／软件开发技术在安全关键工程领域中也开始得到广泛的关注和应用。传统的统一建模语言（如：UML，SysML等）已经越来越多的应用于系统及软件建模，但在面向安全关键领域时这些建模语言及方法目前还存在一些问题，如：本身缺乏对实时嵌入式系统的非功能行为描述的元素及机制（包括：对时间、资源、概率的有效建模等）；建模语言尚缺少模型语义的精确定义，这对使用软件模型展开面向安全性的形式化验证与分析时带来困难等等。
　　本文工作主要是对模型驱动架构（MDA）下的嵌入式系统模型的安全性分析问题展开了研究，探索了基于模型转换的SysML/MARTE状态机、AltaRica模型以及时间自动机的UPPAAL模型的安全性分析与验证方法，具体包括以下几个部分：
　　(1)研究了基于SysML/MARTE的复杂嵌入式系统设计建模问题；系统建模语言 SysML是目前系统工程应用开发的标准建模语言，MARTE主要从时间约束、资源分配等非功能属性方面来对嵌入式系统建模与分析。本文以 SysML状态机模型作为一个典型的研究对象，结合MARTE中包括时间、概率等信息在内的非功能资源方面的语义扩展，用以对复杂嵌入式系统的行为进行建模。
　　(2)对MDA的一个核心问题：模型转换展开了基于AMMA平台的异构模型间转换的方法，包括：建立SysML/MARTE状态机元模型、AltaRica元模型和时间自动机元模型，以及模型之间的语义映射关系，然后基于AMMA平台的模型转换语言ATL构造模型转换规则，为在模型驱动架构下实现从SysML/MARTE状态机模型分别到AltaRica模型、时间自动机模型的转换建立了基础。
　　(3)研究了SysML/MARTE状态机模型在时间属性方面的安全性分析与验证方法；通过元模型的语义映射关系，将SysML/MARTE状态机模型转换到时间自动机模型，所需要满足的时序逻辑公式从AltaRica模型中获取，然后采用分析工具UPPAAL进行安全性的分析与验证。
　　(4)研究了从系统概率属性方面面向 SysML/MARTE状态机模型的安全性验证问题；包括：将SysML/MARTE状态机模型转换到AltaRica模型，生成故障树模型，并将得到的故障树作为故障树分析工具XFTA的输入，进而展开对系统安全分析性和验证。
　　(5)设计了一个基于模型的对嵌入式系统设计分析的框架，并分别通过飞机着陆实例建模以及ARP4751中的刹车控制系统等进行了模型建立并分析验证的实例分析。

目录

封面

声明

中文摘要

英文摘要

目录

缩略词

第一章 绪论

1.1课题研究背景及意义

1.2 当前研究现状

1.3论文的研究内容

第二章 模型驱动架构与系统安全性分析概述

2.1模型驱动架构(MDA)

2.2基于MDA的模型转换

2.3基于模型的系统安全性分析

2.4本章小结

第三章 SysML/MARTE状态机和AltaRica元模型的构造

3.1元模型间同构化

3.2 SysML/MARTE状态机的元模型构造

3.3 AltaRica元模型的构造

3.4时间自动机元模型的构造

3.5本章小结

第四章 SysML/MARTE状态机模型到AltaRica模型的转换

4.1模型转换内容

4.2元模型间的映射关系

4.3本章小结

第五章 基于模型的系统设计安全性验证框架与实例分析

5.1基于模型的系统设计安全性验证框架

5.2飞机着陆系统实例建模分析

5.3机轮刹车系统实例建模分析

5.4本章小结

第六章 总结与展望

6.1总结

6.2展望

参考文献

致谢

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