形式化需求描述

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