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