基于SCADE的嵌入式軟件開發(fā)方法研究
要素,軟件的設(shè)計(jì)模式直接決定了軟件的安全和可靠性。本文研究了高安全性應(yīng)用程序開發(fā)環(huán)境 -SCADE的特點(diǎn)和應(yīng)用,介紹了一種基于該開發(fā)環(huán)境的軟件開發(fā)平臺(tái)方案。大量的工程的應(yīng)用也表明該方案有助于提高嵌入式軟件的開發(fā)質(zhì)量,縮短研制周期,滿足軟件研制需求。
本文引用地址:http://m.butianyuan.cn/article/201609/303507.htm關(guān)鍵詞:SCADE;嵌入式軟件;建模;模擬仿真;形式驗(yàn)證
軟件的安全和可靠性是衡量軟件質(zhì)量最重要的指標(biāo)和軟件開發(fā)的最終目標(biāo)。較之普通軟件領(lǐng)域,在高安全性的嵌入式開發(fā)領(lǐng)域如軌道交通,航空,國防等,軟件因其任務(wù)特點(diǎn),更需要保證高可靠性。然而,何謂“高可靠性軟件”、如何開發(fā)“高可靠性軟件”一直是困擾系統(tǒng)開發(fā)人員的“瓶頸”問題。誠然,軟件的設(shè)計(jì)模式直接決定了軟件的安全和可靠性。文中介紹了一種基于模型的可靠性軟件開發(fā)平臺(tái)方案。大量的工程應(yīng)用也表明該方法是切實(shí)有效的。
1 嵌入式軟件開發(fā)現(xiàn)狀
何謂“高可靠性軟件”?1983年美國IEEE計(jì)算機(jī)學(xué)會(huì)軟件工程技術(shù)委員會(huì)將軟件可靠性定義如下:在規(guī)定的條件下,在規(guī)定的時(shí)間內(nèi),軟件不引起系統(tǒng)失效的概率。在規(guī)定的時(shí)間周期內(nèi)和條件下,程序執(zhí)行要求的功能的能力。這個(gè)標(biāo)準(zhǔn)隨后經(jīng)美國標(biāo)準(zhǔn)化研究院批準(zhǔn)作為美國的國家標(biāo)準(zhǔn),1989年我國國標(biāo)GB/T- 11457采用了這個(gè)定義。
那么,如何開發(fā)“高可靠性軟件”?軟件可靠性工程的任務(wù)是力爭(zhēng)在軟件生命周期過程中最大限度地減少軟件產(chǎn)品中的缺陷。而減少軟件缺陷必須在全面周密的考慮系統(tǒng)在各個(gè)不同階段、不同狀態(tài)下,保證軟件和需求的一致性。
1.1 現(xiàn)有的軟件開發(fā)方法
目前,大多數(shù)嵌入式軟件項(xiàng)目都采用“以手工編碼和以代碼為中心”瀑布模型作為規(guī)范化開發(fā)的基礎(chǔ)。該種開發(fā)方式以代碼開發(fā)為中心,需求分析、軟件設(shè)計(jì)為軟件編碼做準(zhǔn)備,代碼編寫完成后進(jìn)行單元測(cè)試。長(zhǎng)期以來,代碼編寫一直是開發(fā)過程的主要階段,占用了大量的時(shí)間和人力。隨著人們對(duì)軟件質(zhì)量的重視,單元測(cè)試在開發(fā)過程中的地位日益重要,在目前的開發(fā)流程中,越來越多的力量投入到代碼的單元測(cè)試中。
基于代碼開發(fā)方式的缺點(diǎn)非常明顯:
1)開發(fā)效率低下
由于代碼的抽象程度高,不直觀,與軟件需求完全脫節(jié),因此開發(fā)人員不得不花大量的時(shí)間在技術(shù)細(xì)節(jié)上,代碼的修改也很耗時(shí)。
2)質(zhì)量沒有保證
由于軟件代碼由程序員手工編寫,程序員的能力、態(tài)度及狀態(tài)制約了軟件的質(zhì)量。且隨著軟件規(guī)模、復(fù)雜度的不斷增加,團(tuán)隊(duì)開發(fā)情況的出現(xiàn),代碼集成也變得越來越難。
出現(xiàn)這些缺點(diǎn)的主要原因在于,在基于代碼開發(fā)方式下,開發(fā)工作的早期(需求分析、軟件設(shè)計(jì))完全依賴于人工工作,其成果以有歧義的自然語言或圖表方式描述,無法進(jìn)行有效的交流和驗(yàn)證,從而成為錯(cuò)誤引入的重災(zāi)區(qū);而當(dāng)具有動(dòng)態(tài)行為的代碼出現(xiàn)后,對(duì)代碼的測(cè)試是一種事后監(jiān)督的、費(fèi)時(shí)費(fèi)力的做法,只能盡可能地發(fā)現(xiàn)錯(cuò)誤,而無法有效地避免或者是排除錯(cuò)誤。
1.2 “基于模型”的開發(fā)方法
隨著人們對(duì)軟件認(rèn)識(shí)的逐漸加深及實(shí)踐中的探索,模型取代代碼成為了軟件開發(fā)流程的中心。直觀的模型符號(hào)被用于需求分析及以軟件設(shè)計(jì)過程,表達(dá)分析人員對(duì)需求的理解及細(xì)化。由于模型遠(yuǎn)比程序語言的抽象程度低,更易于理解和交流,減少了需求分析和軟件設(shè)計(jì)過程中錯(cuò)誤引入的機(jī)率,尤為重要的是,模型還可用于模擬仿真,表達(dá)其動(dòng)態(tài)特性,從而使開發(fā)人員在開發(fā)的早期能確定性地發(fā)現(xiàn)并排除錯(cuò)誤。
一般來說,基于模型的開發(fā)方式具有以下特征:
1)形式化的圖形符號(hào)
直觀易懂的圖形符號(hào)是模型的主要特征,也是模型優(yōu)于代碼的主要原因。借助于圖形化的符號(hào)組成的模型,閱讀者不僅能快速獲取模型所表達(dá)的含義,而且不會(huì)因知識(shí)背景的不同產(chǎn)生歧義。
2)模型可運(yùn)行
可運(yùn)行的模型為開發(fā)人員了解模型的動(dòng)態(tài)行為提供了方便,可以驗(yàn)證設(shè)計(jì)與需求是否一致。
2 “基于模型”的開發(fā)工具
2.1 什么是“基于模型”的開發(fā)工具?
所謂“基于模型”,是以一種形式化的模型方式描述一個(gè)系統(tǒng)或是一個(gè)子系統(tǒng)。一個(gè)模型可以是數(shù)學(xué)意義上的,由一系列關(guān)于系統(tǒng)的聲明構(gòu)成;也可以是構(gòu)架意義上的(又稱作可執(zhí)行的),用來描述一個(gè)系統(tǒng)對(duì)系統(tǒng)外激勵(lì)的響應(yīng)情況。
隨著計(jì)算機(jī)技術(shù)的迅猛發(fā)展和軟件工程自動(dòng)化的不斷發(fā)展,“基于模型”的開發(fā)工具不斷涌現(xiàn),這類工具的普遍特點(diǎn)是通過形式化的建模方式實(shí)現(xiàn)需求、模型可以直接進(jìn)行模擬、并且可以直接將模型轉(zhuǎn)化為源代碼。
2.2 “基于模型”開發(fā)工具的比較
基于模型的開發(fā)工具有很多,在嵌入式軟件開發(fā)領(lǐng)域應(yīng)用比較廣泛的主要有基于UML的建模工具,或是結(jié)構(gòu)化的設(shè)計(jì)工具(SCADE、SIMULINK等)。
1)基于UML的設(shè)計(jì)工具:關(guān)注于高層的功能劃分、結(jié)構(gòu)分解、行為規(guī)范和需求分析,適合于系統(tǒng)建模;它從軟件工程的角度對(duì)開發(fā)流程進(jìn)行規(guī)范,但很少考慮高可靠性嵌入式軟件開發(fā)的特點(diǎn),軟件工程自動(dòng)化程度較低,生成的只是一個(gè)代碼框架,需要對(duì)它生成的代碼做大量的修改和補(bǔ)充之后才能使用。
2)Simulink:面向仿真,仿真功能比較強(qiáng)大,支持對(duì)硬件和外界環(huán)境的模擬,可以進(jìn)行全局的仿真和調(diào)試;但是由于底層缺乏數(shù)學(xué)理論的支撐,無法保證模型作為需求描述的無歧義性;從生成代碼的角度來說,它生成的代碼也需要做大量的修改和補(bǔ)充之后才能使用,而這種做法在增加工作量的同時(shí),和基于UML的設(shè)計(jì)工具一樣,帶來了一個(gè)潛在的很復(fù)雜的開發(fā)流程管理和質(zhì)量認(rèn)證上的問題。
3)SCADE(Safety—Critical Application Development Environment)是一套基于模型的、面向高可靠性軟件而設(shè)計(jì)的開發(fā)環(huán)境,具有嚴(yán)格的理論基礎(chǔ)支持,充分考慮了高可靠性軟件開發(fā)中的質(zhì)量、安全特性、開發(fā)周期、認(rèn)證等各方面的問題,國內(nèi)外高安全性嵌入式領(lǐng)域應(yīng)用經(jīng)驗(yàn)表明,它非常適合用于開發(fā)高可靠性軟件。
3 基于SCADE的軟件設(shè)計(jì)方法
3.1 SCADE簡(jiǎn)介
SCADE (Safety—Critical Application Development Environment)是一套高安全性嵌入式軟件開發(fā)環(huán)境,運(yùn)用Correct By Construction的設(shè)計(jì)理念,能夠從精確的需求規(guī)范自動(dòng)生成嵌入式源代碼,實(shí)現(xiàn)了開發(fā)流程的高度自動(dòng)化。它涵蓋了嵌入式軟件開發(fā)的整個(gè)流程:需求管理、需求建模、模型檢查、模型仿真、模型覆蓋率分析、形式驗(yàn)證、代碼生成、文檔生成等等。SCADE適用于不同軟、硬件平臺(tái),是一套通用的嵌入式軟件開發(fā)平臺(tái)。
3.2 基于SCADE軟件設(shè)計(jì)方法
在現(xiàn)有的瀑布式的開發(fā)流程中,軟件需求、概要設(shè)計(jì)、詳細(xì)設(shè)計(jì)都是為了編碼;單元測(cè)試、集成測(cè)試、系統(tǒng)測(cè)試都是為了驗(yàn)證代碼的正確性,代碼是整個(gè)工作的重心。使用了SCADE之后,整個(gè)設(shè)計(jì)流程是圍繞著SCADE模型展開的:概要設(shè)計(jì)和詳細(xì)設(shè)計(jì)的過程其實(shí)都是用SCADE建模的過程,并且提供了一系列驗(yàn)證手段保證了模型的正確性和安全性,SC ADE模型成為整個(gè)開發(fā)工作的核心,工作的重心從原先的代碼提高到了模型的級(jí)別。
1)設(shè)計(jì)過程
SCADE提供了兩套機(jī)制(數(shù)據(jù)流圖和安全狀態(tài)機(jī))來進(jìn)行圖形化建模。數(shù)據(jù)流圖適合于連續(xù)系統(tǒng)圖建模,安全狀態(tài)機(jī)適用于離散系統(tǒng)的建模。SCADE將這兩套建模機(jī)制很好
地融合在一起,能夠適用于不同類型系統(tǒng)尤其是混合系統(tǒng)的開發(fā)。
這兩套機(jī)制都建立在嚴(yán)格的數(shù)學(xué)模型基礎(chǔ)之上,具有嚴(yán)格的數(shù)學(xué)語義,它們保證了設(shè)計(jì)模型的精確性、完整性、一致性和無二義性。由于該描述是形式化的,因此建模的過程也是描述需求的過程,得到的是明確無歧義的軟件需求。
2)設(shè)計(jì)過程的驗(yàn)證
SCADE提供了一系列的驗(yàn)證機(jī)制,來確保軟件需求模型描述的正確性和安全性:
①模型靜態(tài)檢查
建立好了需求模型之后,可以對(duì)模型進(jìn)行自動(dòng)檢查,幫助找出模型中的數(shù)據(jù)流不匹配、死循環(huán)等一系列語義和方法學(xué)方面的錯(cuò)誤,并提供超鏈接進(jìn)行錯(cuò)誤定位。
②模擬仿真
模型通過靜態(tài)檢查之后,可以通過SCADE提供的模型仿真器,對(duì)整個(gè)系統(tǒng)或是系統(tǒng)中任意一個(gè)模塊進(jìn)行模擬仿真。該仿真器是一套功能強(qiáng)大的可視化的調(diào)試環(huán)境,可以設(shè)置斷言、斷點(diǎn);可以檢查輸入數(shù)據(jù)、局部變量和輸出數(shù)據(jù)的值;可以用文本或圖表的形式記錄仿真過程中各輸入輸出的值;可以保存和回放仿真的場(chǎng)景 (scenario)。最重要的一點(diǎn)也是區(qū)別其他基于模型開發(fā)工具的最重要的一點(diǎn):SCADE保證仿真結(jié)果和生成代碼運(yùn)行的結(jié)果是一致的。
③覆蓋率分析
模擬仿真是對(duì)模型進(jìn)行功能測(cè)試的過程。為了評(píng)估模型測(cè)試的完備性,SCADE提供了基于模型的覆蓋率分析。根據(jù)既定的或者自定義的覆蓋率準(zhǔn)則,分析仿真場(chǎng)景在模型中的覆蓋程度,并能指明未覆蓋的路徑;隨后用戶對(duì)覆蓋率進(jìn)行分析,找出測(cè)試用例的不足、需求設(shè)計(jì)錯(cuò)誤、死代碼等問題,用于指導(dǎo)設(shè)計(jì)模型改進(jìn)、需求改進(jìn)等。最后,SCADE還能自動(dòng)生成覆蓋率分析的報(bào)告。
④形式驗(yàn)證
模擬仿真能夠測(cè)試系統(tǒng)模型是否實(shí)現(xiàn)了預(yù)期功能,但并不能保證系統(tǒng)在所有情況下都滿足安全特征。由于測(cè)試的局限性,難以通過測(cè)試來驗(yàn)證安全特性,對(duì)于復(fù)雜的邏輯控制系統(tǒng)來說尤是如此。SCADE所提供的形式驗(yàn)證彌補(bǔ)了這一局限性。
3)自動(dòng)生成代碼
經(jīng)過模擬仿真、覆蓋率分析和形式驗(yàn)證,保證了模型的正晚性和安全性以后,可以利用SCADE內(nèi)置的代碼生成器KCG自動(dòng)生成嵌入式產(chǎn)品代碼。它生成的代碼滿足一系列的安全恃性,有良好的可讀性和接口,具有和手寫代碼相當(dāng)?shù)拇笮『妥温省T摯a生成器通過了軍工及航空業(yè)及能源業(yè)相關(guān)標(biāo)準(zhǔn)的鑒定,因此,使用 SCADE之后,不僅大大節(jié)省了編碼工作,而且完全免去了代碼的單元測(cè)試和對(duì)于單元測(cè)試的驗(yàn)證(即代碼覆蓋率分析),很大程度地節(jié)省了驗(yàn)證工作和驗(yàn)證時(shí)間。
4)集成階段的驗(yàn)證
當(dāng)?shù)玫皆创a之后,根據(jù)硬件平臺(tái)使用編譯器(如:Tornado,GCC等)將源代碼編譯為目標(biāo)代碼。高可靠性的軟件開發(fā)流程不僅需要對(duì)源代碼進(jìn)行分析,還需要保證從源代碼到目標(biāo)代碼的一致性。SCADE提供了CVK(Complier Verify Kit)工具包,能夠輔助驗(yàn)證編譯器能否正確地將KCG生成的代碼編譯成目標(biāo)碼。
5)開發(fā)流程管理
作為一個(gè)面向高可靠性軟件而設(shè)計(jì)的開發(fā)環(huán)境,SCADE在保證了嵌入式軟件的可靠性的前提之下,并通過和其他一些工具的配合保證了整個(gè)開發(fā)流程的生命周期數(shù)據(jù)管理。
①通過SCADE RM實(shí)現(xiàn)了開發(fā)過程中數(shù)據(jù)的可追溯性管理;
②通過SCC接口實(shí)現(xiàn)了開發(fā)過程中配置管理,由于SCADE以ASCII格式保存所有數(shù)據(jù),并支持標(biāo)準(zhǔn)的配置管理界面。因此,可以方便的與市面上所有的配置管理工具建立橋接。
綜上所述,SCADE采用“基于模型”的開發(fā)流程代替了“基于代碼”的開發(fā)流程,設(shè)計(jì)的結(jié)果是SCADE模型而不是代碼,從軟件開發(fā)重點(diǎn)從編碼階段提升到了設(shè)計(jì)階段;同時(shí),不再通過對(duì)測(cè)試、或是無法定量衡量的評(píng)審來保證軟件的高可靠性,而是通過對(duì)整個(gè)開發(fā)流程有效的管理來保證軟件的高可靠性。
4 結(jié)論
文中詳細(xì)介紹了以SCADE為核心的軟件開發(fā)平臺(tái),采用該平臺(tái)進(jìn)行高可靠性軟件開發(fā),克服了傳統(tǒng)的以手工編碼為核心的開發(fā)流程的不足,將軟件開發(fā)重點(diǎn)由編碼階段提前到設(shè)計(jì)階段,可以顯著縮短軟件開發(fā)周期,降低開發(fā)成本,提高開發(fā)效率。更為重要的是,傳統(tǒng)軟件開發(fā)流程中的設(shè)計(jì)流程的驗(yàn)證工作主要以手工方式進(jìn)行,驗(yàn)證的驗(yàn)證工作難以實(shí)現(xiàn),而在以SCADE為核心的開發(fā)平臺(tái)中,可以通過模型測(cè)試的方式進(jìn)行需求驗(yàn)證,該驗(yàn)證進(jìn)程可通過模型覆蓋率分析進(jìn)行驗(yàn)證;傳統(tǒng)軟件開發(fā)過程中的單元測(cè)試工作在該開發(fā)平臺(tái)中可以省略。目前,該開發(fā)平臺(tái)已經(jīng)在航空軌道交通等多個(gè)高安全性的嵌入式軟件開發(fā)方面得到廣泛應(yīng)用。作者將在后續(xù)文章中以具體案例對(duì)該開發(fā)平臺(tái)作進(jìn)一步闡述。
評(píng)論