本文選題：嵌入式系統(tǒng) + 安全性驗(yàn)證�。� 參考：《計(jì)算機(jī)科學(xué)與探索》2017年01期

【摘要】：嵌入式系統(tǒng)在航空、航天、交通等安全關(guān)鍵領(lǐng)域的使用愈加廣泛,Alta Rica是一種描述安全關(guān)鍵系統(tǒng)的建模語言,同時(shí)基于Alta Rica模型的安全性分析已成為歐洲的工業(yè)標(biāo)準(zhǔn)。提出了一種面向Alta Rica模型的嵌入式系統(tǒng)安全性驗(yàn)證方法,包括:使用Alta Rica語言對(duì)嵌入式系統(tǒng)進(jìn)行建模;給出Alta Rica模型到Promela模型的轉(zhuǎn)換規(guī)則;對(duì)轉(zhuǎn)換規(guī)則進(jìn)行形式化證明,得到嵌入式系統(tǒng)的Promela模型;使用模型檢驗(yàn)工具SPIN進(jìn)行安全性驗(yàn)證。通過機(jī)輪剎車系統(tǒng)中的機(jī)輪剎車控制單元進(jìn)行實(shí)例分析,驗(yàn)證了轉(zhuǎn)換規(guī)則的正確性和有效性。
[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.
【作者單位】： 南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院;南京大學(xué)計(jì)算機(jī)軟件新技術(shù)國家重點(diǎn)實(shí)驗(yàn)室;
【基金】：國家重點(diǎn)基礎(chǔ)研究發(fā)展計(jì)劃(973計(jì)劃) 教育部回國留學(xué)人員科研啟動(dòng)基金 南京航空航天大學(xué)青年科技創(chuàng)新基金~~
【分類號(hào)】：TP368.1;TP309

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 高海芳;王天雷;邱杰;康獻(xiàn)民;王大承;;基于OpenGL的3DS模型的導(dǎo)入與控制[J];五邑大學(xué)學(xué)報(bào)(自然科學(xué)版);2010年03期

2 劉潔,裴繼紅,牛俊英;基于標(biāo)準(zhǔn)模型文件的建筑物三維數(shù)據(jù)模型[J];現(xiàn)代電子技術(shù);2004年04期

3 宋殿宇,韓潮;關(guān)于在VRML技術(shù)中應(yīng)用STK模型的研究[J];計(jì)算機(jī)仿真;2004年10期

4 王德才;孫玉萍;;Direct3D文件模型[J];電腦編程技巧與維護(hù);2007年08期

5 張秀山;鐘何平;曹水;吳產(chǎn)樂;;層次約束關(guān)系不變的虛擬拆裝模型及其VRML實(shí)現(xiàn)[J];系統(tǒng)仿真學(xué)報(bào);2009年05期

6 陳世福,樊莉萍,徐殿祥,陸慶文;模型描述語言NUMDL的設(shè)計(jì)與實(shí)現(xiàn)[J];軟件學(xué)報(bào);1992年03期

7 呂文杰,徐邦荃;Matlab在仿真研究中的應(yīng)用[J];廣西師院學(xué)報(bào)(自然科學(xué)版);2000年03期

8 陳東亮;陸達(dá);;關(guān)于在OpenGL中裝載3ds模型文件的分析[J];福建電腦;2007年05期

9 韓志忠;;強(qiáng)壯的SolidWorks模型文件[J];科技傳播;2013年02期

10 余夢(mèng)潔;;技術(shù)離不開市場(chǎng)[J];商用汽車新聞;2013年10期

相關(guān)會(huì)議論文 前2條

1 唐喜;任雁銘;孟巖;王治民;;IED自動(dòng)生成IEC61850模型方法探討[A];中國智能電網(wǎng)學(xué)術(shù)研討會(huì)論文集[C];2011年

2 魏先福;黃蓓青;;3D打印與印刷[A];2014第十五屆中國輻射固化年會(huì)論文集[C];2014年

相關(guān)重要報(bào)紙文章 前2條

1 江蘇 佘友軍;自動(dòng)化跑車大制作(上)[N];電腦報(bào);2003年

2 本報(bào)記者 陶婷婷;明天一切是否皆可“打印”[N];上�？萍紙�(bào);2013年

相關(guān)碩士學(xué)位論文 前3條

1 靳松;基于XML的模型文件轉(zhuǎn)換工具的設(shè)計(jì)與實(shí)現(xiàn)[D];東北大學(xué);2013年

2 劉紅宇;基于FSM模型的測(cè)試方案生成方法研究[D];北京工業(yè)大學(xué);2015年

3 趙順華;基于Web的多領(lǐng)域可視化建模技術(shù)研究與實(shí)現(xiàn)[D];華中科技大學(xué);2013年

，

本文編號(hào)：1842863