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

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

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

【參考文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

本文編號(hào)：2674615