面向AltaRica模型的嵌入式系统安全性验证方法

发布时间：2018-05-04 11:25

  本文选题：嵌入式系统 + 安全性验证　； 参考：《计算机科学与探索》2017年01期

【摘要】：嵌入式系统在航空、航天、交通等安全关键领域的使用愈加广泛,Alta Rica是一种描述安全关键系统的建模语言,同时基于Alta Rica模型的安全性分析已成为欧洲的工业标准。提出了一种面向Alta Rica模型的嵌入式系统安全性验证方法,包括:使用Alta Rica语言对嵌入式系统进行建模;给出Alta Rica模型到Promela模型的转换规则;对转换规则进行形式化证明,得到嵌入式系统的Promela模型;使用模型检验工具SPIN进行安全性验证。通过机轮刹车系统中的机轮刹车控制单元进行实例分析,验证了转换规则的正确性和有效性。
[Abstract]:The embedded system has been widely used in aviation, aerospace, traffic and other safety key fields. Alta Rica is a modeling language to describe the security critical system. Meanwhile, the security analysis based on Alta Rica model has become the industrial standard in Europe. A security verification method for embedded system oriented to Alta Rica model is proposed, which includes: modeling embedded system with Alta Rica language, giving conversion rules from Alta Rica model to Promela model, and formalizing the proof of transformation rules. The Promela model of embedded system is obtained, and the model checking tool SPIN is used to verify the security. Through the analysis of wheel brake control unit in wheel brake system, the correctness and validity of the conversion rules are verified.
【作者单位】： 南京航空航天大学计算机科学与技术学院;南京大学计算机软件新技术国家重点实验室;
【基金】：国家重点基础研究发展计划(973计划) 教育部回国留学人员科研启动基金 南京航空航天大学青年科技创新基金~~
【分类号】：TP368.1;TP309

【相似文献】

相关期刊论文 前10条

1 高海芳;王天雷;邱杰;康献民;王大承;;基于OpenGL的3DS模型的导入与控制[J];五邑大学学报(自然科学版);2010年03期

2 刘洁,裴继红,牛俊英;基于标准模型文件的建筑物三维数据模型[J];现代电子技术;2004年04期

3 宋殿宇,韩潮;关于在VRML技术中应用STK模型的研究[J];计算机仿真;2004年10期

4 王德才;孙玉萍;;Direct3D文件模型[J];电脑编程技巧与维护;2007年08期

5 张秀山;钟何平;曹水;吴产乐;;层次约束关系不变的虚拟拆装模型及其VRML实现[J];系统仿真学报;2009年05期

6 陈世福,樊莉萍,徐殿祥,陆庆文;模型描述语言NUMDL的设计与实现[J];软件学报;1992年03期

7 吕文杰,徐邦荃;Matlab在仿真研究中的应用[J];广西师院学报(自然科学版);2000年03期

8 陈东亮;陆达;;关于在OpenGL中装载3ds模型文件的分析[J];福建电脑;2007年05期

9 韩志忠;;强壮的SolidWorks模型文件[J];科技传播;2013年02期

10 余梦洁;;技术离不开市场[J];商用汽车新闻;2013年10期

相关会议论文 前2条

1 唐喜;任雁铭;孟岩;王治民;;IED自动生成IEC61850模型方法探讨[A];中国智能电网学术研讨会论文集[C];2011年

2 魏先福;黄蓓青;;3D打印与印刷[A];2014第十五届中国辐射固化年会论文集[C];2014年

相关重要报纸文章 前2条

1 江苏 佘友军;自动化跑车大制作(上)[N];电脑报;2003年

2 本报记者 陶婷婷;明天一切是否皆可“打印”[N];上海科技报;2013年

相关硕士学位论文 前3条

1 靳松;基于XML的模型文件转换工具的设计与实现[D];东北大学;2013年

2 刘红宇;基于FSM模型的测试方案生成方法研究[D];北京工业大学;2015年

3 赵顺华;基于Web的多领域可视化建模技术研究与实现[D];华中科技大学;2013年

，

本文编号：1842863