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