形式化需求描述_第1頁
形式化需求描述_第2頁
形式化需求描述_第3頁
形式化需求描述_第4頁
全文預(yù)覽已結(jié)束

下載本文檔

版權(quán)說明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權(quán),請進(jìn)行舉報(bào)或認(rèn)領(lǐng)

文檔簡介

航空電子領(lǐng)域中基于形式化方法的安全需求描述1.基于形式化方法的安全需求描述意義和準(zhǔn)則在許多領(lǐng)域軟件系統(tǒng)的安全性與可靠性顯得日益重要,尤其在對安全性和可靠性要求極高的綜合航空電子領(lǐng)域中軟件系統(tǒng)的安全性和可靠性更顯重要。因?yàn)榫C合航空電子系統(tǒng)對于整個(gè)飛機(jī)的安全性起著至關(guān)重要的作用。然而,伴隨著航電系統(tǒng)日益增長的復(fù)雜性和系統(tǒng)集成的問題依然會(huì)增加潛在的錯(cuò)誤并可能直接影響到飛機(jī)的安全性和可靠性。傳統(tǒng)的軟件工程方法已經(jīng)很難滿足這樣復(fù)雜和安全性要求極高的需求,這迫切需要新的方法來設(shè)計(jì)開發(fā)安全性更高,資金時(shí)間投入更少的系統(tǒng),為了解決這些實(shí)際問題,基于模型的開發(fā)方法(MBD)被引入,通過對需求描述嚴(yán)格的形式定義,可執(zhí)行的原型設(shè)計(jì),定理證明,模型檢測,和高質(zhì)量代碼的自動(dòng)生成等形式化技術(shù)大大提升了系統(tǒng)的安全性和可靠性,同時(shí)也大大節(jié)省了時(shí)間和成本。大多軟件開發(fā)的錯(cuò)誤源于需求分析階段的邏輯錯(cuò)誤。這些邏輯錯(cuò)誤會(huì)傳遞到軟件開發(fā)的后續(xù)階段,大量的重復(fù)工作花費(fèi)在修補(bǔ)由于需求階段的邏輯錯(cuò)誤而導(dǎo)致的系統(tǒng)錯(cuò)誤。而且,需求錯(cuò)誤往往是相當(dāng)嚴(yán)重的錯(cuò)誤。需求階段的錯(cuò)誤比設(shè)計(jì)或?qū)崿F(xiàn)階段所引入的錯(cuò)誤更加影響系統(tǒng)的安全性。發(fā)現(xiàn)錯(cuò)誤的一個(gè)有效途徑就是創(chuàng)建一個(gè)系統(tǒng)外部可見行為的精確且可執(zhí)行的系統(tǒng)模型。為了建立可讀的且數(shù)學(xué)形式上的精確的系統(tǒng)功能行為模型,已經(jīng)有多種符號(hào)語言被開發(fā)出來。比較出名的有SCR,RSML,SpecTRM,和Statechartso基于這些符號(hào)語言來創(chuàng)建模型能夠發(fā)現(xiàn)大量系統(tǒng)描述中的錯(cuò)誤。而且能夠作為與用戶交互的實(shí)模型,并能夠類仿真的形式向客戶執(zhí)行。最好的情形就是經(jīng)過精心設(shè)計(jì)的符號(hào)語言能夠支持系統(tǒng)模型的自動(dòng)形式化安全分析(如圖1.1)。它使得通過一致性和完備性檢查來發(fā)現(xiàn)錯(cuò)誤成為可能,同時(shí)有能力來檢查應(yīng)用程序建模的一些性能描述。總之,創(chuàng)建系統(tǒng)行為的精確模型不僅僅使得能夠在系統(tǒng)生命期盡早地發(fā)現(xiàn)錯(cuò)誤,并及時(shí)地解決,還能夠提升后續(xù)的系統(tǒng)設(shè)計(jì),編碼,驗(yàn)證,測試的質(zhì)量。FormalModelPerformAnalysisFormalModelPerformAnalysis圖1.1基于形式化方法的安全性分析系統(tǒng)需求描述作為系統(tǒng)開發(fā)的藍(lán)圖,它應(yīng)該是對系統(tǒng)期望行為的完備的,一致性的,精確的描述。否則將會(huì)把不安全因素帶進(jìn)后續(xù)的設(shè)計(jì)、編碼、測試等環(huán)節(jié),將嚴(yán)重影響系統(tǒng)的安全性能同時(shí)也增加更多的開發(fā)代價(jià)。所以提供方法和技術(shù)使盡可能早地排除與需求相關(guān)的錯(cuò)誤顯得非常重要。為了分析和發(fā)現(xiàn)需求描述的錯(cuò)誤,描述語言所應(yīng)具有的一些標(biāo)準(zhǔn)對于我們達(dá)到我們的目標(biāo)至關(guān)重要。準(zhǔn)則一是需求描述語言只詳細(xì)描述系統(tǒng)的黑盒行為而不包括內(nèi)部的設(shè)計(jì)信息;準(zhǔn)則二是描述語言要讓在保證形式化的準(zhǔn)確性的同時(shí)能夠方便專業(yè)技術(shù)人員和非專業(yè)人員易讀易理解建立起他們對系統(tǒng)統(tǒng)一的認(rèn)識(shí);準(zhǔn)則三,就是要具有描述復(fù)雜系統(tǒng)的能力,在這里主要借鑒了Harel所提出的“clustering“的概念,另一方面也用到了Harel“abstraction”思想;其他兩個(gè)標(biāo)準(zhǔn)是最小性和簡潔性。最小性就是需求描述僅包含對開發(fā)和分析有用的信息。這樣能夠節(jié)省更多的時(shí)間,同時(shí)讓讀者聚焦于對象的重點(diǎn)上。簡潔性就是盡量避免描述語言讓描述和分析過程復(fù)雜化。語言應(yīng)該簡單易于使用而且能讓描述更可讀和更易查錯(cuò)。2.RSML為了更好地描述需求,滿足上面所提到的符號(hào)語言的要求,在這里我們引入了RSML語言,RSML(需求狀態(tài)機(jī)語言)是源于DavidHarel的Statecharts,是加州大學(xué)的NancyLeveson研究組開發(fā)的一種基于狀態(tài)的描述語言用于對過程控制系統(tǒng)的行為建模。RSML的主要設(shè)計(jì)目標(biāo)就是讓非計(jì)算機(jī)專業(yè)人員比如最終用戶,應(yīng)用工程師,管理者,以及來自監(jiān)管機(jī)構(gòu)的代表都能易讀易理解用RSML語言寫的需求描述。一個(gè)RSML描述由變量,狀態(tài),轉(zhuǎn)移,功能函數(shù),宏,常量,和接口組成。需求描述中的變量用于存儲(chǔ)外部傳感器的輸入值,也用于暫存系統(tǒng)的輸出值。Statecharts以分層的形式組織狀態(tài)。RSML包括三種不同類型的狀態(tài):復(fù)合狀態(tài),平行狀態(tài),和原子狀態(tài)。原子狀態(tài)等同于傳統(tǒng)有限狀態(tài)機(jī)中的狀態(tài)。平行狀態(tài)用于模型固有的平行性或建模對象的局部。復(fù)合狀態(tài)(superState)一方面用于隱藏狀態(tài)機(jī)的局部細(xì)節(jié)來使得所得模型更易理解,另一方面封裝狀態(tài)機(jī)的確切行為。圖2.1是ASW需求描述中狀態(tài)的分層建模的例子,它包含以上所說的三種不同狀態(tài)類型。aswRe<iModel圖2.1High-levelASWModelRSML中的狀態(tài)轉(zhuǎn)移控制著一個(gè)狀態(tài)到其他狀態(tài)的轉(zhuǎn)移。狀態(tài)轉(zhuǎn)移由一個(gè)原狀態(tài),一個(gè)目的狀態(tài),一個(gè)觸發(fā)事件,一個(gè)監(jiān)督條件和一組動(dòng)作事件組成。為了執(zhí)行一次RSML狀態(tài)轉(zhuǎn)移,必須有下列情況為真:(1)原狀態(tài)當(dāng)前處于激活狀態(tài),(2)觸發(fā)事件出現(xiàn)在原狀態(tài)處于激活態(tài),(3)當(dāng)觸發(fā)事件發(fā)生時(shí)監(jiān)督條件必須為真。當(dāng)所有這些情況都滿足時(shí),目的狀態(tài)將成為激活狀態(tài),而原狀態(tài)將變?yōu)榉羌せ顮顟B(tài),同時(shí)產(chǎn)生行為事件。監(jiān)督條件簡單地以說就是在不同的狀態(tài)和變量之間的一種謂詞邏輯表達(dá)式,用命題邏輯符號(hào)語言傳統(tǒng)地去定義這些條件通常會(huì)陷入復(fù)雜的表達(dá)式并且變得不可讀。為了克服這一問題,在RSML中使用了析取范式(DNF)的一種表格表示,這種表格被稱為AND/OR表。AND/OR表格的最左一列列出了邏輯短語。其它的列是這些邏輯短語的連接,并且列出了表達(dá)式的邏輯真值。并規(guī)定只要有某一列的值為真則整個(gè)表的值就為真。而每列的真值為真當(dāng)且僅當(dāng)此列的真值與它們所關(guān)聯(lián)的邏輯短語的真值都一致。AND/OR表2.1是謂詞短語((Expression-1AnExpression-2)V(Expression-1八Expression-3))的邏輯等價(jià)描述。OR為了進(jìn)一步增加需求描述的可讀性,Irvine研究組在RSML中引進(jìn)了許多其它的語法結(jié)構(gòu),例如,允許謂詞中的表達(dá)式定義為形如case語句的函數(shù),允許宏定義經(jīng)常使用的且相同的條件。圖2.2,“BelowThreshold”和“AltitudeQualityOK”都是宏。宏BelowThreshold的定義在圖2.3中給出。Transition(S):Transition(S):Above一->BelowLocation:AltitudeStatusMacro:BelowThresholdDefinition:AltitudegAltitudeThreshold||T|NBelowThreshold。TDAltitudcQualityOK()TTriggerEvent:AltReceivedEventCondition:OutputAction:AltStatusEvaluatedEvent圖2.2ATransitionandMacrofromtheASWrequirementsRSML支持系統(tǒng)級(jí)組件間通信的嚴(yán)格的描述和分析,系統(tǒng)組件間的的聯(lián)系通過通道的形式。每個(gè)組件可能有多個(gè)輸入/輸出通道。通信的發(fā)生通過消息機(jī)制來驅(qū)動(dòng)。3.RSML用于需求形式化描述的好處RSML語言易讀易理解,能夠使設(shè)計(jì)人員和各戶之間對于需求描述的理解更一致。能夠讓各戶更多地參與到系統(tǒng)開發(fā)中來,從而使開發(fā)的產(chǎn)品更加地符和期望。RSML形式化地描述系統(tǒng)的行為模型,能夠方便地翻譯為定理自動(dòng)證明和模型檢測的輸入形式使模

溫馨提示

  • 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
  • 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
  • 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內(nèi)容里面會(huì)有圖紙預(yù)覽,若沒有圖紙預(yù)覽就沒有圖紙。
  • 4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
  • 5. 人人文庫網(wǎng)僅提供信息存儲(chǔ)空間,僅對用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對任何下載內(nèi)容負(fù)責(zé)。
  • 6. 下載文件中如有侵權(quán)或不適當(dāng)內(nèi)容,請與我們聯(lián)系,我們立即糾正。
  • 7. 本站不保證下載資源的準(zhǔn)確性、安全性和完整性, 同時(shí)也不承擔(dān)用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。

最新文檔

評論

0/150

提交評論