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

J4 ›› 2015, Vol. 37 ›› Issue (8): 1498-1509.

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

刘雪1,胡军1,2, 黄志球1,马金晶1,程桢1，石娇洁1

(1.南京航空航天大学计算机科学与技术学院，江苏南京 210016;
2.南京大学计算机软件新技术国家重点实验室，江苏南京 210093)

收稿日期:2014-09-01 修回日期:2014-11-25 出版日期:2015-08-25 发布日期:2015-08-25
基金资助:
国家重点基础研究发展计划973计划资助项目（2014CB744904）;国家自然科学基金资助项目(61100034,61170043)；南京航空航天大学青年科技创新基金资助项目（NS2014098）；回国留学人员科研启动基金资助项目(2012)

Research on model driven safety verification
for embedded system designs

LIU Xue1,HU Jun1,2,HUANG Zhiqiu1,MA Jinjing1,CHENG Zhen1,SHI Jiaojie1

(1.School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016；
2.State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210093,China)

Received:2014-09-01 Revised:2014-11-25 Online:2015-08-25 Published:2015-08-25

摘要/Abstract

摘要：

基于模型的嵌入式系统安全性分析与验证方法是近年来在安全攸关系统工程领域中出现的一个重要研究热点。提出一种基于模型驱动架构的面向SysML/MARTE状态机的系统安全性验证方法，具体包括：构建了具备SysML/MARTE扩展语义的状态机元模型，以及安全性建模与分析语言AltaRica的语义模型GTS的元模型；然后建立了从SysML/MARTE状态机模型分别到时间自动机模型以及AltaRica模型的语义映射模型转换规则，并基于AMMA平台和时间自动机验证工具UPPAAL设计实现了对SysML/MARTE状态机的模型转换与系统安全性形式化验证的框架。最后给出了一个飞机着陆控制系统设计模型的安全性验证实例分析。

关键词: 系统安全性分析, 模型驱动工程, SysML/MARTE, 状态机模型, 嵌入式系统

Abstract:

In recent years the model based safety analysis and verification method for embedded systems is an important research hotspot in the field of safety critical systems engineering. We put forward a system safety verification method based on the model driven architecture, which is SysML/MARTE state machine oriented, including the construction of both the state machine metamodel which has SysML/MARTE extension semantics, and the GTS metamodel which is the semantic model of AltaRica (ie.safety modeling and analysis language). We then establish semantic mapping model transformation rules from a SysML/MARTE state machine model to the timed automata model and to the AltaRica model respectively. Thirdly, based on the platform of the AMMA and the timed automata verification tools UPPAAL we design and realize the model transformation of the SysML/MARTE state machine and the framework for system safety formal verification. Finally a safety verification example about aircraft landing control system design model is analyzed.

Key words: system safety analysis；model-driven engineering；SysML/MARTE；state machine model；embedded system

刘雪1,胡军1,2, 黄志球1,马金晶1,程桢1，石娇洁1. 模型驱动的嵌入式系统设计安全性验证方法研究[J]. J4, 2015, 37(8): 1498-1509.

LIU Xue1,HU Jun1,2,HUANG Zhiqiu1,MA Jinjing1,CHENG Zhen1,SHI Jiaojie1. Research on model driven safety verification
for embedded system designs [J]. J4, 2015, 37(8): 1498-1509.

[1]	魏臻1, 2, 原玉磊1, 刘月辉1, 2, 莫家胜1, 2, 扈啸1, 2. 基于FT-X DSP轨迹跟踪的插桩工具设计与实现[J]. 计算机工程与科学, 2025, 47(8): 1343-1353.
[2]	龚锐, 石伟, 刘威, 张剑锋, 王蕾. 基于NAND Flash的CPU安全启动设计与实现[J]. 计算机工程与科学, 2022, 44(6): 971-978.
[3]	陈祥国, 尚凡, 宋君强. 嵌入式系统安全防护方案比较与应用案例分析[J]. 计算机工程与科学, 2022, 44(3): 417-426.
[4]	邢红星, 魏叶华, 乐懿. 硬件成本缩减的异构分布式嵌入式系统调度算法[J]. 计算机工程与科学, 2021, 43(2): 258-265.
[5]	周明进1,卢再奇2. 基于ARM的嵌入式数据录取设备研制[J]. 计算机工程与科学, 2018, 40(9): 1556-1561.
[6]	李攀1,2，田泽1,2，蔡叶芳1,2，张亦姝3，杨海波1,2,霍卫涛1,2,王玉欢1,2. FC-AE-ASM协议优化设计[J]. 计算机工程与科学, 2017, 39(2): 280-284.
[7]	卢灿举，张云峰，高春颖，刘俊. 案例教学下嵌入式系统课程的改革与实践[J]. 计算机工程与科学, 2016, 38(增刊): 248-251.
[8]	陈勇1,袁梦霆2,李清安2. 分区内存体系结构片选指令优化方法[J]. J4, 2016, 38(2): 195-201.
[9]	池鹏可，苏成悦，谢广泉，柳丁. Android平台上的多用户无线投影控制系统设计[J]. J4, 2015, 37(11): 2148-2153.
[10]	武小平. 面向系统综合能力培养的“嵌入式系统”教学探讨[J]. J4, 2014, 36(A2): 238-241.
[11]	王苏峰，陆洪毅，肖侬. 前后台系统渐进式比较教学方法探索[J]. J4, 2014, 36(A1): 100-102.
[12]	宋丽华, 战颖, 简阳, 张鑫磊, 鲍世昆. 基于S3C6410的嵌入式系统休眠与唤醒策略设计与实现[J]. 计算机工程与科学, 2014, 36(5): 790-796.
[13]	吕晖1，丁亚军2，郑方1，吴东1，谢向辉1. 支持跨步访问的嵌入式存储系统[J]. J4, 2014, 36(2): 211-215.
[14]	尹亚明1，刘秋丽2，陈书明1. PCI Express技术在嵌入式MPSoC中的应用[J]. J4, 2013, 35(1): 41-46.
[15]	张其亮1,2,陈永生2,韩斌1. 基于嵌入式系统的全景图像拼接系统设计[J]. J4, 2012, 34(6): 118-122.