【摘要】：使用傳統(tǒng)的開發(fā)方法對安全關(guān)鍵系統(tǒng)進行開發(fā)時,早期系統(tǒng)設(shè)計階段的錯誤往往到開發(fā)后期的測試階段才能檢測出來,重新對系統(tǒng)結(jié)構(gòu)進行錯誤修改會造成大量的時間和人力耗費。并且由于測試并不能保證系統(tǒng)中不存在錯誤,無法滿足安全關(guān)鍵系統(tǒng)對安全性和可靠性的要求。與之對應(yīng)的是,形式化開發(fā)方法使用精確的數(shù)學(xué)語言根據(jù)系統(tǒng)需求進行描述,消除自然語言帶來的二義性,同時,形式化方法根據(jù)系統(tǒng)需求進行建模后,使用數(shù)學(xué)證明的方式來驗證模型的正確性,能夠在開發(fā)早期發(fā)現(xiàn)需求與設(shè)計上存在的錯誤,避免了后期的測試所帶來的時間和成本消耗。然而,由于形式化方法在使用時需要將自然語言描述的需求文本轉(zhuǎn)換成精確的形式化規(guī)約,對開發(fā)人員的專業(yè)知識背景要求很高。因此一般需要使用需求工程中的需求分析方法將系統(tǒng)需求進行分解,轉(zhuǎn)換成半形式化的中間語言,減輕前期獲取需求規(guī)約的困難。本文使用SysML/KAOS方法在前期對需求進行處理,將文本需求轉(zhuǎn)換成使用特定標記語言表示的目標(goal)中,然后根據(jù)目標模型中的精化分解關(guān)系將復(fù)雜需求進行分解,建立需求的層次結(jié)構(gòu)。同時,建立從SysML/KAOS方法到形式化建模語言Event-B的關(guān)系映射,將目標模型中的目標和需求精化關(guān)系轉(zhuǎn)換到Event-B的模型元素中,然后通過Event-B中的驗證機制對轉(zhuǎn)換的正確性和一致性進行驗證。本文的主要研究工作如下:(1)將SysML/KAOS模型中表示功能需求的實現(xiàn)目標(Achieve goal)和表示安全需求的維持目標(Maintain goal)轉(zhuǎn)換到Event-B模型中的對應(yīng)元素;(2)將目標模型中的三種需求精化模式對應(yīng)轉(zhuǎn)換到Event-B的模型精化關(guān)系中,同時給出了轉(zhuǎn)換一致性和正確性證明;(3)對于轉(zhuǎn)換中存在的活性屬性丟失問題進行討論,給出了目標模型中活性屬性在Event-B建模過程中的表達方式,然后針模型中已經(jīng)添加的活性屬性可能在精化過程中丟失的問題進行研究,給出的精化中活性屬性保持的方法和相關(guān)證明。
【圖文】：

圖 3.14 Event-B 中模型 M2精化后的事件使用 ProB 工具對模型 M2進行驗證與模擬的結(jié)果如圖 3.15，可以看到，在該工具驗證下的不變式和事件的正確性能夠完整的保持

持活性屬性保持的安全關(guān)鍵系統(tǒng)建模方oor_open = Fift_move =TLift_moveDoor_openDoor_openLift_moveColse_doorLift_stopLift_start圖 5.6 模型 M1 的狀態(tài)變遷圖了表示安全性屬性的不變式@inv1，則中的事件生成證明義務(wù)，，然后通過證明結(jié)果如下：
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2018
【分類號】：TP311.5

【參考文獻】

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

1 李婉璐;;軟件工程中的形式化方法研究綜述[J];數(shù)字技術(shù)與應(yīng)用;2015年10期

2 楊啟亮;邢建春;王平;;安全關(guān)鍵系統(tǒng)及其軟件方法[J];計算機應(yīng)用與軟件;2011年02期

3 祝義;黃志球;曹子寧;周航;劉亞萍;;一種基于形式化規(guī)約生成軟件體系結(jié)構(gòu)模型的方法[J];軟件學(xué)報;2010年11期

4 楊仕平;熊光澤;桑楠;;安全關(guān)鍵系統(tǒng)高可信保障技術(shù)的研究[J];計算機科學(xué);2003年05期

5 王繼成,高珍;軟件需求分析的研究[J];計算機工程與設(shè)計;2002年08期

6 黎忠文,熊光澤;形式化方法與安全關(guān)鍵系統(tǒng)[J];計算機應(yīng)用;2000年09期

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

1 蘇雯;基于Event-B的混合系統(tǒng)形式化：理論與實踐[D];華東師范大學(xué);2013年

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

1 葉水琴;基于目標模型的橫切關(guān)注點識別方法研究[D];武漢工程大學(xué);2015年

2 彭小玲;軟件非功能需求層次模型研究[D];中南大學(xué);2011年

3 李平;面向目標建模的MDA模型轉(zhuǎn)換研究與實現(xiàn)[D];哈爾濱工程大學(xué);2011年

4 汪光明;FKAOS方法中Agent實體優(yōu)化的研究和應(yīng)用[D];合肥工業(yè)大學(xué);2008年

本文編號：2674615