SCADE的案例
嵌入式系統(tǒng) | 基于SCADE Display模型的驗證
圖表12 使用SCADE QTE在主機上執(zhí)行SCADE Display模型功能測試和像素比對后的文本報告
圖表13 使用SCADE QTE在主機上執(zhí)行SCADE Display模型功能測試和像素比對后的圖形報告
視頻4: 使用SCADE QTE在主機上執(zhí)行SCADE Display模型功能測試和像素比對
2.3 執(zhí)行在主機上的模型覆蓋分析
使用SCADE QTE在主機上進行模型覆蓋分析結果如下圖，可以便捷地通過顏色來區(qū)分覆蓋分析的完整度，綠色是完全覆蓋，紅色是未覆蓋，紫色是不可覆蓋且沒有解釋。
圖表14 使用SCADE QTE在主機上執(zhí)行SCADE Display模型覆蓋分析后的全局報告
圖表15 使用SCADE QTE在主機上執(zhí)行SCADE Display模型覆蓋分析后的部分設計畫面的結果報告
視頻5: 使用SCADE QTE在主機上執(zhí)行SCADE Display模型的覆蓋分析
2.4 基于目標機上的測試
如果需要在目標機上進行軟硬件集成測試時，SCADE QTE支持將主機上測試完畢后得到的測試用例轉換為可連接目標機的第三方程序對應的測試用例，以便用戶能簡單快捷地進行目標機上的測試。
展開 嵌入式系統(tǒng) | 基于SCADE Suite模型的驗證
除此之外，還有SCADE快速原型(Rapid Prototype)，SCADE形式化驗證(Design Verify)（*關于該部分內容可詳細參考《基于SCADE模型的形式化方法》的第五節(jié)），SCADE最壞運行時間和堆棧分析(Timing and Stack Optimizer)，SCADE編譯器驗證套件(Complier Verification Kit)，SCADE軟件生命周期管理(ALM)橋接器和SCADE多學科仿真文件生成(FMI/FMU)生成器等工具用于其他的驗證活動。
2
SCADE認證級測試環(huán)境Qualified Test Environment
圖表1: SCADE認證級測試環(huán)境工作流
大規(guī)模的自動化驗證活動推薦使用SCADE的認證級測試環(huán)境(Qualified Test Environment)來操作。SCADE QTE是可通過DO-330 TQL-5級別鑒定的驗證工具。
展開 嵌入式系統(tǒng) | 基于SCADE Suite模型的驗證
除此之外，還有SCADE快速原型(Rapid Prototype)，SCADE形式化驗證(Design Verify)（*關于該部分內容可詳細參考《基于SCADE模型的形式化方法》的第五節(jié)），SCADE最壞運行時間和堆棧分析(Timing and Stack Optimizer)，SCADE編譯器驗證套件(Complier Verification Kit)，SCADE軟件生命周期管理(ALM)橋接器和SCADE多學科仿真文件生成(FMI/FMU)生成器等工具用于其他的驗證活動。
2
SCADE認證級測試環(huán)境Qualified Test Environment
圖表1: SCADE認證級測試環(huán)境工作流
大規(guī)模的自動化驗證活動推薦使用SCADE的認證級測試環(huán)境(Qualified Test Environment)來操作。SCADE QTE是可通過DO-330 TQL-5級別鑒定的驗證工具。
展開 嵌入式系統(tǒng) | 基于SCADE Display模型的驗證
圖表12 使用SCADE QTE在主機上執(zhí)行SCADE Display模型功能測試和像素比對后的文本報告
圖表13 使用SCADE QTE在主機上執(zhí)行SCADE Display模型功能測試和像素比對后的圖形報告
視頻4: 使用SCADE QTE在主機上執(zhí)行SCADE Display模型功能測試和像素比對
2.3 執(zhí)行在主機上的模型覆蓋分析
使用SCADE QTE在主機上進行模型覆蓋分析結果如下圖，可以便捷地通過顏色來區(qū)分覆蓋分析的完整度，綠色是完全覆蓋，紅色是未覆蓋，紫色是不可覆蓋且沒有解釋。
圖表14 使用SCADE QTE在主機上執(zhí)行SCADE Display模型覆蓋分析后的全局報告
圖表15 使用SCADE QTE在主機上執(zhí)行SCADE Display模型覆蓋分析后的部分設計畫面的結果報告
視頻5: 使用SCADE QTE在主機上執(zhí)行SCADE Display模型的覆蓋分析
2.4 基于目標機上的測試
如果需要在目標機上進行軟硬件集成測試時，SCADE QTE支持將主機上測試完畢后得到的測試用例轉換為可連接目標機的第三方程序對應的測試用例，以便用戶能簡單快捷地進行目標機上的測試。
展開 
SCADE — 產(chǎn)品級安全關鍵系統(tǒng)的MBD開發(fā)套件
? SCADE汽車包，專為汽車領域提供SCADE Architect 和SCADE Suite專業(yè)擴展，包括:
? AUTOSAR定制符合AUTOSAR4.2.2標準
? 支持SCADE Architect項目ARXML文件的導入/導出
? 支持SCADE Architect和SCADE Suite進行雙向同步，確保架構模型和詳細設計模型一致性
? SCADE Suite生成的代碼符合AUTOSAR標準
? 支持ASAM MCD-2 DC（aka ASAP2）軟件標定和測量
展開 3/22 Ansys SCADE 2022 R1 新功能
內容簡介
1.SCADE Achitect的新功能，添加FACE 3.1版本支持，新增AutoSAR架構設計新特性
2.SCADE Achitect支持對Dassualt的Cameo架構文件導入，支持對EA的Sparx文件導入
3.SCADE Suite UI的改進
4.SCADE Suite中形式化驗證對抽象對象分析介紹
5.SCADE Suite/Test中基于形式化驗證的模型覆蓋分析方法介紹和應用
6.SCADE Display新增8個特效容器，對復雜字體顯示的支持
7.SCADE Display對3D圖元的支持
8.SCADE Lifecycle改進更新
9.SCADE對AbsInt WCET支持的策略變化
10.文檔更新 EN 50128 A661方案
面向受眾
SCADE工具用戶，航空航天，軌道交通、汽車電子領域中系統(tǒng)架構設計，軟件開發(fā)驗證
時間
2022年3月22日（周二）16:00-17:00
展開 SCADE—產(chǎn)品級安全關鍵系統(tǒng)的MBD開發(fā)套件
借助SCADE LifeCycle，參與關鍵應用開發(fā)的所有系統(tǒng)和軟件團隊都可以在SCADE應用的整個生命周期內，管理和控制其設計和驗證活動
SCADE汽車包：專為汽車領域提供SCADE Architect和SCADE Suite擴展，包括
? AUTOSAR定制符合AUTOSAR4.2.2標準
? 支持SCADE Architect項目ARXML文件的導入/導出
? 支持SCADE Architect和SCADE Suite進行雙向同步，確保架構模型和詳細設計模型一致性
? SCADE Suite生成的代碼符合AUTOSAR標準
? 支持ASAMMCD-2DC(aka ASAP2)軟件標定和測量
應用案例
德國大眾：自2016年開始，基于SCADE在BMS、EPS中構建軟件，滿足ISO 26262 ASILC/D的應用要求。通過多個項目的比較評估，可以有效減少56%的開發(fā)時間，為項目節(jié)省30%的人力和成本
斯巴魯：在推出新混合動力和電動車型的市場競爭中，Ansys SCADE在過去10年已經(jīng)成為斯巴魯?shù)囊豁椫匾獞?zhàn)略工具，兌現(xiàn)汽車制造商對于出色安全性和可靠性的承諾。節(jié)省ECU的端到端開發(fā)時間，同時保持其控制軟件的準確性，這對于斯巴魯推出創(chuàng)新技術至關重要
主要客戶
大眾、寶馬、斯巴魯、NEVS、Faraday Future、馬自達、TOYOTA TSUSHO ELECTRONICS、德爾福、DENSO、DURA、Method Electronics、Autodrive Solutions等。
展開 嵌入式系統(tǒng) | 細數(shù)Ansys SCADE的前世今生
這就不得不提到Ansys SCADE系列產(chǎn)品。
SCADE誕生于上世紀80年代的法國，從歐洲的航空與核能領域的工程應用起步，經(jīng)過近40年的發(fā)展，現(xiàn)代SCADE已經(jīng)是融合了Esterel、Lustre、SAO\SAGA、Lucid Synchrone等多個語言和工具的集大成之作。由于SCADE專注于流程規(guī)范、標準嚴苛的安全關鍵行業(yè)，行業(yè)的特性使得其多應用于研制具有相當密級的、高難度的重大項目。因此，盡管進入中國市場已有10多年，其知名度卻一般。
在逐漸成為航空航天、國防軍工、軌道交通、核能重工、汽車電子等安全關鍵行業(yè)里具有廣泛的商業(yè)應用的同時，SCADE也是產(chǎn)學研相結合的一個典范，SCADE研發(fā)團隊中脫穎而出的法國科學院院士和圖靈獎獲得者就是對該產(chǎn)品的一種絕佳肯定。本文將主要介紹SCADE的起源，發(fā)展，現(xiàn)狀和展望，在后續(xù)系列文章中也將對國外多家知名企業(yè)的SCADE應用情況做詳細介紹，希望以此讓大家對SCADE產(chǎn)品和行業(yè)應用有更好的認識。
01
誕生階段
在上世紀80年代早期，Jean-Paul Marmorat和Jean-Paul Rigault，這兩位在巴黎高等礦業(yè)學校(Ecole des Mines de Paris)研究控制理論和計算機科學的學者,他們在設計機器人汽車的過程中，受困于傳統(tǒng)編程語言不太適合寫出精確的控制邏輯，因此專門設計了一種新的語言，而這就是SCADE語言的雛形。
展開 “中車SCADE軟件建模勞動競賽”圓滿結束
Ansys SCADE 基于模型的嵌入式安全軟件開發(fā)工具鏈
Ansys SCADE 車載安全嵌入式軟件解決方案，提供全生命周期的基于模型的開發(fā)工具鏈，涵蓋軟件架構設計、詳細設計、代碼自動生成、軟件單元測試、集成測試、過程追溯以及相應文檔生成，客戶可根據(jù)自生需要選擇單點工具或整套工具鏈。
Ansys SCADE Architect
嵌入式系統(tǒng)&軟件架構設計工具，支持SysML和AUTOSAR CP標準
Ansys SCADE Suite
嵌入式系統(tǒng)控制軟件詳細設計工具，支持建模、仿真、自動生成高質量的符合ISO26262 ASIL D級的代碼
Ansys SCADE Display
嵌入式系統(tǒng)人機界面設計工具，支持所見即所得的圖形建模、仿真、自動生成高質量的符合ISO26262 ASIL D級的代碼
Ansys SCADE Tester
嵌入式軟件的自動測試環(huán)境，用來進行基于Ansys SCADE Suite和Display設計模型的功能測試以及覆蓋率（DC和MC/DC）的獲取和分析
Ansys SCADE Lifecycle
基于Ansys SCADE開發(fā)環(huán)境的嵌入式系統(tǒng)開發(fā)生命周期管理和支持工具，包括設計文檔的自動生成、建立模型和需求的追溯關系以及模型的構型管理支持等等。
展開 嵌入式系統(tǒng) | Ansys SCADE在巴黎地鐵交通集團RATP的應用
2
形式化方法在RATP的擴大應用
不過，1998年后在RATP眾多供應商中僅有西門子(Siemens)和阿爾斯通(Alstom)兩家繼續(xù)使用B方法進行其他項目軌交信號系統(tǒng)的研發(fā)，而以安薩爾多Ansaldo，泰雷茲Thales，阿?，mAreva為代表的供應商則選擇使用SCADE產(chǎn)品進行軌交信號系統(tǒng)的開發(fā)，還有其他供應商使用Petri網(wǎng)或者Ada語言行開發(fā)……之后西門子和阿爾斯通在不少項目上也開始使用SCADE進行大規(guī)模的研發(fā)。值得一提的是，Z語言和Lustre語言都是創(chuàng)立于上世紀80年代初，之后又分別演進出了B語言(Event B語言)和SCADE語言。在同樣都是形式化語言的基礎上，B語言的語法語義的掌握既需要專家的長期支持，又需要經(jīng)常實踐才能達到一定的門檻；而SCADE語言是基于模型的開發(fā)驗證工具及可橋接的第三方工具更多，這可能是其應用更廣泛的原因。
圖表1: RATP的CBTC和聯(lián)鎖項目中的供應商與采用的形式化開發(fā)技術
3
RATP的PERF
為了在評估軟件系統(tǒng)時能獨立于各供應商選用開發(fā)的形式化模型，RATP根據(jù)內部的安全政策，研制出了獨立的工具鏈，并在此基礎上提出了PERF（Proof Executed over a Retro-engineered Formal model）方法論。PERF是在系統(tǒng)開發(fā)之后執(zhí)行的一種形式化證明方法。與諸如B方法這類貫穿于系統(tǒng)的開發(fā)階段的形式化技術不同，PERF的驗證技術僅在V流程開發(fā)周期的右側上升階段(即驗證階段)應用。
展開 嵌入式系統(tǒng) | 基于SCADE模型的形式化方法
Miller, Steven P關于模型檢查技術的可擴展驗證域圖
4
基于SCADE的模型檢查
對SCADE模型進行形式化分析的絕大部分商用工具采用的就是基于BMC方法的模型檢查技術。當前SCADE 在2020 R1版本中包含了Prover Technology的Design Verifier引擎，Design Verifier引擎里內置了SAT解算器，可以對SCADE模型進行模型檢查，當結果為錯誤時，自動給出反例的測試用例。
使用SCADE模型實現(xiàn)形式化驗證的通用方法是：保持原有設計模型不變，根據(jù)需求定義含安全屬性的觀察模型，再設計頂層操作符將設計模型和屬性觀察模型串聯(lián)起來，最終分析屬性模型的輸出即可。
SCADE模型檢查方法簡圖
基于SCADE模型的形式化方法詳細工作流如下。
SCADE模型的形式化方法工作流
創(chuàng)建新的形式化驗證工程，或在當前開發(fā)工程中使能形式化分析引擎，這樣就能自動將形式化驗證相關的Suite預定義庫導入到工程中
根據(jù)安全需求和使用場景定義觀察者模型，其中包含的安全屬性也是用Suite設計，該安全屬性的輸出必須設計為bool類型，以true值輸出代表安全導向，供形式化引擎進行分析
創(chuàng)建頂層操作符，將原設計模型和觀察者/屬性模型連接起來。
展開 
嵌入式系統(tǒng) | Ansys SCADE在軌交列車控制系統(tǒng)中的應用
在軟件設計階段，使用SCADE進行形式化建模和后續(xù)驗證，其中可以用到如下模塊：
SCADE Suite Editor 支持圖形或文本建模
SCADE Requirements Gateway Integration 支持模型級追蹤管理
SCADE Model Check 支持語法語義檢查
SCADE Model Diff 支持模型比對
SCADE Simulator 支持模型級仿真、調試；支持自動化定制
SCADE Rapid Prototype 支持快速設計仿真界面進行交互式測試
SCADE Code Generator KCG 支持認證級C或Ada代碼生成
SCADE Reporter 支持文檔生成
SCADE Model Test Coverage MTC: 支持模型級和代碼級的覆蓋分析；支持自動化定制
SCADE Design Verifier: 橋接Prover公司工具，支持形式化分析
SCADE Timing Verifier: 橋接AbsInt公司工具，支持最壞運行時間和堆棧分析
RT-Tester: 橋接目標機測試工具，支持將模型級測試用例轉換為選用工具的測試用例
6
SCADE在OpenETCS中的形式化驗證
展開 報名 | Ansys SCADE 2022 R1 新功能
Ansys SCADE 在2022 R1新版本中支持航空航天與國防領域（DO-178C、ARINC 661、FACE）、汽車領域（ISO 26262、 AUTOSAR）和工業(yè)領域（IEC 61508、EN 50128）中安全、可互操作嵌入式軟件的國際標準。
3月22日，Ansys 2022 R1新品發(fā)布系列網(wǎng)絡研討會中將推出『Ansys SCADE 2022 R1 新功能』主題內容，將介紹SCADE Achitect的新功能，SCADE Suite UI的改進，SCADE Display實現(xiàn)的新功能以及SCADE Lifecycle的優(yōu)化等等，歡迎大家預約本場活動。
時間
3月22日（星期二），16:00-17:00
面向受眾
SCADE工具用戶、航空航天、軌道交通、汽車電子領域中系統(tǒng)架構設計、軟件開發(fā)驗證等
講師介紹
沈軼燁 | Ansys高級應用工程師
Ansys高級應用工程師，負責系統(tǒng)事業(yè)部的安全關鍵領域的系統(tǒng)和軟件的開發(fā)驗證。
展開 嵌入式系統(tǒng) | Ansys SCADE在航天自動運載飛船中的應用
自動運載飛船主要為國際空間站提供如下服務：
燃料補給
貨運交付，運輸包括推進劑、水、空氣、食物和科研設備等各種有效載荷
國際空間站的軌道修正
國際空間站的垃圾收集與銷毀
圖表4: Astrium的自動運載飛船ATV項目
2.2
SCADE開發(fā)的ATV軟件
自動運載飛船的安全關鍵模塊的軟件開發(fā)使用了SCADE，最初是使用版本V3。
圖為SCADE中定義的類型、常量、軟件架構和可激活塊。
圖表5: Astrium ATV項目中定義的SCADE類型、常量、軟件架構和可激活塊
SCADE定義的狀態(tài)機層級、子狀態(tài)機。
圖表6: Astrium ATV項目中定義的SCADE狀態(tài)機層級、子狀態(tài)機
建模完畢后，除了傳統(tǒng)的驗證活動外，Astrium公司還使用了法國國家科研中心(CNRS)以嵌入式系統(tǒng)研究著稱的VERIMAG實驗室的工具LESAR進行基于SCADE模型的形式化分析。LESAR工作原理同后期SCADE內嵌入的Prover工具一樣。(可參考 嵌入式系統(tǒng) | 基于SCADE模型的形式化方法 一文)。最后將SCADE模型生成代碼，在項目中應用。
展開 嵌入式系統(tǒng) | Ansys SCADE在空客電傳飛控系統(tǒng)中的應用
當前Ansys公司SCADE Suite產(chǎn)品中含有該模塊。
圖表19：PowerPC MPC755 aiT/WECT
Stackanalyzer
Stackanalyzer是AbsInt公司的工具。以二進制形式分析程序堆棧的使用，計算實際內存使用量的上限。該靜態(tài)分析有助于證明沒有程序執(zhí)行引起的堆棧溢出。當前Ansys公司SCADE Suite產(chǎn)品中含有該模塊。
Lesar
Lesar是使用二元決策圖(BDD: Binary Decision Diagram)對基于Lustre語言模型進行模型檢查的工具，其算法用于枚舉可達狀態(tài)。
L4/-Tool/Lucifer/SCADE Designer Verifier
L4是Prover Technology公司開發(fā)的可對SCADE模型進行形式化驗證的插件，可提供類似Lucifer的功能，但界面更加友好，可以與SCADE集成開發(fā)環(huán)境無縫連接。
-Tools是Prover Technology公司基于St?lmarck證據(jù)流程的的通用驗證工具。
L4、-Tools和Lucifer都是Prover Technology公司提供的針對SCADE模型進行形式化驗證的早期版本。只能處理整型數(shù)據(jù)類型。
展開 