形式化需求描述

航空電子領(lǐng)域中基于形式化方法的安全需求描述1.基于形式化方法的安全需求描述意義和準(zhǔn)則在許多領(lǐng)域軟件系統(tǒng)的安全性與可靠性顯得日益重要，尤其在對(duì)安全性和可靠性要求極高的綜合航空電子領(lǐng)域中軟件系統(tǒng)的安全性和可靠性更顯重要。因?yàn)榫C合航空電子系統(tǒng)對(duì)于整個(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）被引入，通過對(duì)需求描述嚴(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)該是對(duì)系統(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)對(duì)于我們達(dá)到我們的目標(biāo)至關(guān)重要。準(zhǔn)則一是需求描述語言只詳細(xì)描述系統(tǒng)的黑盒行為而不包括內(nèi)部的設(shè)計(jì)信息；準(zhǔn)則二是描述語言要讓在保證形式化的準(zhǔn)確性的同時(shí)能夠方便專業(yè)技術(shù)人員和非專業(yè)人員易讀易理解建立起他們對(duì)系統(tǒng)統(tǒng)一的認(rèn)識(shí)；準(zhǔn)則三，就是要具有描述復(fù)雜系統(tǒng)的能力，在這里主要借鑒了Harel所提出的“clustering“的概念，另一方面也用到了Harel“abstraction”思想；其他兩個(gè)標(biāo)準(zhǔn)是最小性和簡潔性。最小性就是需求描述僅包含對(duì)開發(fā)和分析有用的信息。這樣能夠節(jié)省更多的時(shí)間，同時(shí)讓讀者聚焦于對(duì)象的重點(diǎn)上。簡潔性就是盡量避免描述語言讓描述和分析過程復(fù)雜化。語言應(yīng)該簡單易于使用而且能讓描述更可讀和更易查錯(cuò)。2.RSML為了更好地描述需求，滿足上面所提到的符號(hào)語言的要求，在這里我們引入了RSML語言，RSML(需求狀態(tài)機(jī)語言)是源于DavidHarel的Statecharts，是加州大學(xué)的NancyLeveson研究組開發(fā)的一種基于狀態(tài)的描述語言用于對(duì)過程控制系統(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)用于模型固有的平行性或建模對(duì)象的局部。復(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ì)人員和各戶之間對(duì)于需求描述的理解更一致。能夠讓各戶更多地參與到系統(tǒng)開發(fā)中來，從而使開發(fā)的產(chǎn)品更加地符和期望。RSML形式化地描述系統(tǒng)的行為模型，能夠方便地翻譯為定理自動(dòng)證明和模型檢測的輸入形式使模