<dfn id="yhprb"><s id="yhprb"></s></dfn><dfn id="yhprb"><delect id="yhprb"></delect></dfn><dfn id="yhprb"></dfn><dfn id="yhprb"><delect id="yhprb"></delect></dfn><dfn id="yhprb"></dfn><dfn id="yhprb"><s id="yhprb"><strike id="yhprb"></strike></s></dfn><small id="yhprb"></small><dfn id="yhprb"></dfn><small id="yhprb"><delect id="yhprb"></delect></small><small id="yhprb"></small><small id="yhprb"></small> <delect id="yhprb"><strike id="yhprb"></strike></delect><dfn id="yhprb"></dfn><dfn id="yhprb"></dfn><s id="yhprb"><noframes id="yhprb"><small id="yhprb"><dfn id="yhprb"></dfn></small><dfn id="yhprb"><delect id="yhprb"></delect></dfn><small id="yhprb"></small><dfn id="yhprb"><delect id="yhprb"></delect></dfn><dfn id="yhprb"><s id="yhprb"></s></dfn> <small id="yhprb"></small><delect id="yhprb"><strike id="yhprb"></strike></delect><dfn id="yhprb"><s id="yhprb"></s></dfn><dfn id="yhprb"></dfn><dfn id="yhprb"><s id="yhprb"></s></dfn><dfn id="yhprb"><s id="yhprb"><strike id="yhprb"></strike></s></dfn><dfn id="yhprb"><s id="yhprb"></s></dfn>

新聞中心

EEPW首頁(yè) > 嵌入式系統 > 設計應用 > 基于SCADE的嵌入式軟件開(kāi)發(fā)方法研究

基于SCADE的嵌入式軟件開(kāi)發(fā)方法研究

作者: 時(shí)間:2016-09-12 來(lái)源:網(wǎng)絡(luò ) 收藏

要素,軟件的設計模式直接決定了軟件的安全和可靠性。本文研究了高安全性應用程序開(kāi)發(fā)環(huán)境 -的特點(diǎn)和應用,介紹了一種基于該開(kāi)發(fā)環(huán)境的軟件開(kāi)發(fā)平臺方案。大量的工程的應用也表明該方案有助于提高的開(kāi)發(fā)質(zhì)量,縮短研制周期,滿(mǎn)足軟件研制需求。

本文引用地址:http://dyxdggzs.com/article/201609/303507.htm

關(guān)鍵詞:;;;;形式驗證

軟件的安全和可靠性是衡量軟件質(zhì)量最重要的指標和軟件開(kāi)發(fā)的最終目標。較之普通軟件領(lǐng)域,在高安全性的嵌入式開(kāi)發(fā)領(lǐng)域如軌道交通,航空,國防等,軟件因其任務(wù)特點(diǎn),更需要保證高可靠性。然而,何謂“高可靠性軟件”、如何開(kāi)發(fā)“高可靠性軟件”一直是困擾系統開(kāi)發(fā)人員的“瓶頸”問(wèn)題。誠然,軟件的設計模式直接決定了軟件的安全和可靠性。文中介紹了一種基于模型的可靠性軟件開(kāi)發(fā)平臺方案。大量的工程應用也表明該方法是切實(shí)有效的。

1 開(kāi)發(fā)現狀

何謂“高可靠性軟件”?1983年美國IEEE計算機學(xué)會(huì )軟件工程技術(shù)委員會(huì )將軟件可靠性定義如下:在規定的條件下,在規定的時(shí)間內,軟件不引起系統失效的概率。在規定的時(shí)間周期內和條件下,程序執行要求的功能的能力。這個(gè)標準隨后經(jīng)美國標準化研究院批準作為美國的國家標準,1989年我國國標GB/T- 11457采用了這個(gè)定義。

那么,如何開(kāi)發(fā)“高可靠性軟件”?軟件可靠性工程的任務(wù)是力爭在軟件生命周期過(guò)程中最大限度地減少軟件產(chǎn)品中的缺陷。而減少軟件缺陷必須在全面周密的考慮系統在各個(gè)不同階段、不同狀態(tài)下,保證軟件和需求的一致性。

1.1 現有的軟件開(kāi)發(fā)方法

目前,大多數嵌入式軟件項目都采用“以手工編碼和以代碼為中心”瀑布模型作為規范化開(kāi)發(fā)的基礎。該種開(kāi)發(fā)方式以代碼開(kāi)發(fā)為中心,需求分析、軟件設計為軟件編碼做準備,代碼編寫(xiě)完成后進(jìn)行單元測試。長(cháng)期以來(lái),代碼編寫(xiě)一直是開(kāi)發(fā)過(guò)程的主要階段,占用了大量的時(shí)間和人力。隨著(zhù)人們對軟件質(zhì)量的重視,單元測試在開(kāi)發(fā)過(guò)程中的地位日益重要,在目前的開(kāi)發(fā)流程中,越來(lái)越多的力量投入到代碼的單元測試中。

基于代碼開(kāi)發(fā)方式的缺點(diǎn)非常明顯:

1)開(kāi)發(fā)效率低下

由于代碼的抽象程度高,不直觀(guān),與軟件需求完全脫節,因此開(kāi)發(fā)人員不得不花大量的時(shí)間在技術(shù)細節上,代碼的修改也很耗時(shí)。

2)質(zhì)量沒(méi)有保證

由于軟件代碼由程序員手工編寫(xiě),程序員的能力、態(tài)度及狀態(tài)制約了軟件的質(zhì)量。且隨著(zhù)軟件規模、復雜度的不斷增加,團隊開(kāi)發(fā)情況的出現,代碼集成也變得越來(lái)越難。

出現這些缺點(diǎn)的主要原因在于,在基于代碼開(kāi)發(fā)方式下,開(kāi)發(fā)工作的早期(需求分析、軟件設計)完全依賴(lài)于人工工作,其成果以有歧義的自然語(yǔ)言或圖表方式描述,無(wú)法進(jìn)行有效的交流和驗證,從而成為錯誤引入的重災區;而當具有動(dòng)態(tài)行為的代碼出現后,對代碼的測試是一種事后監督的、費時(shí)費力的做法,只能盡可能地發(fā)現錯誤,而無(wú)法有效地避免或者是排除錯誤。

1.2 “基于模型”的開(kāi)發(fā)方法

隨著(zhù)人們對軟件認識的逐漸加深及實(shí)踐中的探索,模型取代代碼成為了軟件開(kāi)發(fā)流程的中心。直觀(guān)的模型符號被用于需求分析及以軟件設計過(guò)程,表達分析人員對需求的理解及細化。由于模型遠比程序語(yǔ)言的抽象程度低,更易于理解和交流,減少了需求分析和軟件設計過(guò)程中錯誤引入的機率,尤為重要的是,模型還可用于,表達其動(dòng)態(tài)特性,從而使開(kāi)發(fā)人員在開(kāi)發(fā)的早期能確定性地發(fā)現并排除錯誤。

一般來(lái)說(shuō),基于模型的開(kāi)發(fā)方式具有以下特征:

1)形式化的圖形符號

直觀(guān)易懂的圖形符號是模型的主要特征,也是模型優(yōu)于代碼的主要原因。借助于圖形化的符號組成的模型,閱讀者不僅能快速獲取模型所表達的含義,而且不會(huì )因知識背景的不同產(chǎn)生歧義。

2)模型可運行

可運行的模型為開(kāi)發(fā)人員了解模型的動(dòng)態(tài)行為提供了方便,可以驗證設計與需求是否一致。

2 “基于模型”的開(kāi)發(fā)工具

2.1 什么是“基于模型”的開(kāi)發(fā)工具?

所謂“基于模型”,是以一種形式化的模型方式描述一個(gè)系統或是一個(gè)子系統。一個(gè)模型可以是數學(xué)意義上的,由一系列關(guān)于系統的聲明構成;也可以是構架意義上的(又稱(chēng)作可執行的),用來(lái)描述一個(gè)系統對系統外激勵的響應情況。

隨著(zhù)計算機技術(shù)的迅猛發(fā)展和軟件工程自動(dòng)化的不斷發(fā)展,“基于模型”的開(kāi)發(fā)工具不斷涌現,這類(lèi)工具的普遍特點(diǎn)是通過(guò)形式化的方式實(shí)現需求、模型可以直接進(jìn)行模擬、并且可以直接將模型轉化為源代碼。

2.2 “基于模型”開(kāi)發(fā)工具的比較

基于模型的開(kāi)發(fā)工具有很多,在嵌入式軟件開(kāi)發(fā)領(lǐng)域應用比較廣泛的主要有基于UML的工具,或是結構化的設計工具(、SIMULINK等)。

1)基于UML的設計工具:關(guān)注于高層的功能劃分、結構分解、行為規范和需求分析,適合于系統建模;它從軟件工程的角度對開(kāi)發(fā)流程進(jìn)行規范,但很少考慮高可靠性嵌入式軟件開(kāi)發(fā)的特點(diǎn),軟件工程自動(dòng)化程度較低,生成的只是一個(gè)代碼框架,需要對它生成的代碼做大量的修改和補充之后才能使用。

2)Simulink:面向仿真,仿真功能比較強大,支持對硬件和外界環(huán)境的模擬,可以進(jìn)行全局的仿真和調試;但是由于底層缺乏數學(xué)理論的支撐,無(wú)法保證模型作為需求描述的無(wú)歧義性;從生成代碼的角度來(lái)說(shuō),它生成的代碼也需要做大量的修改和補充之后才能使用,而這種做法在增加工作量的同時(shí),和基于UML的設計工具一樣,帶來(lái)了一個(gè)潛在的很復雜的開(kāi)發(fā)流程管理和質(zhì)量認證上的問(wèn)題。

3)SCADE(Safety—Critical Application Development Environment)是一套基于模型的、面向高可靠性軟件而設計的開(kāi)發(fā)環(huán)境,具有嚴格的理論基礎支持,充分考慮了高可靠性軟件開(kāi)發(fā)中的質(zhì)量、安全特性、開(kāi)發(fā)周期、認證等各方面的問(wèn)題,國內外高安全性嵌入式領(lǐng)域應用經(jīng)驗表明,它非常適合用于開(kāi)發(fā)高可靠性軟件。

3 基于SCADE的軟件設計方法

3.1 SCADE簡(jiǎn)介

SCADE (Safety—Critical Application Development Environment)是一套高安全性嵌入式軟件開(kāi)發(fā)環(huán)境,運用Correct By Construction的設計理念,能夠從精確的需求規范自動(dòng)生成嵌入式源代碼,實(shí)現了開(kāi)發(fā)流程的高度自動(dòng)化。它涵蓋了嵌入式軟件開(kāi)發(fā)的整個(gè)流程:需求管理、需求建模、模型檢查、模型仿真、模型覆蓋率分析、形式驗證、代碼生成、文檔生成等等。SCADE適用于不同軟、硬件平臺,是一套通用的嵌入式軟件開(kāi)發(fā)平臺。

3.2 基于SCADE軟件設計方法

在現有的瀑布式的開(kāi)發(fā)流程中,軟件需求、概要設計、詳細設計都是為了編碼;單元測試、集成測試、系統測試都是為了驗證代碼的正確性,代碼是整個(gè)工作的重心。使用了SCADE之后,整個(gè)設計流程是圍繞著(zhù)SCADE模型展開(kāi)的:概要設計和詳細設計的過(guò)程其實(shí)都是用SCADE建模的過(guò)程,并且提供了一系列驗證手段保證了模型的正確性和安全性,SC ADE模型成為整個(gè)開(kāi)發(fā)工作的核心,工作的重心從原先的代碼提高到了模型的級別。

a.jpg

1)設計過(guò)程

SCADE提供了兩套機制(數據流圖和安全狀態(tài)機)來(lái)進(jìn)行圖形化建模。數據流圖適合于連續系統圖建模,安全狀態(tài)機適用于離散系統的建模。SCADE將這兩套建模機制很好

地融合在一起,能夠適用于不同類(lèi)型系統尤其是混合系統的開(kāi)發(fā)。

這兩套機制都建立在嚴格的數學(xué)模型基礎之上,具有嚴格的數學(xué)語(yǔ)義,它們保證了設計模型的精確性、完整性、一致性和無(wú)二義性。由于該描述是形式化的,因此建模的過(guò)程也是描述需求的過(guò)程,得到的是明確無(wú)歧義的軟件需求。

2)設計過(guò)程的驗證

SCADE提供了一系列的驗證機制,來(lái)確保軟件需求模型描述的正確性和安全性:

①模型靜態(tài)檢查

建立好了需求模型之后,可以對模型進(jìn)行自動(dòng)檢查,幫助找出模型中的數據流不匹配、死循環(huán)等一系列語(yǔ)義和方法學(xué)方面的錯誤,并提供超鏈接進(jìn)行錯誤定位。

模型通過(guò)靜態(tài)檢查之后,可以通過(guò)SCADE提供的模型仿真器,對整個(gè)系統或是系統中任意一個(gè)模塊進(jìn)行模擬仿真。該仿真器是一套功能強大的可視化的調試環(huán)境,可以設置斷言、斷點(diǎn);可以檢查輸入數據、局部變量和輸出數據的值;可以用文本或圖表的形式記錄仿真過(guò)程中各輸入輸出的值;可以保存和回放仿真的場(chǎng)景 (scenario)。最重要的一點(diǎn)也是區別其他基于模型開(kāi)發(fā)工具的最重要的一點(diǎn):SCADE保證仿真結果和生成代碼運行的結果是一致的。

③覆蓋率分析

模擬仿真是對模型進(jìn)行功能測試的過(guò)程。為了評估模型測試的完備性,SCADE提供了基于模型的覆蓋率分析。根據既定的或者自定義的覆蓋率準則,分析仿真場(chǎng)景在模型中的覆蓋程度,并能指明未覆蓋的路徑;隨后用戶(hù)對覆蓋率進(jìn)行分析,找出測試用例的不足、需求設計錯誤、死代碼等問(wèn)題,用于指導設計模型改進(jìn)、需求改進(jìn)等。最后,SCADE還能自動(dòng)生成覆蓋率分析的報告。

④形式驗證

模擬仿真能夠測試系統模型是否實(shí)現了預期功能,但并不能保證系統在所有情況下都滿(mǎn)足安全特征。由于測試的局限性,難以通過(guò)測試來(lái)驗證安全特性,對于復雜的邏輯控制系統來(lái)說(shuō)尤是如此。SCADE所提供的形式驗證彌補了這一局限性。

3)自動(dòng)生成代碼

經(jīng)過(guò)模擬仿真、覆蓋率分析和形式驗證,保證了模型的正晚性和安全性以后,可以利用SCADE內置的代碼生成器KCG自動(dòng)生成嵌入式產(chǎn)品代碼。它生成的代碼滿(mǎn)足一系列的安全恃性,有良好的可讀性和接口,具有和手寫(xiě)代碼相當的大小和孜率。該代碼生成器通過(guò)了軍工及航空業(yè)及能源業(yè)相關(guān)標準的鑒定,因此,使用 SCADE之后,不僅大大節省了編碼工作,而且完全免去了代碼的單元測試和對于單元測試的驗證(即代碼覆蓋率分析),很大程度地節省了驗證工作和驗證時(shí)間。

4)集成階段的驗證

當得到源代碼之后,根據硬件平臺使用編譯器(如:Tornado,GCC等)將源代碼編譯為目標代碼。高可靠性的軟件開(kāi)發(fā)流程不僅需要對源代碼進(jìn)行分析,還需要保證從源代碼到目標代碼的一致性。SCADE提供了CVK(Complier Verify Kit)工具包,能夠輔助驗證編譯器能否正確地將KCG生成的代碼編譯成目標碼。

5)開(kāi)發(fā)流程管理

作為一個(gè)面向高可靠性軟件而設計的開(kāi)發(fā)環(huán)境,SCADE在保證了嵌入式軟件的可靠性的前提之下,并通過(guò)和其他一些工具的配合保證了整個(gè)開(kāi)發(fā)流程的生命周期數據管理。

①通過(guò)SCADE RM實(shí)現了開(kāi)發(fā)過(guò)程中數據的可追溯性管理;

②通過(guò)SCC接口實(shí)現了開(kāi)發(fā)過(guò)程中配置管理,由于SCADE以ASCII格式保存所有數據,并支持標準的配置管理界面。因此,可以方便的與市面上所有的配置管理工具建立橋接。

綜上所述,SCADE采用“基于模型”的開(kāi)發(fā)流程代替了“基于代碼”的開(kāi)發(fā)流程,設計的結果是SCADE模型而不是代碼,從軟件開(kāi)發(fā)重點(diǎn)從編碼階段提升到了設計階段;同時(shí),不再通過(guò)對測試、或是無(wú)法定量衡量的評審來(lái)保證軟件的高可靠性,而是通過(guò)對整個(gè)開(kāi)發(fā)流程有效的管理來(lái)保證軟件的高可靠性。

4 結論

文中詳細介紹了以SCADE為核心的軟件開(kāi)發(fā)平臺,采用該平臺進(jìn)行高可靠性軟件開(kāi)發(fā),克服了傳統的以手工編碼為核心的開(kāi)發(fā)流程的不足,將軟件開(kāi)發(fā)重點(diǎn)由編碼階段提前到設計階段,可以顯著(zhù)縮短軟件開(kāi)發(fā)周期,降低開(kāi)發(fā)成本,提高開(kāi)發(fā)效率。更為重要的是,傳統軟件開(kāi)發(fā)流程中的設計流程的驗證工作主要以手工方式進(jìn)行,驗證的驗證工作難以實(shí)現,而在以SCADE為核心的開(kāi)發(fā)平臺中,可以通過(guò)模型測試的方式進(jìn)行需求驗證,該驗證進(jìn)程可通過(guò)模型覆蓋率分析進(jìn)行驗證;傳統軟件開(kāi)發(fā)過(guò)程中的單元測試工作在該開(kāi)發(fā)平臺中可以省略。目前,該開(kāi)發(fā)平臺已經(jīng)在航空軌道交通等多個(gè)高安全性的嵌入式軟件開(kāi)發(fā)方面得到廣泛應用。作者將在后續文章中以具體案例對該開(kāi)發(fā)平臺作進(jìn)一步闡述。



評論


相關(guān)推薦

技術(shù)專(zhuān)區

關(guān)閉
国产精品自在自线亚洲|国产精品无圣光一区二区|国产日产欧洲无码视频|久久久一本精品99久久K精品66|欧美人与动牲交片免费播放
<dfn id="yhprb"><s id="yhprb"></s></dfn><dfn id="yhprb"><delect id="yhprb"></delect></dfn><dfn id="yhprb"></dfn><dfn id="yhprb"><delect id="yhprb"></delect></dfn><dfn id="yhprb"></dfn><dfn id="yhprb"><s id="yhprb"><strike id="yhprb"></strike></s></dfn><small id="yhprb"></small><dfn id="yhprb"></dfn><small id="yhprb"><delect id="yhprb"></delect></small><small id="yhprb"></small><small id="yhprb"></small> <delect id="yhprb"><strike id="yhprb"></strike></delect><dfn id="yhprb"></dfn><dfn id="yhprb"></dfn><s id="yhprb"><noframes id="yhprb"><small id="yhprb"><dfn id="yhprb"></dfn></small><dfn id="yhprb"><delect id="yhprb"></delect></dfn><small id="yhprb"></small><dfn id="yhprb"><delect id="yhprb"></delect></dfn><dfn id="yhprb"><s id="yhprb"></s></dfn> <small id="yhprb"></small><delect id="yhprb"><strike id="yhprb"></strike></delect><dfn id="yhprb"><s id="yhprb"></s></dfn><dfn id="yhprb"></dfn><dfn id="yhprb"><s id="yhprb"></s></dfn><dfn id="yhprb"><s id="yhprb"><strike id="yhprb"></strike></s></dfn><dfn id="yhprb"><s id="yhprb"></s></dfn>