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