軟件工程在高安全性嵌入式軟件開發(fā)的應(yīng)用

1、基于模型的軟件工程在高安全性嵌入式軟件開發(fā)的應(yīng)用高安全性嵌入式軟件的現(xiàn)狀及趨勢(shì)0.1M0.6M6M1.7M1st Gen.2nd Gen.4th Gen.LOCElectro-mechanicalSoftwareTimeThe number of function implemented by software 80%Complexity3rd Gen.軟件比重急劇上升高安全性嵌入式軟件的現(xiàn)狀及趨勢(shì)1991年海灣戰(zhàn)爭(zhēng)，愛國(guó)者導(dǎo)彈在攔截飛毛腿導(dǎo)彈中幾次攔截失敗，其直接原因?yàn)檐浖到y(tǒng)未能及時(shí)消除計(jì)時(shí)累計(jì)誤差。1996年阿里亞娜型運(yùn)載火箭由于控制軟件數(shù)據(jù)轉(zhuǎn)換溢出起飛40秒后爆炸，造成經(jīng)濟(jì)損失達(dá)5億美

2、元。1999年大力神4B運(yùn)載火箭由于軟件問題飛行9秒后偏離航向，造成衛(wèi)星未進(jìn)入預(yù)定軌道。軟件安全性要求越來(lái)越突出傳統(tǒng)研制方式面臨的問題1）軟件設(shè)計(jì)與開發(fā)之間存在壁壘，造成項(xiàng)目管理不能很好實(shí)施，開發(fā)反復(fù)迭代，研制周期無(wú)法保證。軟件需求編寫規(guī)格說明分析設(shè)計(jì)原型系統(tǒng)設(shè)計(jì)階段項(xiàng)目管理缺陷管理文檔管理任務(wù)管理協(xié)作管理組件管理手寫代碼代碼調(diào)試測(cè)試系統(tǒng)集成系統(tǒng)開發(fā)階段過早開始編碼設(shè)計(jì)結(jié)果割裂項(xiàng)目組織不能很好實(shí)施反復(fù)迭代傳統(tǒng)研制方式面臨的問題2）文檔的不可驗(yàn)證性以及手工編寫代碼，導(dǎo)致錯(cuò)誤發(fā)現(xiàn)滯后，開發(fā)代價(jià)很大，軟件質(zhì)量無(wú)法保證。傳統(tǒng)研制方式面臨的問題3）嵌入式系統(tǒng)軟件的本質(zhì)特征要求軟件驗(yàn)證必須結(jié)合目標(biāo)平臺(tái)，但

3、目前驗(yàn)證工作完全依賴于目標(biāo)平臺(tái)，使軟件驗(yàn)證工作的開展受制于硬件的研制進(jìn)度。4）嚴(yán)重依賴于人工，自動(dòng)化程度不足，效率低且很多工作對(duì)人的經(jīng)驗(yàn)依賴大。急需改變傳統(tǒng)研制流程！在國(guó)外已經(jīng)得到廣泛使用；國(guó)內(nèi)雖然起步較晚，但發(fā)展迅速，尤其在民用領(lǐng)域?；谀Ｐ偷能浖_發(fā)方法提供了有效的手段！汽車核工業(yè)軌道交通航空A380飛控、航電等系統(tǒng)80%的代碼都是模型自動(dòng)生成法國(guó)泰勒斯公司的THEMIS工具鏈中集成的商用建模工具Embedded System & SoftwareLifecycle ManagementEmbeddedSystem DesignControlSoftware DesignHMISoftwa

4、re DesignTestingEnvironment（Safety Critical Application Development Environmen）ANSYS SCADE主要產(chǎn)品線ANSYS基于模型的軟件工程解決方案軟件高層需求軟件架構(gòu)設(shè)計(jì)軟件詳細(xì)設(shè)計(jì)自動(dòng)生成代碼架構(gòu)模型驗(yàn)證模型級(jí)驗(yàn)證多學(xué)科模型閉環(huán)仿真系統(tǒng)驗(yàn)證軟硬件集成驗(yàn)證DOORS/WORD自動(dòng)同步自動(dòng)生成代碼SCADE代碼生成器SCADE Suite和SCADE DisplaySCADE SystemSimplorerSCADE Test功能層定義功能層架構(gòu)及數(shù)據(jù)定義功能層數(shù)據(jù)流軟件層定義軟件架構(gòu)定義傳遞的數(shù)據(jù)消息功能層到軟件層

5、的映射平臺(tái)層定義計(jì)算單元、總線、交換機(jī)等軟件層到硬件的映射軟件架構(gòu)設(shè)計(jì)：三層設(shè)計(jì)推薦功能層功能架構(gòu)設(shè)計(jì)信號(hào)/數(shù)據(jù) 定義數(shù)據(jù)傳播軟件層A429/AFDX/ message definitionA429 messageAFDX message功能到軟件的分配軟件層(AFDX)功能層軟件層(ARINC 429)分配分配1. Allocate data to message2. Allocate functional component to software component平臺(tái)層A429 busesAFDX busesAFDX Virtual Links軟件到平臺(tái)層的分配軟件層(AFDX)功能層

6、軟件層(ARINC 429)平臺(tái)層(AFDX)平臺(tái)層(ARINC 429)1. Allocate message to buses/virtual links2. Allocate software component to hardware componentICD (Interface Control Document)ARINC 429RDC A429 MessagesICD (Interface Control Document)AFDXCPU1 AFXD Virtual LinksAFXD Messages DefinitionDS Definition自帶加自定義規(guī)則庫(kù)，自動(dòng)使用這

7、些規(guī)則進(jìn)行檢查分析比如AFDX通訊帶寬檢查Checks that the sum of AFDX message lenght * rate of the AFDX logical port they go throughtis lower than the coreesponding AFDX physical port bandwith 架構(gòu)模型檢查分析SCADE System與SCADE Suite數(shù)據(jù)接口同步接口比較與合并軟件架構(gòu)和詳細(xì)設(shè)計(jì)模型間的同步軟件控制邏輯建模軟件控制邏輯建模case State is when State1 = Guard1 := X 3; if (EVENT

8、1 and (Guard1 or Guard2) then if (Guard1) then X := 5; State := State2; else if (Guard2) then X := 6; end if; State := State3; end if; end if; when State2 = if (EVENT1) then X := 7; State := State1; end if; when State3 = if (EVENT1 and EVENT1) then X := 8; State := State1; end if;End case更加直觀簡(jiǎn)單ADA語(yǔ)言

9、SCADE模型的背后是SCADE語(yǔ)言SCADE語(yǔ)言是同步的形式化語(yǔ)言，起源于同步語(yǔ)言Lustre同步語(yǔ)言更方便描述反應(yīng)系統(tǒng)(Reactive System)嚴(yán)謹(jǐn)精確、無(wú)二義性確定性更加容易驗(yàn)證Correct/Safety by constructionSCADE的建模構(gòu)件都是經(jīng)過嚴(yán)格定義，都是安全構(gòu)件盡可能在建模的時(shí)候確保滿足高安全Do It Right The First Time!不僅僅是可視化的模型顯示畫面建模Embedded HMIs(Cockpits, Dashboards, Control Centers, etc.)Rail DMIsSchematics(Plant mimic,

10、 electrics, hydraulics, etc.)2D/3D Simulators & Trainers(Maintenance, pilots, crews)支持“所見即所得”的設(shè)計(jì)，提高開發(fā)效率支持交互式：支持鼠標(biāo)、鍵盤、觸摸屏、多點(diǎn)控制等豐富的控件庫(kù)和專業(yè)儀表，允許用戶自定義控件支持符合ARINC 661規(guī)范的座艙顯示系統(tǒng)開發(fā)顯示畫面建模汽車儀表面板示例Automotive tactile/interactive infotainment HMI demo model developed with SCADE Display, for Android & iOS提前進(jìn)行驗(yàn)證基于模

11、型的驗(yàn)證能提前發(fā)現(xiàn)缺陷根據(jù)客戶統(tǒng)計(jì)反饋，使用SCADE開發(fā)的應(yīng)用基本上90%的缺陷能在模型級(jí)驗(yàn)證時(shí)捕獲。模型檢查SCADE的語(yǔ)法語(yǔ)義檢查設(shè)計(jì)標(biāo)準(zhǔn)符合性檢查 2015 ANSYS Inc. and Esterel TechnologiesError message: Incompatible type interfacelocate仿真調(diào)試顯示模型邏輯模型仿真面板單步、多部、連續(xù)調(diào)試模型覆蓋率分析模型覆蓋率分析能識(shí)別哪些基于需求實(shí)現(xiàn)的模型沒有被來(lái)源于需求的測(cè)試用例所覆蓋是評(píng)估模型驗(yàn)證活動(dòng)完備性的途徑。模型覆蓋率分析用于檢測(cè)不充分的測(cè)試軟件需求不充分非預(yù)期功能經(jīng)過DO-178C (DO-330 T

12、QL-5)工具鑒定 2015 ANSYS Inc. and Esterel Technologies模型覆蓋率分析例子 2015 ANSYS Inc. and Esterel Technologies運(yùn)行一遍，同時(shí)獲取模型和源代碼結(jié)構(gòu)覆蓋率。最壞運(yùn)行時(shí)間和堆棧分析針對(duì)模型評(píng)估其在目標(biāo)平臺(tái)的最壞運(yùn)行時(shí)間和最大堆棧使用情況 2015 ANSYS Inc. and Esterel Technologies形式化驗(yàn)證 2015 ANSYS Inc. and Esterel Technologies安全屬性定義安全屬性評(píng)估生成反例SCADE模型安全屬性輸入滿足安全屬性？自動(dòng)分析，不需要寫測(cè)試用例，是傳統(tǒng)

13、測(cè)試方法的補(bǔ)充。多學(xué)科聯(lián)合仿真電路仿真降階模型 3D物理仿真功能模擬仿真接口(FMI) 軟件控制模型接口和降階后的2-D & 3-D模型詳細(xì)的電源電路仿真測(cè)試嵌入軟件降階后的3-D模型支持 FMI 2.0自動(dòng)代碼代碼void Button_ABC_N(inC_Button_ABC_N *inC, outC_Button_ABC_N *outC) /* ABC_N:Button:SM1:SSM_SM1_dispatch_sel */ SSM_Button_SM1_ST SSM_SM1_dispatch_sel; if (outC-init) outC-init = kcg_false; SSM_

14、SM1_dispatch_sel = SSM_SM1_Unselected_ABC_N; else SSM_SM1_dispatch_sel = outC-M_pre_; switch (SSM_SM1_dispatch_sel) case SSM_SM1_Locked_ABC_N : outC-foreground = white_ABC_N; outC-background = green_ABC_N; if (inC-Unlock) outC-M_pre_ = SSM_SM1_Preselected_ABC_N; else outC-M_pre_ = SSM_SM1_Locked_ABC

15、_N; break; case SSM_SM1_WaitUnlock_ABC_N : outC-foreground = black_ABC_N; outC-background = grey_ABC_N; if (inC-Unlock) outC-M_pre_ = SSM_SM1_Unselected_ABC_N; else outC-M_pre_ = SSM_SM1_WaitUnlock_ABC_N; break;支持生成C和ADA代碼代碼生成器經(jīng)過DO-178B A級(jí)和DO-178C TQL-1級(jí)(航空)、EN 50128 SIL 3/4(軌道)、IEC 61508 SIL3(重工)、I

16、EC 60880(核電)、ISO 26262 ASIL D級(jí)(汽車)等安全標(biāo)準(zhǔn)認(rèn)證。為什么要工具鑒定？自動(dòng)保證代碼和模型的一致性。省略代碼級(jí)的驗(yàn)證工作。代碼生成器經(jīng)過鑒定生成的C代碼滿足：可移植性好，兼容ISO-C標(biāo)準(zhǔn)代碼反映數(shù)據(jù)流模型架構(gòu)，可追溯到SCADE模型代碼可讀性好內(nèi)存分配完全靜態(tài)，沒有動(dòng)態(tài)內(nèi)存分配沒有指針運(yùn)算沒有遞歸所有的循環(huán)邊界都是確定的所有的數(shù)組邊界都是確定的最長(zhǎng)執(zhí)行時(shí)間都是確定的顯示部分代碼兼容OpenGL標(biāo)準(zhǔn)(OpenGL, OpenGL SC和OpenGL ES)，容易跨平臺(tái)移植達(dá)到高安全性標(biāo)準(zhǔn)，可以用于真實(shí)項(xiàng)目!Rule 1: Restrict all code to

17、very simple control flow constructsdo not use goto statements, setjmp or longjmp constructs, or direct or indirect recursion.Rule 2: Give all loops a fixed upper bound. Rule 3: Do not use dynamic memory allocation after initialization.Rule 4: No function should be longer than what can be printed on

18、a single sheet of paper in a standard format with one line per statement and one line per declaration.Rule 5: The codes assertion density should average to minimally two assertions per function.Rule 6: Declare all data objects at the smallest possible level of scope.Rule 7: Each calling function mus

19、t check the return value of nonvoid functions, and each called function must check the validity of all parameters provided by the caller.Rule 8: The use of the preprocessor must be limited to the inclusion of header files and simple macro definitions.Rule 9: The use of pointers must be restricted. Specifically, no more than one level of dereferencing should be used.Rule 10: All code must be compiled, from the first day of development, with all compiler warnings enabled at the most pedantic setting a