|
嵌入式技術是計算機發展的趨勢之一，被廣泛應用于工業和軍事領域。SCADE(高安全性的應用程序開發環境)為嵌入式軟件提供了一套基于模型的開發方式。從嵌入式軟件的特點入手，對基于模型的嵌入式系統軟件開發技術進行了深入剖析，并給出了一個基于SCADE的開發實例。 1引言 隨著嵌入式應用技術的發展，嵌入式系統被廣泛應用于人們生活的各個方面。大量功能強大而價格便宜的通用嵌入式硬件隨之出現在市場上。而如何能夠在通用硬件平臺上，高效的開發出滿足安全性與可靠性需要的專用嵌入式軟件成為了制約嵌入式技術應用的瓶頸。在計算機領域，如何為軟件的工業化大生產創造必要的技術條件和設計模式一直是軟件工程研究的首要問題。無論是軟件工程領域出現過的計算機輔助軟件工程的熱潮，還是，基于面向對象技術和組件技術的“裝配重用”軟件思路，都有一些根本性的問題沒有得到解決，因此大規模的“裝配”軟件生產還處在一個理想階段。 隨著研究的深入，用模型化。組件化的方法定義并開發軟件及其系統的思想引起了人們的興趣，也提供了一種新的軟件工業化大生產的可能性。在這方面，嵌入式軟件由于其本身的特殊性走在了通用軟件(PC機用軟件)的前面。 2 SCADE軟件開發環境簡介 SCADE(Safety-Critical Application Develop-ment Environment)高安全性的應用程序開發環境，是法國Esterel Technologies公司研制的一個用于開發達到歐洲航空業DO一178B標準的嵌入式軟件的完整工具包。它針對嵌入式軟件的特點，運用了正確構建(Correct by Construction)的概念，提出了一種基于模型的圖形化開發方式，覆蓋了從需求分析到代碼實現的整個軟件開發流程。 SCADE開發環境提供的一系列開發工具，實現了直觀的圖形化需求建模功能，基于模型的仿真驗證和軟件測試功能，以及基于模型的標準C代碼和開發文檔的自動生成功能。其嚴謹的建模理論和經過高安全性驗證的代碼生成器KCG，保證了軟件需求和代碼產品的高度同步。 SCADE開發環境的出現，使軟件設計工作可以集中在需求建模的層面，為基于模型的軟件開發方法提供了載體。 3基于SCADE的嵌入式軟件開發理論基礎 根據嵌入式系統的特點，SCADE提出了反應式系統。確定性。同步假設。并發性四個關鍵概念，從嵌入式系統的本質特征出發，極大的簡化了系統設計的考慮，為基于模型的開發方式提供了理論基礎。 3.1反應式系統 反應式(Reactive system)系統是指在運行過程中，不停的和外部環境交換信息，以外部環境的輸入信息為主導，進行特定的計算和輸出的嵌人式系統。 反應式系統的工作方式是一個“輸入一計算一輸出”的連續循環過程。反應式系統一般還兼具實時性和周期性，廣泛應用于工業領域的嵌入式系統大都屬于這種系統。反應式系統的工作方式如圖1所示。 反應式系統的概念，把嵌入式系統簡化為一個能不斷接收輸入，并計算輸出的黑盒，為嵌人式系統的需求建模提供了基本模型。 3.2確定性 一個系統，如果使用相同的一組輸入序列，在相同的時間調度下，其反應情況相同，始終產生相同的一組輸出，那么它就是確定的。確定性提高了系統的安全性，是大多數嵌入式軟件的重要需求，在航空航天等高科技領域，這也是一個必要條件。‘確定性的要求降低了系統設計的復雜度，簡化了系統建模和仿真驗證的考慮。SCADE開發環境提供的各種機制確保了系統的確定性，開發者不能引入不確定性。 3.3同步假設 同步假設(synchrony hypothesis)是假設反應式系統的處理速度無限快，即系統在一個可以忽略不計的瞬間響應輸入，并產生輸出。這樣，任何兩次響應之間都不會重疊，每一次輸出都會在下一次輸人前完成。 相對于通用軟件的設計，時間是嵌入式系統設計必須考慮的一個因素，而嵌入式軟件的運行時間又是與硬件環境息息相關的。為了簡化系統設計，SCADE提出了同步假設概念，把物理時間從系統設計中剝離出來。一方面確保了系統的實時性，另一方面也體現了設計的平臺無關性。 同時，為了考慮系統的運算時間問題，SCADE通過基本指令步長將實際的物理時間離散成指令周期時間，從而產生了邏輯時間。這樣，就可以使用邏輯時間來代替物理時間，給出運算時間的參考值。 3.4并發性 并發性概念認為系統所有輸入都是并發的，系統運算模塊按照數據流動執行，而且根據同步假設，所有模塊的運行都是在可以忽略不計的時間內完成的。其中，沒有輸入輸出關系的模塊都是并發執行的，有輸入輸出關系的模塊是按照輸入輸出關系順序執行的。 并發性概念進一步簡化了系統設計的復雜度，也為系統仿真提供了一種簡化的“運行”方式。 4基于SCADE的嵌入式軟件開發關鍵技術 4.1建模機制 基于模型的開發流程，其基礎就是模型描述問題，也就是尋找一種合適的形式來描述系統。 根據嵌入式軟件的特點，可以把其劃分為接口和功能模塊兩部分，功能模塊部分由連續控制部分與狀態邏輯部分組成，其輸人輸出端分別為傳感器和執行器。嵌入式軟件的一般結構如圖2所示。 針對這種劃分，SCADE提供了兩套圖形化的建模機制：數據流圖和有限狀態機。對應嵌入式軟件結構的劃分，數據流圖模型可以用來表示連續控制部分，主要包括傳感器采樣。信號處理。復雜的數學邏輯計算。實現各種算法等功能;有限狀態機模型可以用來表示狀態邏輯部分，主要包括各種系統狀態的遷移和工作模式的變化等功能。 這是一種已被證實為有效并廣泛使用的嵌入式軟件建模方式之一，能夠簡單有效的描述嵌入式系統。 4.2需求建模 一個復雜的嵌入式系統的需求建模過程，是一項系統的設計工作，一般有自頂向下和自底向上兩種設計方式： 自頂向下的設計方式是一種從抽象到具體的過程。它首先需要根據系統的接口需求，建立系統的黑盒模型;然后根據系統的功能需求，對系統進行模塊劃分，并層層細化，直至最低層的功能單元;最后是功能單元的實現工作。 自底向上的設計方式是一種從具體到抽象的過程。它根據系統的功能需求，首先實現的是底層的各個功能模塊，然后根據各模塊之間的接口定義，層層組合，最后形成整個系統模型。 這兩種設計方式在實際使用中各有優劣，可以根據具體需要組合使用。 同時，SCADE的建模方式也可以被認為是一種基于組件的開發方式。一個功能獨立，接口明確構功能算法模型就類似于一個封裝好的組件，可以直接通過接口調用。而SCADE軟件開發環境的高安全性限制和平臺無關性，保證了模型的通用性和重用價值。這樣，基于成熟算法模型的封裝與重用，可以使軟件開發變成模型組件的“裝配”，極大的提高軟件生產效率，也減少了引人錯誤的可能。 4.3模型驗證手段 基于嚴密的建模理論，SCADE提供了一系列基于模型的驗證手段，使模型檢查。系統調試和仿真驗證工作都可以在模型層面上完成。其中主要有以下幾項： (1)靜態檢查，檢查模型設計是否有靜態語意。語法錯誤;(2)模擬仿真，根據算法設計測試用例，通過仿真器模擬接口輸入輸出，直接“執行”模型來實現仿真的功能;(3)形式驗證，根據需求設計的安全特性，通過嘗試在邏輯上尋找反例來檢查模型的安全性;(4)系統原型仿真，通過與其他設計工具的橋接，可以實現系統與模擬外部環境模型的連接運行，方便測試和需求驗證。 對于一個系統模型的驗證工作，一般是按照自底向上的順序進行的。首先要對底層功能模塊進行驗證，由于其結構和接口最為簡單，所以最易于調試。在所有組成模塊都經過充分驗證的基礎上，可以繼續進行上一層模型的驗證工作，并一步步的遞推至最頂層的系統模型。 4.4代碼自動生成 SCADE基于嚴格的數學理論和一套形式化方法，能夠確保其代碼和模型的完全一致，并滿足一系列的安全性特征，是完全面向工程的產品代碼。 SCADE的代碼生成過程提供了多種設置以滿足各種需求，需要根據實際使用需要進行配置，一般情況下其產品可以直接嵌人到產品中去而不需要做任何修改。 5開發實例 依據上述開發技術，實例構建某型號制導炸彈飛控軟件的制導控制模塊，來實踐基于模型的嵌人式軟件開發流程。 5.1開發流程 基于SCADE的嵌入式軟件開發流程，主要工作集中在建模層面，其流程如圖3所示。 5.2需求分析軟件需求規格描述如下： (1)需要實現的功能：此模塊為計算功能模塊，主要根據慣性系下比例導引指令。彈目相對位置和彈體姿態計算彈體需要實現的過載指令。 (2)輸入：慣性系下比例導引指令。彈目相對位置。炸彈姿態。 (3)輸出：彈體導引指令。 5.3需求建模 需求建模可以分為概要設計階段和詳細設計階段。概要設計階段的主要工作是建立系統模型和模塊分層細化;詳細設計階段的主要工作是完成具體模塊設計。 在這個例子中，根據算法所要實現的功能首先定義了整個系統的輸入輸出變量，然后建立系統的黑盒模型，如圖4所示。 下面根據模塊功能，對系統模型進行了進一步劃分，主要分為以下幾個模塊： (1)飛行狀態條件計算模塊Condition.其輸人為彈體姿態和彈目相對位置信息，以及兩個常數參數，輸出為三個飛行狀態變化的條件。 (2)飛行狀態判斷模塊Fly-State.其輸人為三個狀態變化條件變量，輸出為三種狀態標志。 (3)導引指令坐標系轉換模塊Transition.其輸入為彈體姿態和慣性系下比例導引指令，輸出為彈體系下比例導引指令。 (4)過載計算模塊Acceleration.其輸入為三個飛行狀態標志，彈體速度。攻角信息，彈體系下的比例導引指令，以及一個常數參數，輸出為彈體過載指令。 (5)過載限幅模塊Alimit.其輸入為彈體過載指令，輸出為限幅后的彈體過載指令。 其中Condition.Acceleration.Transition和Alimit是功能計算模塊，用數據流圖建模;Fly-State是狀態計算模塊，用有限狀態機建模。系統模型圖如圖5所示。 圖6為飛行狀態計算模塊Fly-State的模型，其中共包含3個狀態，分別為初始狀態(Istate)，轉彎狀態(Tstate)和俯沖狀態(Astate)。根據三個輸入的布爾量條件可以進行狀態變化。其中的狀態變化都是單向不可反復的，變化方向和線條箭頭方向一致。 5.4模型驗證和算法調試 完成模型設計后，需要使用SCADE提供的一系列檢查驗證手段來確保模型的正確性和安全性。對于發現的問題，可以在直觀的圖形化模型上進行模型修改和參數調試。 使用模擬仿真工具，可以通過設計各種測試用例來模擬可能出現的實際情況，對模型進行仿真調試。可以從控制算法角度和軟件工程角度對模型進行優化，以達到滿足設計需求的目的。 5.5代碼集成 在代碼集成階段，根據實際需要，按照效率優先原則進行了配置并自動生成了標準C代碼。然后對使用了SCADE自動生成代碼的軟件進行仿真，其仿真結果與模型仿真的結果一致，滿足設計需求。 6結束語 SCADE軟件開發環境的出現，提供了一種基于模型的高安全性嵌入式軟件解決方案，使嵌入式軟件的開發效率大大提高。同時由于使用了基于模型的設計流程和高度自動化的開發進程，研制工作的重心集中在建模層面，把軟件設計人員從繁復的編碼和驗證工作中解放出來，能夠把大量的精力投入到算法設計和建模工作中，這對于嵌入式軟件的工程開發有著重要的意義。 |
