由于安全關(guān)鍵系統(tǒng)的全生命周期會(huì)長達(dá)幾十年，再考慮到后期的維護(hù)、改造和升級(jí)費(fèi)用，傳統(tǒng)方式設(shè)計(jì)的軟件成本幾乎不可控制。有什么工具和技術(shù)，能在現(xiàn)代安全關(guān)鍵系統(tǒng)的軟件規(guī)模急劇增長的前提下，既能保證系統(tǒng)的安全可靠，又能適當(dāng)降低設(shè)計(jì)的復(fù)雜度，還能在開發(fā)階段的前期檢測(cè)出缺陷，以減少開發(fā)成本呢？這就不得不提到Ansys SCADE系列產(chǎn)品。

SCADE誕生于上世紀(jì)80年代的法國，從歐洲的航空與核能領(lǐng)域的工程應(yīng)用起步，經(jīng)過近40年的發(fā)展，現(xiàn)代SCADE已經(jīng)是融合了Esterel、Lustre、SAO\SAGA、Lucid Synchrone等多個(gè)語言和工具的集大成之作。由于SCADE專注于流程規(guī)范、標(biāo)準(zhǔn)嚴(yán)苛的安全關(guān)鍵行業(yè)，行業(yè)的特性使得其多應(yīng)用于研制具有相當(dāng)密級(jí)的、高難度的重大項(xiàng)目。因此，盡管進(jìn)入中國市場(chǎng)已有10多年，其知名度卻一般。

在逐漸成為航空航天、國防軍工、軌道交通、核能重工、汽車電子等安全關(guān)鍵行業(yè)里具有廣泛的商業(yè)應(yīng)用的同時(shí)，SCADE也是產(chǎn)學(xué)研相結(jié)合的一個(gè)典范，SCADE研發(fā)團(tuán)隊(duì)中脫穎而出的法國科學(xué)院院士和圖靈獎(jiǎng)獲得者就是對(duì)該產(chǎn)品的一種絕佳肯定。本文將主要介紹SCADE的起源，發(fā)展，現(xiàn)狀和展望，在后續(xù)系列文章中也將對(duì)國外多家知名企業(yè)的SCADE應(yīng)用情況做詳細(xì)介紹，希望以此讓大家對(duì)SCADE產(chǎn)品和行業(yè)應(yīng)用有更好的認(rèn)識(shí)。

在上世紀(jì)80年代早期，Jean-Paul Marmorat和Jean-Paul Rigault，這兩位在巴黎高等礦業(yè)學(xué)校(Ecole des Mines de Paris)研究控制理論和計(jì)算機(jī)科學(xué)的學(xué)者,他們?cè)谠O(shè)計(jì)機(jī)器人汽車的過程中，受困于傳統(tǒng)編程語言不太適合寫出精確的控制邏輯，因此專門設(shè)計(jì)了一種新的語言，而這就是SCADE語言的雛形。

不久，在巴黎索菲亞科技園(Sophia-Antipolis)，由研究所主任Gerard Berry帶領(lǐng)的國立巴黎高科礦業(yè)學(xué)院和法國國立計(jì)算機(jī)及自動(dòng)化研究院(INRIA)所組成的聯(lián)合團(tuán)隊(duì)學(xué)者也逐漸加入到這個(gè)語言的開發(fā)中來，并以索菲亞科技園旁風(fēng)景秀麗的Esterel山命名該語言（Esterel山也與以電影節(jié)聞名于世的法國南部小城戛納相距不遠(yuǎn)）。

與此同期，位于格勒諾布爾(Grenoble)的法國國家科學(xué)研究院(CNRS)的Paul Caspi和Nicolas Halbwachs兩位學(xué)者共同發(fā)明了Lustre語言，Lustre語言是開源的，而且是一種形式的語言，在學(xué)術(shù)領(lǐng)域有較多研究。

在上世紀(jì)80年代中期，Gerard Berry團(tuán)隊(duì)的Laurent Cosserat、Philippe Couronné和Georges Gonthier相繼開發(fā)出了Esterel版本1/2/3。其中版本2引入了Gerard Berry與貝爾實(shí)驗(yàn)室的Ravi Sethi共同設(shè)計(jì)的算法，能將正則表達(dá)式轉(zhuǎn)換為自動(dòng)機(jī)(automata)。版本3開始逐步走向?qū)嵱没?，在Dassault Aviation和Bertin兩家公司有了成功實(shí)踐后，Esterel語言已能在中小規(guī)模的項(xiàng)目上應(yīng)用。

位于法國格勒諾布爾的Merlin-Gerin公司，即后來的施耐德電氣公司(Schneider-Electric)，正承擔(dān)為法國電力公司研制名為SPIN(integrated nuclear protection system)的反應(yīng)堆保護(hù)系統(tǒng)，用于檢測(cè)和緊急制動(dòng)法國新型核電站反應(yīng)堆。由于該系統(tǒng)的軟件需要滿足安全關(guān)鍵的要求，而市場(chǎng)上沒有合適的COTS產(chǎn)品用于開發(fā)，Merlin-Gerin管理層不得不決定自己研制一套開發(fā)工具。

Merlin-Gerin公司聘請(qǐng)Lustre語言研發(fā)團(tuán)隊(duì)的兩位成員Eric Pilaud和Jean-Louis Bergerand為負(fù)責(zé)人，開發(fā)了名為SAGA (Assisted Specification and Automatic Generation) 的工具。SAGA工具是基于Lustre語言設(shè)計(jì)的，可以混合圖形和文本語法進(jìn)行編程，并含有一個(gè)簡(jiǎn)單而高效的代碼生成器。不久，SAGA工具大獲成功，順利開發(fā)出了SPIN N4系列產(chǎn)品，并相繼應(yīng)用到了法國四個(gè)1450 MWe機(jī)組(N4 PWR)以及法國原子能委員會(huì)的幾個(gè)研究堆。

在上世紀(jì)80年代末期，三大同步語言研究小組—Gerard Berry在索菲亞科技園的Esterel團(tuán)隊(duì)，Nicolas Halbwachs和Paul Caspi在格勒諾布爾的Lustre團(tuán)隊(duì)，Albert Benveniste和Paul Le Guernic在雷恩的Signal團(tuán)隊(duì)，三方通力協(xié)作相互借鑒，共同確立了同步語言編程的特點(diǎn)。

Lustre、Signal和Esterel三種同步語言

到了上世紀(jì)90年代早期，數(shù)字設(shè)備巴黎研究實(shí)驗(yàn)室的Jean Vuillemin團(tuán)隊(duì)正在開發(fā)基于Perle FPGA的設(shè)備，以期應(yīng)用于基于Alpha工作站的快速協(xié)處理器。同大部分硬件設(shè)計(jì)團(tuán)隊(duì)一樣，盡管很清楚基于數(shù)據(jù)流的硬件設(shè)計(jì)，但苦于無法有效地開發(fā)出包含大量門電路和寄存器的控制密集型復(fù)雜設(shè)計(jì)，于是他們寄希望于Esterel語言。于是Gerard Berry以咨詢顧問的身份加入Jean Vuillemin團(tuán)隊(duì)，并成功設(shè)計(jì)了Esterel語言到電路的高效直接轉(zhuǎn)換，同時(shí)避免了Esterel版本3中對(duì)大規(guī)模項(xiàng)目的狀態(tài)空間異常暴漲問題。這種新方法對(duì)Esterel語言的軟件應(yīng)用產(chǎn)生了決定性的影響，確保Estererl語言可推廣到更大規(guī)模的應(yīng)用程序開發(fā)。經(jīng)過改進(jìn)和優(yōu)化，Esterel版本4也于1992年正式發(fā)布。

版本4雖然解決了版本3中因程序規(guī)模增大后狀態(tài)空間暴漲的問題，但是卻增加了額外的因果關(guān)系方面的約束，限制了用戶在循環(huán)設(shè)計(jì)方面的應(yīng)用習(xí)慣。1995年前后，Gerard Berry參考了普林斯頓大學(xué)電機(jī)工程學(xué)院Sharad Malik教授關(guān)于循環(huán)電路的論文，并沿用了加州理工大學(xué)Tom Shiple關(guān)于布爾電路的觀點(diǎn)，逐漸加深了對(duì)因果關(guān)系的理解。新增了構(gòu)建語義 (constructive semantics) ，并最終開發(fā)出了Esterel版本5。

位于以色列雷霍沃特(Rehovot)魏茲曼科學(xué)院(the Weizmann institute of Science)的David Harel教授在上世紀(jì)80年代發(fā)表過圖形化狀態(tài)機(jī)StateChart的設(shè)計(jì)，但是StateChart不太適用于涉及通信、并發(fā)、搶占功能的反應(yīng)式系統(tǒng)。在StateChart基礎(chǔ)上，CNRS成員兼Nice-Sophia Antipolis大學(xué)I3S實(shí)驗(yàn)室教授Charles André發(fā)表了符合同步假設(shè)的圖形化狀態(tài)機(jī)SyncChart。1997年，Esterel團(tuán)隊(duì)用Ocaml語言開發(fā)了scg2strl工具，支持將SyncChart轉(zhuǎn)換為Esterel語言，在進(jìn)行模塊化改進(jìn)后形成了Esterel版本6。版本6在達(dá)索航空，泰雷茲，Thomson CSF公司等多個(gè)項(xiàng)目上都有成功的應(yīng)用案例。

90年代末期，Gerard Berry與Intel公司的Michael Kishinevsky先生開始合作擴(kuò)展Esterel語言，使其可以定義任何類型的真實(shí)同步電路。這需要語言定義的深度擴(kuò)展及修改新的編譯功能，以便能夠支持任意的數(shù)據(jù)路徑和位操作結(jié)構(gòu)等內(nèi)容，這些工作為后來Esterel版本7的發(fā)布奠定了堅(jiān)實(shí)的基礎(chǔ)。

同期，Merlin-Gerin公司逐漸感到疲于長期投入資源來研制并維護(hù)SAGA工具，就與位于圖盧茲的Verilog軟件公司協(xié)作，進(jìn)行SAGA工具的商業(yè)化開發(fā)。有趣的是，當(dāng)時(shí)同樣位于圖盧茲的Aerospatiale公司，現(xiàn)在屬于Airbus集團(tuán)，在開發(fā)空客A320機(jī)型的線傳飛控系統(tǒng)(fly-by-wire flight control)時(shí)，遇到與Merlin-Gerin公司相同的安全關(guān)鍵方面的問題，并因此也設(shè)計(jì)了一個(gè)內(nèi)部工具SAO(Computer Assisted Specification)，SAO也具備自動(dòng)代碼生成功能。

在獲悉相關(guān)情況后，Verilog公司牽頭聯(lián)系了Aerospatiale公司，并協(xié)商成立了由Aerospatiale公司，Merlin-Gerin公司和Verilog公司三方合作的共同體，并最終研制出了綜合SAGA和SAO功能的新工具——SCADE。

1993年，Verilog公司與CNRS的Lustre團(tuán)隊(duì)合作創(chuàng)立了VERIMAG聯(lián)合實(shí)驗(yàn)室，Verilog公司聘請(qǐng)VERIMAG實(shí)驗(yàn)室的Daniel Pilaud負(fù)責(zé)領(lǐng)導(dǎo)SCADE團(tuán)隊(duì)。不久SCADE工具成功地應(yīng)用到了歐直的EC135/155，空客的A340-600機(jī)型，Thales Rail Signaling System的香港地鐵等項(xiàng)目。后來Daniel Pilaud根據(jù)在Aerospatiale公司合作的成果，與INRIA的Alain Deutsch博士創(chuàng)立了PolySpace Technologies公司，2007年P(guān)olySpace Technologies公司被Mathworks公司并購。而VERIMAG聯(lián)合實(shí)驗(yàn)室的創(chuàng)始人Joseph Sifakis博士由于“在將Model Checking發(fā)展為被硬件和軟件業(yè)中所廣泛采納的高效驗(yàn)證技術(shù)上的卓越貢獻(xiàn)”獲得了2007年的圖靈獎(jiǎng)。

在90年代中后期，瑞典的Prover-Technology與SCADE團(tuán)隊(duì)合作，通過采用同步觀察(Synchronous Observers)技術(shù)來定義屬性(Properties)和假設(shè)(Assumptions)等約束，將其基于可滿足性問題(SAT-based)設(shè)計(jì)的工具Prover嵌入到SCADE產(chǎn)品中，極大地提升了SCADE產(chǎn)品的驗(yàn)證能力，從此SCADE具有了在模型級(jí)進(jìn)行形式化驗(yàn)證的功能。90年代末期Verilog公司先被法國CS集團(tuán)并購，又被瑞典Telelogic公司并購。

成立于1984年的Simulog公司是從INRIA分拆出來的，包括Gerard Berry在內(nèi)的許多INRIA學(xué)者都是Simulog的聯(lián)合創(chuàng)始人，Simulog公司是INRIA科研成果成功轉(zhuǎn)化的案例之一。Simulog公司開始負(fù)責(zé)將Esterel產(chǎn)品商業(yè)化。

1999年，Simulog公司分拆出Esterel語言相關(guān)產(chǎn)品，成立了愛斯特爾技術(shù)公司 (Esterel Technologies) 。Gerard Berry教授作為愛斯特爾技術(shù)公司首席科學(xué)家(Chief Scientist Officer)于2002年榮膺法國科學(xué)院院士，之后相繼獲得法國技術(shù)研究院院士，歐洲科學(xué)院院士。

2001年，愛斯特爾技術(shù)公司并購了Telelogic公司的SCADE業(yè)務(wù)，開始著手融合Esterel語言和基于Lustre語言的SCADE產(chǎn)品。由于Lustre是聲明式的，側(cè)重描述數(shù)據(jù)流，但不支持狀態(tài)機(jī)；Esterel語言是命令式的，側(cè)重描述控制流，但支持的狀態(tài)機(jī)SyncState較復(fù)雜，不宜通過認(rèn)證。于是愛斯特爾技術(shù)公司決定通過幾個(gè)同步語言概念的借鑒與融合，形成新的SCADE語言。

這項(xiàng)研發(fā)的學(xué)術(shù)方面工作由時(shí)任巴黎第十一大學(xué)的Marc Pouzet教授，與愛斯特爾技術(shù)公司的Jean-Louis Calaco和Bruno Pagano共同完成。Marc Pouzet教授使用其設(shè)計(jì)的融合Lustre語言和ML語言(函數(shù)式編程語言)兩者特性的Lucid Synchrone語言擴(kuò)展了SCADE語言，其中的ReLuC編譯器是新版SCADE語言對(duì)應(yīng)的代碼生成器(KCG)的原型，該編譯器也是用Ocaml語言編寫。

另外，在新版SCADE語言中除了添加狀態(tài)機(jī)功能之外，愛斯特爾技術(shù)公司還新增了勒諾布爾大學(xué)Florence Maraninchi教授設(shè)計(jì)的迭代器(用于循環(huán)設(shè)計(jì))等一系列高階運(yùn)算功能，新增了由UPMC，INRIA，ENS Paris三個(gè)機(jī)構(gòu)聯(lián)合成立的PARKAS小組設(shè)計(jì)的Zelus語言中關(guān)于常微分方程擴(kuò)展功能等。值得一提的是，Marc Pouzet教授獲得了2016年度INRIA創(chuàng)新獎(jiǎng)，表彰他在同步語言領(lǐng)域的精深造詣，以及為推動(dòng)SCADE語言發(fā)展做出的卓越貢獻(xiàn)。

2005年愛斯特爾技術(shù)公司擴(kuò)展了SCADE品牌，SCADE旨在成為面向安全關(guān)鍵嵌入式領(lǐng)域的、基于模型的、覆蓋全生命周期應(yīng)用的工具。原SCADE產(chǎn)品更名為SCADE Suite，適用于控制軟件的邏輯建模。

2006年愛斯特爾技術(shù)公司收購了Thales Avionics和Diehl Aerospace聯(lián)合研制的嵌入式圖形顯示設(shè)計(jì)工具IMAGEIMAGE，并重新定義品牌名為SCADE Display。原IMAGE工具曾經(jīng)在空客的A380和A400M，達(dá)索航空的陣風(fēng)戰(zhàn)機(jī)，蘇霍伊的支線客機(jī)等項(xiàng)目上有成功應(yīng)用。

2009年愛斯特爾技術(shù)公司與CEA LIST研究所組成了名為LISTEREL Critical Software Lab聯(lián)合研發(fā)實(shí)驗(yàn)室。不久該實(shí)驗(yàn)室推出了基于SysML語言的架構(gòu)設(shè)計(jì)工具，并定義品牌名為SCADE System，后又更名為SCADE Architect。區(qū)別于傳統(tǒng)基于SysML的架構(gòu)設(shè)計(jì)工具，SCADE Architect支持在SysML的基礎(chǔ)進(jìn)行封裝定制，擴(kuò)展出了符合ARP 4754A流程的航空嵌入式系統(tǒng)設(shè)計(jì)解決方案 (支持導(dǎo)出符合ARINC 429,ARINC 664，ARINC 653等協(xié)議的ICD；支持基于AADL 2.2版本對(duì)航電非功能屬性進(jìn)行建模、實(shí)現(xiàn)虛擬系統(tǒng)的集成；支持FACE: Future Airborne Capability Environment架構(gòu)(最高3.0版本))、擴(kuò)展出了符合ISO 26262流程的汽車嵌入式系統(tǒng)設(shè)計(jì)解決方案(支持AUTOSAR標(biāo)準(zhǔn))。

同年，為了專注于安全關(guān)鍵系統(tǒng)領(lǐng)域的業(yè)務(wù)，愛斯特爾技術(shù)公司將研制多年的旨在簡(jiǎn)化電子系統(tǒng)級(jí)(ESL)設(shè)計(jì)和系統(tǒng)級(jí)芯片(SoC)設(shè)計(jì)的EDA工具Esterel Studio 出售給了Synfora公司。而2010年，Synopsys公司又收購了Synfora公司。盡管如此，SCADE依然可以通過定制與部分硬件設(shè)計(jì)語言進(jìn)行橋接或轉(zhuǎn)換。

2011年愛斯特爾技術(shù)公司推出SCADE Lifecycle產(chǎn)品，用于幫助系統(tǒng)和軟件開發(fā)人員進(jìn)行產(chǎn)品的全生命周期管理。

2012年愛斯特爾技術(shù)公司推出SCADE ARINC 661解決方案，可用于符合ARINC 661標(biāo)準(zhǔn)的交互式座艙顯示系統(tǒng)的設(shè)計(jì)。SCADE ARINC 661是業(yè)內(nèi)唯一的、以基于模型的方式完全實(shí)現(xiàn)ARINC 661標(biāo)準(zhǔn)版本4和版本5中定義的所有控件 (Widget)的解決方案。當(dāng)前兼容支持的最高版本為ARINC 661版本6(含93個(gè)Widget，15個(gè)Extension) 。

同年，Ansys收購愛斯特爾技術(shù)公司，并將其歸于Ansys的系統(tǒng)事業(yè)部(System Business Unit)。

2015年Ansys發(fā)布了SCADE R16版本，從這時(shí)開始SCADE品牌產(chǎn)品的版本號(hào)同Ansys所有產(chǎn)品的版本號(hào)保持一致。

SCADE版本與發(fā)布年份的關(guān)系

2016年Ansys推出了SCADE Test產(chǎn)品，用于實(shí)現(xiàn)基于模型的軟件驗(yàn)證。SCADE Test中包含可通過DO-178C/DO-331 TQL-5級(jí)工具鑒定的自動(dòng)化的認(rèn)證測(cè)試環(huán)境 (QTE: Qualified Test Environment) 。支持在開發(fā)平臺(tái)上對(duì)SCADE Suite模型和SCADE Display進(jìn)行功能測(cè)試(含圖形的像素比對(duì)功能)和覆蓋分析(含模型級(jí)和代碼級(jí)覆蓋分析結(jié)果)；支持與主流目標(biāo)機(jī)測(cè)試平臺(tái)的橋接，重用模型級(jí)的測(cè)試用例。

2019年Ansys推出了品牌名為SCADE Vision的基于AI感知的系統(tǒng)測(cè)試產(chǎn)品，該產(chǎn)品是Ansys與美國卡內(nèi)基梅隆大學(xué)聯(lián)合開發(fā)的AI智能感知算法驗(yàn)證套件。SCADE Vision是基于網(wǎng)絡(luò)前端Web圖形界面和云端部署的后臺(tái)搜索引擎的，允許用戶配置輸入視頻/圖像存儲(chǔ)庫、感知算法/待測(cè)卷積神經(jīng)網(wǎng)絡(luò) (CNN: Convolutional Neural Network) 等，可自動(dòng)識(shí)別包括自動(dòng)駕駛車輛在內(nèi)的各類感知系統(tǒng)中的潛在漏洞，幫助用戶查找和分類這些系統(tǒng)中可能出現(xiàn)不安全行為的邊界狀況，有效降低AI智能感知算法的驗(yàn)證效率并快速定位AI智能感知算法的潛在缺陷。

2020年Ansys發(fā)布了SCADE 2020版本。

通過以上發(fā)展歷史回顧可以看出，SCADE系列產(chǎn)品是伴隨著眾多理論研究和工程領(lǐng)域的實(shí)踐應(yīng)用而逐步發(fā)展起來的。現(xiàn)代SCADE語言至少綜合了圖表2所示6種語言的特性，這也奠定了其堅(jiān)實(shí)的理論基礎(chǔ)。

SCADE語言的淵源

注：Lustre語言是開源的，在學(xué)術(shù)領(lǐng)域有較多研究。SCADE語言可認(rèn)為是由Lustre語言發(fā)展而來的商業(yè)化版本之一，但SCADE語言包含更多的特性，可無縫連接Ansys的相關(guān)產(chǎn)品，不論在商業(yè)領(lǐng)域還是軍事領(lǐng)域，都有更多成功的大型工程應(yīng)用。

Lustre語言及其派生的語言和工具

相對(duì)于單核處理器的局限性，多核(Multi-Core)處理器由于其更高的能效逐漸被考慮用于安全關(guān)鍵領(lǐng)域。SCADE多核相關(guān)的研發(fā)計(jì)劃是：生成可在多核目標(biāo)上高效執(zhí)行的代碼，并依然保留原有的精確、無歧義的、確定性語義和平臺(tái)無關(guān)性。當(dāng)前主要與Infineon Aurix (Hightec)，Kalray MPPA (Kalray)和SYSGO PikeOS (S3P)幾款產(chǎn)品合作，已根據(jù)部分客戶的需求有了方案應(yīng)用，未來將在工業(yè)實(shí)踐中使該功能商業(yè)化。

SCADE多核代碼生成器工作流

在形式化方法領(lǐng)域，主要的開發(fā)目標(biāo)是將Prover Technology與RATP兩家公司創(chuàng)立的HLL語言融入新版本產(chǎn)品的形式化流程中。HLL語言有助于在安全關(guān)鍵系統(tǒng)領(lǐng)域中使用模型檢查技術(shù)進(jìn)行形式化驗(yàn)證，當(dāng)前主要有Prover Technology，RATP，Systerel，SafeRiver，Ansys五家公司參與到HLL語言相關(guān)的工作中。

在人工智能領(lǐng)域，主要的開發(fā)目標(biāo)是將傳統(tǒng)的基于模型的開發(fā)驗(yàn)證流程與新型AI研發(fā)流程相結(jié)合。當(dāng)前的主要合作伙伴是空客，將在未來歐洲設(shè)想的未來空中作戰(zhàn)系統(tǒng)(FCAS: Future Combat Air System)的高級(jí)無人機(jī)飛行控制系統(tǒng)中率先應(yīng)用該項(xiàng)創(chuàng)新。

[1]    Halbwachs N. A synchronous language at work: the story of Lustre[C]//Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2005. MEMOCODE'05. IEEE, 2005: 3-11.

[2]    Berry G. The constructive semantics of pure Esterel[J]. 1999.

[3]    Halbwachs N, Caspi P, Raymond P, et al. The synchronous data flow programming language LUSTRE[J]. Proceedings of the IEEE, 2002, 79(9):1305-1320.

[4]    Benveniste A, Caspi P, Edwards S A, et al. The synchronous languages 12 years later[J]. Proceedings of the IEEE, 2003, 91(1):64-83.

[5]    Bergerand J L, Pilaud E. SAGA: A Software Development Environment for Dependability Automatic Controls[J]. Ifac Proceedings Volumes, 1988, 21(18):11-16.

[6]    Harel D. Statecharts: a visual formalism for complex systems[J]. Science of Computer Programming, 1987, 8(3):231-274.

[7]    Charles A. Representation and analysis of reactive behaviors: A synchronous approach[C]//Computational Engineering in Systems Applications, CESA. 1996, 96: 19-29.

[8]    Pilaud D. Example of technologies push in the embedded market[J]. 1999.

[9]    Cola?o J L, Pagano B, Pouzet M. A conservative extension of synchronous data-flow with state machines[C]//Proceedings of the 5th ACM international conference on Embedded software. ACM, 2005: 173-182..

[10]  Maraninchi F, Morel L. Arrays and contracts for the specification and analysis of regular systems[C]//Proceedings. Fourth International Conference on Application of Concurrency to System Design, 2004. ACSD 2004. IEEE, 2004: 57-66.

[11] Verimag Laboratory. Lustre, a Synchronous Dataflow Language. [EB/OL].http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/doc/lustre.pdf

[12] Cola?o J L, Pagano B, Pasteur C, et al. Scade 6: from a Kahn Semantics to a Kahn Implementation for Multicore[C]//2018 Forum on Specification & Design Languages (FDL). IEEE, 2018: 5-16.

[13] Beno?t Dupont de Dinechin. MPPA Manycore Processor:At the heart of Intelligent Systems. [EB/OL]. https://www.european-processor-initiative.eu/wp-content/uploads/2019/10/Kalray-NEWCAS-2019.pdf. Jul,2019