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

高玉娜

（上海海洋大學(xué) 工程學(xué)院，上海 201306）

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

1 嵌入式軟件開發(fā)現(xiàn)狀

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

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

1.1 現(xiàn)有的軟件開發(fā)方法

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

基于代碼開發(fā)方式的缺點非常明顯：

1）開發(fā)效率低下

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

2）質(zhì)量沒有保證

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

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

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

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

一般來說，基于模型的開發(fā)方式具有以下特征：

1）形式化的圖形符號

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

2）模型可運行

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

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

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

所謂“基于模型”，是以一種形式化的模型方式描述一個系統(tǒng)或是一個子系統(tǒng)[3]。一個模型可以是數(shù)學(xué)意義上的，由一系列關(guān)于系統(tǒng)的聲明構(gòu)成；也可以是構(gòu)架意義上的（又稱作可執(zhí)行的），用來描述一個系統(tǒng)對系統(tǒng)外激勵的響應(yīng)情況。

隨著計算機技術(shù)的迅猛發(fā)展和軟件工程自動化的不斷發(fā)展，“基于模型”的開發(fā)工具不斷涌現(xiàn)，這類工具的普遍特點是通過形式化的建模方式實現(xiàn)需求、模型可以直接進行模擬、并且可以直接將模型轉(zhuǎn)化為源代碼。

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

基于模型的開發(fā)工具有很多，在嵌入式軟件開發(fā)領(lǐng)域應(yīng)用比較廣泛的主要有基于UML的建模工具，或是結(jié)構(gòu)化的設(shè)計工具（SCADE、SIMULINK 等）。

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

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

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

3 基于SCADE的軟件設(shè)計方法

3.1 SCADE簡介

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

3.2 基于SCADE軟件設(shè)計方法

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

圖1 基于SCADE的嵌入式軟件開發(fā)平臺Fig.1 Structure of embedded software development platform with SCADE

1）設(shè)計過程

SCADE提供了兩套機制（數(shù)據(jù)流圖和安全狀態(tài)機）來進行圖形化建模。數(shù)據(jù)流圖適合于連續(xù)系統(tǒng)圖建模，安全狀態(tài)機適用于離散系統(tǒng)的建模。SCADE將這兩套建模機制很好地融合在一起，能夠適用于不同類型系統(tǒng)尤其是混合系統(tǒng)的開發(fā)。

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

2）設(shè)計過程的驗證

SCADE提供了一系列的驗證機制，來確保軟件需求模型描述的正確性和安全性：

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

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

②模擬仿真

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

③覆蓋率分析

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

④形式驗證

模擬仿真能夠測試系統(tǒng)模型是否實現(xiàn)了預(yù)期功能，但并不能保證系統(tǒng)在所有情況下都滿足安全特征。由于測試的局限性，難以通過測試來驗證安全特性，對于復(fù)雜的邏輯控制系統(tǒng)來說尤是如此。SCADE所提供的形式驗證[4]彌補了這一局限性。

3）自動生成代碼

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

4）集成階段的驗證

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

5）開發(fā)流程管理

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

①通過SCADE RM實現(xiàn)了開發(fā)過程中數(shù)據(jù)的可追溯性管理；

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

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

4 結(jié) 論

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

[1]宋彬，沈懷容.航天產(chǎn)品單元可靠性評估軟件研究[J].裝備指揮技術(shù)學(xué)院學(xué)報，2002，12（4）:54-57 SONG Bin，SEHN Huai-rong.Research on reliability evaluation software for spaceflight items[J].Equipment Command Cechnical College Journals，2001，12（4）:54-57.

[2]石柱，何新貴.航天型號軟件生存周期模型選擇指南[J].計算機工程與設(shè)計，2000，21（6）:43-47.SHI Zhu，HE Xin-gui.Guidelines on selecting an appropriate software Life-cycle model for a specific aerospace software project[J].Computer Engineering and Design，2000，21（6）:43-47.

[3]楊麗莎，王慧.基于模型的嵌入式軟件設(shè)計[J].計算機應(yīng)用研究，2004，21（12）:76-78.YANG Li-sha，WANG Hui.Model-based design of embedded software[J].Application Research of Computers，2004，21（12）:76-78.

[4]林楓.基于SCADE的形式化驗證技術(shù)研究[J].測控技術(shù)，2011，30（12）:71-74.LIN Feng.Research on SCADE-Based formal verification technology[J].Measurement and Control Technology，2011，30（12）:71-74.

[5]Jean-Louis Camus，Bernard Dion.Efficient development of airborne software with SCADE suite[M].Esterel Technologies，2011.

[6]Berry G.The Constructive Semantics of Pure Esterel Draft V3[M].Esterel Technologies，2009.