SIGNAL模型多線程代碼生成研究*

闞雙龍，黃志球，楊志斌

南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，南京 210016

1　引言

安全攸關(guān)系統(tǒng)是指系統(tǒng)的失效會(huì)導(dǎo)致重大的人員傷亡、財(cái)產(chǎn)損失和環(huán)境污染的一類系統(tǒng)[1]。嵌入式系統(tǒng)定義為由軟件和硬件組成的面向特定任務(wù)的計(jì)算機(jī)系統(tǒng)。很多的安全攸關(guān)嵌入式系統(tǒng)是反應(yīng)式系統(tǒng)，反應(yīng)式系統(tǒng)的特點(diǎn)是這類系統(tǒng)不斷地與外部環(huán)境進(jìn)行交互，每一次交互可以規(guī)約為3個(gè)操作：（1）接收外部環(huán)境輸入；（2）根據(jù)輸入進(jìn)行計(jì)算；（3）將計(jì)算結(jié)果反饋輸出到外部環(huán)境。一次與環(huán)境的交互稱為一次反應(yīng)計(jì)算，整個(gè)系統(tǒng)的計(jì)算由一條反應(yīng)計(jì)算的序列組成[2]。反應(yīng)式系統(tǒng)的特定計(jì)算模式使得部分學(xué)者考慮新的設(shè)計(jì)語言來對(duì)其進(jìn)行建模。

同步語言[3]是針對(duì)反應(yīng)式系統(tǒng)提出的一種系統(tǒng)建模語言。該語言將一次反應(yīng)計(jì)算的時(shí)間抽象為一個(gè)邏輯時(shí)刻。系統(tǒng)的計(jì)算就是一條邏輯時(shí)刻的序列。同步語言是一種具有精確語義的形式化語言，目前已經(jīng)被成功應(yīng)用到工業(yè)界。例如基于同步語言LUSTRE[4]的集成開發(fā)工具SCADE[5]已經(jīng)在空客A380的軟件開發(fā)中得到成功應(yīng)用。

同步語言可以分為兩類：第一類是命令式同步語言（imperative synchronous language），第二類是聲明式同步語言（declarative synchronous language）。

命令式同步語言包括 ESTEREL[6]、Statecharts[7]、Argos[8]、SyncCharts[9]等。其中ESTEREL支持傳統(tǒng)命令式語言的順序、迭代等特性，同時(shí)又支持反應(yīng)式系統(tǒng)對(duì)每一次反應(yīng)計(jì)算的規(guī)約。對(duì)ESTEREL的編譯可以生成自動(dòng)機(jī)[10]和控制流圖[11]等。ESTEREL的典型應(yīng)用包括自動(dòng)化交通、航空航天、國防、鐵路交通等領(lǐng)域的嵌入式設(shè)計(jì)。狀態(tài)圖是一種圖形化的設(shè)計(jì)語言，它的基本特征包括對(duì)嵌入式系統(tǒng)的通信、并發(fā)和層次性進(jìn)行建模。但是狀態(tài)圖本身是一種半形式化的建模語言，已有工作對(duì)其形式語義進(jìn)行定義[12]。Argos是狀態(tài)圖的一種擴(kuò)展，它的特點(diǎn)是比狀態(tài)圖支持更嚴(yán)格的同步語義。SyncCharts同步語言同時(shí)受到ESTEREL和狀態(tài)圖的影響，因此它具有兩者的特征。

聲明式同步語言包括LUSTRE[4]、LUCID Synchrone[13]和SIGNAL[14]。這3類都屬于數(shù)據(jù)流語言，數(shù)據(jù)流語言起源于20世紀(jì)70年代[15]。LUSTRE語言是由法國科學(xué)院Verimag實(shí)驗(yàn)室發(fā)明的同步語言，它是一種函數(shù)式語言，其基本對(duì)象由一系列值和節(jié)點(diǎn)的流組成。一個(gè)流可以定義為由一個(gè)時(shí)刻集合和每一時(shí)刻出現(xiàn)的值組成。LUSTRE建模語言的編譯過程需要對(duì)模型中時(shí)鐘結(jié)構(gòu)的一致性進(jìn)行驗(yàn)證，另外也需要對(duì)模型的調(diào)度約束進(jìn)行驗(yàn)證。LUSTRE語言在航空航天、國防、鐵路等領(lǐng)域的嵌入式軟件中被使用。工業(yè)界的LUSTRE工具SCADE[5]在安全攸關(guān)領(lǐng)域已經(jīng)獲得了成功的應(yīng)用。SCADE可以支持航空安全性標(biāo)準(zhǔn)DO-178B[16]的A級(jí)代碼生成標(biāo)準(zhǔn)。LUCID Synchrone是建立在函數(shù)式語言O(shè)Caml[17]上的一種高階函數(shù)式同步語言。LUCID Synchrone通過類型的計(jì)算來對(duì)同步模型中的抽象時(shí)鐘進(jìn)行演算。SIGNAL是由法國信息自動(dòng)化研究所（INRIA）發(fā)明的一種同步語言，與之前的聲明式同步語言不同，它是一種支持多時(shí)鐘的嵌入式軟件建模語言[2]。該語言描述了事件序列的值，以及不同事件序列之間的同步關(guān)系。多時(shí)鐘系統(tǒng)非常適合對(duì)分布式系統(tǒng)進(jìn)行建模。

同步語言一個(gè)很重要的特點(diǎn)是支持精確的代碼自動(dòng)生成。例如SCADE工具支持LUSTRE同步模型順序代碼（sequential code）的自動(dòng)生成。同步語言SIGNAL由于其多時(shí)鐘特性，可以支持分布式系統(tǒng)的建模，并且可以生成多線程代碼。

本文的貢獻(xiàn)是提出了一種面向同步語言SIGNAL的多線程Java代碼生成方法。選擇SIGNAL的原因是該同步語言是一種多時(shí)鐘同步語言，可以生成多線程代碼（multi-threaded code），適用于分布式系統(tǒng)或者多核系統(tǒng)應(yīng)用的建模。而LUSTRE、LUCID Synchrone屬于單時(shí)鐘同步語言，難以應(yīng)用于分布式或者多核系統(tǒng)，且主要生成順序代碼（sequential code）。相比于已有工作，其主要?jiǎng)?chuàng)新為：基于可重用中間結(jié)構(gòu)——同步時(shí)鐘衛(wèi)式操作（synchronous clock guarded action，S-CGA），研究代碼生成技術(shù)。其他的同步語言可以通過轉(zhuǎn)化到該中間結(jié)構(gòu)，重用該中間結(jié)構(gòu)到多線程Java代碼生成過程。本文采用Java的原因是美國航天局（NASA）已經(jīng)使用Java對(duì)航天器進(jìn)行編程。另外本文工作是團(tuán)隊(duì)已有工作[18-19]的延續(xù)。

本文組織結(jié)構(gòu)如下：第2章給出了SIGNAL語言的基本語法和語義；第3章給出了SIGNAL模型到帶劃分衛(wèi)式操作的轉(zhuǎn)化過程；第4章給出了帶劃分衛(wèi)式操作到Java代碼的生成過程；第5章給出了空客A340警報(bào)系統(tǒng)的實(shí)例分析；第6章為本文相關(guān)工作和結(jié)束語。

2　SIGNAL語言的基本語法和語義

本文所有的基本概念均來自于文獻(xiàn)[2]。同步語言是基于同步時(shí)間模型進(jìn)行定義的。同步時(shí)間模型假設(shè)對(duì)于每一次的計(jì)算，當(dāng)收到一個(gè)輸入事件時(shí)，系統(tǒng)對(duì)該事件的計(jì)算一定在下一個(gè)輸入事件到來之前結(jié)束。圖1給出了同步時(shí)間模型的示意圖。上面的物理時(shí)間軸表示的是周圍環(huán)境，即物理世界的時(shí)間。一次反應(yīng)計(jì)算包含3個(gè)步驟：接收輸入事件；對(duì)輸入進(jìn)行計(jì)算；向環(huán)境輸出響應(yīng)。圖1中包含兩次反應(yīng)計(jì)算。同步時(shí)間模型將每一次反應(yīng)計(jì)算的時(shí)間抽象為一個(gè)時(shí)刻，即計(jì)算持續(xù)時(shí)間為0，稱為邏輯時(shí)間。

同步模型實(shí)際上是一種平臺(tái)無關(guān)模型，它不關(guān)注每一次計(jì)算需要多少時(shí)間，只關(guān)注輸入事件計(jì)算的順序。每一時(shí)刻的計(jì)算稱為一次反應(yīng)計(jì)算。

Fig.1　Synchronous time model圖1　同步時(shí)間模型

同步語言SIGNAL也是基于以上同步時(shí)間模型。SIGNAL包含兩個(gè)重要的概念：信號(hào)和信號(hào)的抽象時(shí)鐘。

定義1（信號(hào)）一個(gè)信號(hào)s定義為一個(gè)全序序列（total order sequence）(st)t∈I，序列中所有的值st為同一類型的值。集合I為自然數(shù)集合N的一個(gè)初始段，也包括空段。

定義2（抽象時(shí)鐘）一個(gè)信號(hào)的抽象時(shí)鐘簡(jiǎn)稱為時(shí)鐘，定義為所有該信號(hào)出現(xiàn)且有值的時(shí)刻的集合。

不同的信號(hào)之間存在著約束關(guān)系，SIGNAL語言定義了4種基本操作來規(guī)約信號(hào)之間的關(guān)系。

（1）瞬時(shí)函數(shù)操作

瞬時(shí)函數(shù)操作定義為sn:=f(s1,s2,…,sn-1)，是一個(gè)n-1元函數(shù)，其中sk定義為一個(gè)信號(hào)，其形式化語義為：

其中，siτ表示信號(hào)si在時(shí)刻τ的值。符號(hào)⊥表示該時(shí)刻值缺失，即該時(shí)刻信號(hào)沒有值。瞬時(shí)函數(shù)要求所有參與的信號(hào)都要有同樣的時(shí)鐘，也就是說所有的信號(hào)要么全部出現(xiàn)且有值，要么全部缺失。圖2給出了瞬時(shí)函數(shù)s3:=s1×s2的值與時(shí)鐘的關(guān)系?？梢钥闯雒恳粫r(shí)刻3個(gè)信號(hào)的值要么全部出現(xiàn)，要么全部缺失（缺失用符號(hào)“.”表示）。并且在每一時(shí)刻3個(gè)信號(hào)的值滿足s3的值為s1的值與s2的值的乘積。瞬時(shí)函數(shù)中的操作可以為普通的算術(shù)操作，包括加、減、乘、除、取模等。

Fig.2　An instance of instantaneous operation圖2　瞬時(shí)操作實(shí)例

（2）延時(shí)操作

延時(shí)操作允許訪問一個(gè)信號(hào)之前時(shí)鐘的值。這里只介紹最簡(jiǎn)單的情況：即給定一個(gè)時(shí)刻t，如何獲得該時(shí)刻的上一個(gè)時(shí)刻的值。延時(shí)操作的語法定義為s2:=s1$1 initc，其中s1和s2為兩個(gè)信號(hào)，c是一個(gè)初始常量，它的類型必須與信號(hào)s2的類型相同。給定一個(gè)時(shí)刻t，s2獲得除了時(shí)刻t之外最近時(shí)刻s1的值，初始時(shí)，s2的值為c。下面給出延時(shí)操作的形式化語義：

與瞬時(shí)函數(shù)相同，延時(shí)操作的兩個(gè)信號(hào)具有相同的時(shí)鐘，圖3給出延時(shí)操作s2:=s1$1 init 3.14的運(yùn)行實(shí)例?？梢钥闯鰞蓚€(gè)信號(hào)具有相同的時(shí)鐘。在初始時(shí)，s2的值為3.14。在其他時(shí)刻s2的值為s1在之前時(shí)刻的值。

Fig.3　An instance of delay operation圖3　延時(shí)操作實(shí)例

（3）條件采樣操作

條件采樣操作支持從一個(gè)信號(hào)中抽取符合一定條件的序列。該操作的語法定義為s2:=s1whenb，其中s1和s2是具有相同類型的信號(hào)，b是一個(gè)布爾信號(hào)。條件采樣的語義定義為：

給出一個(gè)符號(hào)表示，[b]表示信號(hào)b出現(xiàn)且值為true的時(shí)鐘。信號(hào)s2的時(shí)鐘定義為信號(hào)s1的時(shí)鐘和[b]的交，即在任意時(shí)刻如果s2出現(xiàn)，當(dāng)且僅當(dāng)s1和[b]同時(shí)出現(xiàn)。圖4給出了條件采樣操作s2:=s1whenb的運(yùn)行實(shí)例。從圖中可以看出，當(dāng)s2出現(xiàn)的時(shí)候s1和b同時(shí)出現(xiàn)，并且當(dāng)b為真時(shí)，s2的值與s1的值相同。

Fig.4　An instance of undersampling operation圖4　條件采樣運(yùn)行實(shí)例

（4）確定性合并

確定性合并定義了兩個(gè)信號(hào)的交錯(cuò)功能。它的語法定義為s3:=s1defaults2，其中s1、s2和s3是3個(gè)類型相同的信號(hào)。確定性合并的語義定義為：

信號(hào)s3的時(shí)鐘定義為信號(hào)s1的時(shí)鐘和信號(hào)s2的時(shí)鐘的并。圖5給出了確定性合并s3:=s1defaults2的一個(gè)運(yùn)行實(shí)例。在任意時(shí)刻如果s1或s2出現(xiàn)，那么s3出現(xiàn)，并且s1比s2有更高的優(yōu)先級(jí)。

Fig.5　An instance of deterministic merging圖5　確定性合并運(yùn)行實(shí)例

每一基本操作定義了一個(gè)等式。在4個(gè)基本操作的基礎(chǔ)上，介紹進(jìn)程的概念以及進(jìn)程的基本操作。一個(gè)進(jìn)程定義為一個(gè)信號(hào)等式的集合，這些等式由4個(gè)基本操作組成，并且規(guī)約了信號(hào)值和時(shí)鐘之間的關(guān)系。針對(duì)進(jìn)程有兩個(gè)基本的操作：（1）兩個(gè)進(jìn)程的組合操作（composition）；（2）進(jìn)程的局部定義操作（local declaration）。

首先介紹進(jìn)程的組合操作。對(duì)于兩個(gè)進(jìn)程P和Q，它們的組合操作定義為P|Q。P|Q將P和Q中的進(jìn)程進(jìn)行了合并，規(guī)約了P和Q中所有信號(hào)的關(guān)系，信號(hào)的時(shí)鐘之間的關(guān)系以及信號(hào)值之間的關(guān)系。例如：s2:=N*s1|cond:=s2>32是兩個(gè)進(jìn)程的組合。信號(hào)s2計(jì)算的值，將在cond的計(jì)算中被使用。在一次反應(yīng)計(jì)算過程中s2和cond按依賴關(guān)系逐次被計(jì)算，并且它們的組合規(guī)約了s2的時(shí)鐘和cond是同一時(shí)鐘。

下面介紹局部定義。局部定義的語法為：Pwhere type_1s_1;…;type_n s_n;end，其中P為一個(gè)進(jìn)程，s_1,…,s_n為n個(gè)信號(hào)。信號(hào)s_1,…,s_n的作用域局限在進(jìn)程P之內(nèi)，即只有在進(jìn)程P之內(nèi)才可以使用這些信號(hào)。這和程序設(shè)計(jì)語言中的局部變量有相似的含義。

“高校固定資產(chǎn)管理平臺(tái)”的使用，推進(jìn)了固定資產(chǎn)管理工作的信息化進(jìn)程，也促進(jìn)了高校數(shù)字校園的建設(shè)，實(shí)現(xiàn)對(duì)固定資產(chǎn)的動(dòng)態(tài)管理，同時(shí)也真實(shí)反映學(xué)校的固定資產(chǎn)及財(cái)務(wù)狀況。

進(jìn)程框架的格式如圖6（a）所示。該模型包括：（1）一個(gè)接口，包含進(jìn)程的名稱，在關(guān)鍵字process之后定義；一組參數(shù)，參數(shù)是一組在編譯時(shí)就可以確定的常量；一組輸入信號(hào)在“?”之后和一組輸出變量在符號(hào)“!”之后。（2）主體，包括進(jìn)程的內(nèi)部行為和一些局部信號(hào)的定義。一個(gè)進(jìn)程框架定義了一個(gè)進(jìn)程模型，包括了輸入和輸出。圖6（b）給出一個(gè)進(jìn)程框架的例子。它包括參數(shù)N，輸入信號(hào)s1和輸出信號(hào)cond。主體行為中包含了對(duì)兩個(gè)進(jìn)程的組合。信號(hào)s2是局部信號(hào)，只能在進(jìn)程P1中使用。

Fig.6　Process framework and an instance圖6　進(jìn)程框架及其實(shí)例

3　SIGNAL到帶劃分衛(wèi)式操作轉(zhuǎn)化

本文代碼自動(dòng)生成技術(shù)給出從SIGNAL模型到多線程Java代碼的轉(zhuǎn)化過程。整個(gè)轉(zhuǎn)化過程涉及如下3個(gè)中間結(jié)構(gòu)：同步時(shí)鐘衛(wèi)式操作（S-CGA），衛(wèi)式操作（guarded action，GA），帶劃分的衛(wèi)式操作（guarded action with clusters，GACL）。其中S-CGA為可重用中間結(jié)構(gòu)，即其他的同步語言也可以轉(zhuǎn)化為該中間結(jié)構(gòu)。整個(gè)轉(zhuǎn)化過程分為以下幾個(gè)步驟：

（1）SIGNAL模型到S-CGA的轉(zhuǎn)化；

（2）S-CGA到GA的轉(zhuǎn)化；

（3）GA到GACL的轉(zhuǎn)化；

（4）GACL到多線程Java代碼的轉(zhuǎn)化。

本章只關(guān)注步驟（1）、（2）、（3）。步驟（4）在第4章進(jìn)行詳細(xì)介紹。為了更好地對(duì)轉(zhuǎn)化過程進(jìn)行說明，本文以圖7的運(yùn)行實(shí)例對(duì)整個(gè)轉(zhuǎn)化過程進(jìn)行說明。圖7中需要說明的是符號(hào)“^=”，該符號(hào)表示兩個(gè)信號(hào)的時(shí)鐘相同。實(shí)際上它們可以使用基本操作表達(dá)。例如可以表示為以下3個(gè)瞬時(shí)函數(shù)操作：

Fig.7　Arunning example of SIGNAL model圖7　一個(gè)SIGNAL運(yùn)行實(shí)例

3.1　SIGNAL到S-CGA轉(zhuǎn)化

本節(jié)給出SIGNAL模型到中間結(jié)構(gòu)S-CGA的轉(zhuǎn)化過程。首先給出S-CGA的定義，然后針對(duì)每一個(gè)SIGNAL操作給出對(duì)應(yīng)的S-CGA轉(zhuǎn)化規(guī)則。

定義3（S-CGA）S-CGA定義為一個(gè)變量集合X上的衛(wèi)式操作集合，每一個(gè)變量都有自己的時(shí)鐘，對(duì)于一個(gè)變量x∈X，它的時(shí)鐘表示為x?，又稱為時(shí)鐘變量，每一個(gè)衛(wèi)式操作定義為以下5種形式之一：

從SIGNAL模型到S-CGA的轉(zhuǎn)化是比較直接的且上下文無關(guān)，即針對(duì)每一條SIGNAL語句將其對(duì)應(yīng)轉(zhuǎn)化為相應(yīng)的S-CGA語句。對(duì)應(yīng)的轉(zhuǎn)化規(guī)則如表1所示。

Table 1　Translation rules from SIGNAL to S-CGA表1　SIGNAL到S-CGA轉(zhuǎn)化規(guī)則

圖7的SIGNAL運(yùn)行實(shí)例經(jīng)過該步的轉(zhuǎn)化可以得到對(duì)應(yīng)的S-CGA。具體的S-CGA如圖8所示。這里需要解釋的是（13）、（14）行它們分別對(duì)應(yīng)x1^=x2和x1^=y2，實(shí)際上它們被簡(jiǎn)化了。例如（13）行的完整寫法為t1:=(x1=x1);t2;=(x2=x2);t1:=t2。

Fig.8　S-CGAof running example圖8　運(yùn)行實(shí)例的S-CGA

3.2　S-CGA到GA的轉(zhuǎn)化

從S-CGA到GA的轉(zhuǎn)化需要考慮S-CGA中的時(shí)鐘信息。因?yàn)镾-CGA和SIGNAL中的所有變量一一對(duì)應(yīng)，所以S-CGA中的時(shí)鐘信息和SIGNAL中的時(shí)鐘信息等價(jià)。時(shí)鐘信息的表現(xiàn)形式為時(shí)鐘層次（clock hierarchy），時(shí)鐘層次被用來消除S-CGA中的時(shí)鐘變量。另外從S-CGA到GA轉(zhuǎn)化需要對(duì)特殊符號(hào)next和init進(jìn)行處理。因?yàn)橐延械某绦蛟O(shè)計(jì)語言，例如C、C++和Java等，都不存在時(shí)鐘的概念以及符號(hào)next和init，只有消除這些符號(hào)才能有效地進(jìn)行代碼生成。

定義4（時(shí)鐘層次）時(shí)鐘層次定義為由一組節(jié)點(diǎn)組成的樹形結(jié)構(gòu)，每一個(gè)節(jié)點(diǎn)是一組時(shí)鐘等價(jià)類，只有一個(gè)全局時(shí)鐘作為樹的根節(jié)點(diǎn)，在父節(jié)點(diǎn)和子節(jié)點(diǎn)之間存在著時(shí)鐘蘊(yùn)含關(guān)系，即如果一個(gè)時(shí)刻在子節(jié)點(diǎn)的時(shí)鐘內(nèi)，那么該時(shí)刻一定在其父節(jié)點(diǎn)的時(shí)鐘內(nèi)。

SIGNAL中時(shí)鐘層次的詳細(xì)求解方法可以參考文獻(xiàn)[20]，本節(jié)對(duì)運(yùn)行實(shí)例的時(shí)鐘層次進(jìn)行分析，給出消除時(shí)鐘變量的方法。圖9給出圖7中SIGNAL模型的時(shí)鐘層次。它包含有4個(gè)時(shí)鐘等價(jià)類C0、C1、C2、C3。等價(jià)類中每一個(gè)元素都表示一個(gè)時(shí)鐘。例如表示s1的時(shí)鐘，表示全局時(shí)鐘除去s1的時(shí)鐘，[x1]表示當(dāng)x1出現(xiàn)并且其值為真的時(shí)鐘。用這些時(shí)鐘等價(jià)類可以表示所有S-CGA衛(wèi)式條件中的時(shí)鐘變量。在得到時(shí)鐘層次之后，可以對(duì)S-CGA中的時(shí)鐘變量進(jìn)行消除。利用時(shí)鐘層次消除時(shí)鐘變量主要包含以下兩個(gè)步驟：

（1）使用全局時(shí)鐘和其他非時(shí)鐘變量定義已有的時(shí)鐘等價(jià)類，這樣每一個(gè)時(shí)鐘等價(jià)類可以用一個(gè)由全局時(shí)鐘和非時(shí)鐘變量組成的表達(dá)式表示，這里稱之為時(shí)鐘表達(dá)式。

（2）針對(duì)每一個(gè)S-CGA中的衛(wèi)式操作，用true代替時(shí)鐘表達(dá)式中的全局時(shí)鐘，用時(shí)鐘表達(dá)式代替時(shí)鐘變量。

Fig.9　Clock hierarchy of running example圖9　運(yùn)行實(shí)例的時(shí)鐘層次

針對(duì)圖9中的時(shí)鐘層次，介紹時(shí)鐘變量約簡(jiǎn)方法。C0是全局時(shí)鐘。C1的時(shí)鐘可以表示為C1=C0∧x1，C2的時(shí)鐘可以表示為C2=C0∧x2,C3的時(shí)鐘可以表示為C3=?C1∧C2=?x1∧x2。如果將C0設(shè)置為真，那么4個(gè)時(shí)鐘等價(jià)類可以表示為：C0=true,C1=true∧x1=x1，C2=true∧x2=x2，C3=true∧?x1∧x2=?x1∧x2。可以看出C0、C1、C2、C3都可以用普通變量來表示，而不需要時(shí)鐘變量。實(shí)際上時(shí)鐘變量可以分別用x1和x2替換。

在消除時(shí)鐘變量之后，需要考慮對(duì)特殊符號(hào)next和init的處理。首先針對(duì)next符號(hào)，引入輔助變量。對(duì)于每一個(gè)操作next(x)=y引入輔助變量next_x，該操作轉(zhuǎn)化為兩條賦值語句：x=next_x,next_x=y。這兩條語句按順序執(zhí)行，先賦值x，再賦值next_x。需要說明的是，當(dāng)將next_x賦值給x時(shí)，next_x的值是上一個(gè)反應(yīng)計(jì)算的值。對(duì)x賦值之后，才能在當(dāng)前反應(yīng)計(jì)算next_x的值，也就是下一個(gè)反應(yīng)x的值。

對(duì)于特殊符號(hào)init，它表示對(duì)一組變量設(shè)置初始值。針對(duì)每一個(gè)操作init(x)=y，轉(zhuǎn)化為init:next_x=y。關(guān)鍵字init表示該語句為初始化語句。所有的初始化語句都是next變量的初始化，這是由SIGNAL程序的語義決定的，所有初始操作都是由SIGNAL的延時(shí)操作產(chǎn)生的。由于next(x)的轉(zhuǎn)化規(guī)則，這里初始化next_x而不是x。變量next_x實(shí)際上為狀態(tài)變量或稱為存儲(chǔ)變量，它們決定了一個(gè)S-CGA的狀態(tài)，其他的變量是無狀態(tài)變量。圖10給出了從運(yùn)行實(shí)例的S-CGA轉(zhuǎn)化得到的GA。需要注意的是圖8中（5）、（6）、（8）、（9）、（13）、（14）在GA中消失，因?yàn)镚A在轉(zhuǎn)化為程序之后，可以保證這幾條語句的成立。

Fig.10　GAof running example圖10　運(yùn)行實(shí)例的GA

3.3　GA到GACL轉(zhuǎn)化

在消除了時(shí)鐘變量、next和init符號(hào)之后，可以得到GA。GA中的每一個(gè)衛(wèi)式操作，都可以用程序設(shè)計(jì)語言的變量和操作表達(dá)。衛(wèi)式操作之間存在某些依賴關(guān)系，這些依賴關(guān)系決定了GA中衛(wèi)式操作的執(zhí)行順序。本文使用數(shù)據(jù)依賴圖（data dependence graph，DDG）描述衛(wèi)士操作的依賴關(guān)系。衛(wèi)式操作之間的依賴關(guān)系可以通過衛(wèi)式操作和變量之間的讀寫依賴來定義。

定義5（衛(wèi)式操作和變量之間的依賴關(guān)系）對(duì)于一個(gè)表達(dá)式e，F(xiàn)V(e)表示出現(xiàn)在e中的自由變量（free variable）的集合。衛(wèi)式操作對(duì)變量的讀寫依賴關(guān)系定義如下：

其中，RdVars為讀依賴；WrVars為寫依賴。

定義6（數(shù)據(jù)依賴圖）GA的數(shù)據(jù)依賴圖定義為，其中V是圖節(jié)點(diǎn)的集合，每一個(gè)節(jié)點(diǎn)對(duì)應(yīng)一個(gè)衛(wèi)式操作；E?V×V是有向邊的集合，表示節(jié)點(diǎn)之間的依賴關(guān)系。對(duì)于兩個(gè)衛(wèi)式操作ga1和ga2，如果它們滿足如下兩個(gè)條件之一：

（1）存在一個(gè)變量x，并且存在x的next變量next_x，滿足x∈WrVars(ga2)并且next_x∈WrVars(ga1)；

（2）存在一個(gè)變量x，并且x沒有對(duì)應(yīng)的next變量，滿足x∈WrVars(ga2)?RdVars(ga1)。那么存在一條依賴邊從ga1到ga2，即ga1依賴ga2，表示為(ga1,ga2)。

衛(wèi)式操作ga1依賴于衛(wèi)式操作ga2，表明ga1的執(zhí)行必須在ga2之后。圖11給出了運(yùn)行實(shí)例數(shù)據(jù)依賴圖的例子（數(shù)據(jù)依賴圖為除去虛線框之后的圖）。這里解釋一下衛(wèi)式操作（a）y2=next_y2與衛(wèi)式操作（b）next_y2=y3之間的關(guān)系。如圖11所示，衛(wèi)式操作（b）必須在衛(wèi)式操作（a）之后執(zhí)行，但是衛(wèi)式操作（a）需要使用變量next_y2。該變量是一個(gè)狀態(tài)變量，它存儲(chǔ)的是之前計(jì)算的當(dāng)前反應(yīng)的y2的值。而衛(wèi)式操作（b）計(jì)算的next_y2的值是下一個(gè)反應(yīng)y2的值。因此這里必須首先對(duì)y2進(jìn)行賦值然后再計(jì)算next_y2的值。另外衛(wèi)式操作x1?x=s1在圖中簡(jiǎn)化為x=s1。因?yàn)樵撔l(wèi)式操作依賴于x1?s1=y1，所依賴的衛(wèi)式操作已經(jīng)可以保證x1一定為真，所以對(duì)依賴圖可以進(jìn)行簡(jiǎn)化。

Fig.11　Thread partition of running example圖11　運(yùn)行實(shí)例的線程劃分

在得到GA的數(shù)據(jù)依賴圖后，根據(jù)數(shù)據(jù)依賴圖，需要對(duì)其進(jìn)行劃分得到多個(gè)線程。為了提高劃分后線程的執(zhí)行效率，本文給出線程劃分的原則如下：對(duì)于每一個(gè)線程內(nèi)的衛(wèi)式操作集合滿足衛(wèi)式操作之間是全序關(guān)系，并且當(dāng)一個(gè)線程開始執(zhí)行，它不能被其他線程阻塞（blocked）。

這里阻塞的含義是當(dāng)線程內(nèi)的一個(gè)衛(wèi)式操作被執(zhí)行，它所有依賴的變量都已經(jīng)被計(jì)算過，從而不需要等待其他變量被計(jì)算。

針對(duì)以上原則，本文給出GA數(shù)據(jù)依賴圖的劃分算法如下：

步驟1初始時(shí)，將每一個(gè)衛(wèi)式操作看作一個(gè)簇（cluster），即每一個(gè)簇包含唯一一個(gè)衛(wèi)式操作。

步驟2對(duì)于兩個(gè)簇c1、c2，如果滿足c1是c2的唯一父節(jié)點(diǎn)，則將這兩個(gè)簇合成一個(gè)簇。重復(fù)步驟2直到?jīng)]有可以合并的簇為止。

GA劃分中的每一個(gè)簇就是一個(gè)線程。初始時(shí)，每一個(gè)簇都只包含一個(gè)衛(wèi)式操作，很明顯滿足線程劃分原則。步驟2合成的新簇仍然符合線程劃分原則。需要注意的是init操作是不在簇劃分范圍之內(nèi)的。初始化操作只在系統(tǒng)啟動(dòng)的時(shí)候執(zhí)行，之后的反應(yīng)計(jì)算初始化操作都不參與。對(duì)GA進(jìn)行劃分后得到的結(jié)構(gòu)稱為帶劃分的衛(wèi)式操作（GACL）。圖11為運(yùn)行實(shí)例的線程劃分實(shí)例。圖中給出了衛(wèi)式操作的數(shù)據(jù)依賴，虛線框內(nèi)是劃分的一個(gè)線程。只有一個(gè)衛(wèi)式操作的線程無虛線框。

4　帶劃分衛(wèi)式操作到Java代碼生成

從GACL到多線程Java代碼的自動(dòng)生成包括兩方面：（1）對(duì)GACL靜態(tài)結(jié)構(gòu)的自動(dòng)生成，即衛(wèi)式操作和衛(wèi)式操作的劃分等；（2）靜態(tài)結(jié)構(gòu)在執(zhí)行過程中的動(dòng)態(tài)調(diào)用。圖12給出了生成Java代碼的結(jié)構(gòu)。

Fig.12　Structure of code generation圖12　代碼生成結(jié)構(gòu)

圖12中Java代碼靜態(tài)部分負(fù)責(zé)表示GACL中的衛(wèi)式操作、簇和劃分的概念。Java代碼動(dòng)態(tài)部分負(fù)責(zé)對(duì)以上劃分進(jìn)行計(jì)算的調(diào)度。兩部分通過Cluster和Task進(jìn)行關(guān)聯(lián)，一個(gè)計(jì)算任務(wù)關(guān)聯(lián)到一個(gè)劃分的計(jì)算。下面對(duì)這兩部分進(jìn)行詳細(xì)介紹。

4.1　Java代碼靜態(tài)結(jié)構(gòu)

Java代碼的靜態(tài)結(jié)構(gòu)類圖如圖13所示，它包含了3個(gè)主要的接口：IGuardedAction、ICluster、IPartition。這3個(gè)接口分別對(duì)應(yīng)衛(wèi)式操作、簇和劃分。類GuardedAction0……GuardedActionN是接口IGuarded-Action的N個(gè)實(shí)現(xiàn)。針對(duì)每一個(gè)衛(wèi)式操作實(shí)現(xiàn)相應(yīng)的類。Cluster實(shí)現(xiàn)了一個(gè)簇的表示。Partition實(shí)現(xiàn)了一個(gè)劃分的表示。一個(gè)劃分包含了多個(gè)簇，一個(gè)簇包含了多個(gè)衛(wèi)式操作。本文只對(duì)接口IGuardedAction和其實(shí)現(xiàn)類GuardedAction進(jìn)行詳細(xì)介紹。

接口IGuardedAction的代碼如下：

該接口包含3個(gè)方法：guard、action和isReady。這3個(gè)方法分別對(duì)應(yīng)衛(wèi)式操作的衛(wèi)式條件、操作和依賴關(guān)系。IsReady表示該衛(wèi)式操作是否可以被執(zhí)行，即該衛(wèi)式操作所有讀變量是否已經(jīng)被計(jì)算，讀變量已經(jīng)有值。

Fig.13　Class diagram of static code圖13　靜態(tài)代碼類圖

針對(duì)本文運(yùn)行實(shí)例中的衛(wèi)式操作x1?s1=y1，它對(duì)應(yīng)的衛(wèi)式操作類如下：

其中衛(wèi)式條件為x1，操作guard()返回該變量的值。操作為s1=y1。賦值c_s1表示該變量被計(jì)算有值。最后的isReady函數(shù)表示如果x1和y1都被計(jì)算過，那么該衛(wèi)式操作就可以被計(jì)算。

4.2　Java代碼動(dòng)態(tài)結(jié)構(gòu)

圖14給出了動(dòng)態(tài)部分代碼的類圖。包含了兩個(gè)接口：ITask和IThreadPool。ITask對(duì)應(yīng)一個(gè)任務(wù)，它將分配給一個(gè)線程去執(zhí)行。IThreadPool對(duì)應(yīng)一個(gè)線程池的概念，它負(fù)責(zé)線程的創(chuàng)建和任務(wù)的分配。類WorkerThread對(duì)一個(gè)線程進(jìn)行了實(shí)現(xiàn)。這里對(duì)類Task、ThreadPool和WorkerThread進(jìn)行詳細(xì)介紹。

類Task的代碼如下：

在類Task中包含了一個(gè)變量cluster，該變量表示該Task對(duì)應(yīng)該cluster。方法isReady測(cè)試該task是否可以被執(zhí)行，一個(gè)task是否可以被執(zhí)行就是該task對(duì)應(yīng)的cluster是否可以被執(zhí)行。方法invoke就是嘗試啟動(dòng)一個(gè)task。方法invokeChildren嘗試啟動(dòng)一個(gè)task所有的直接后繼任務(wù)。方法computation是執(zhí)行該task對(duì)應(yīng)的cluster中的所有衛(wèi)式操作，在執(zhí)行完操作后，需要測(cè)試它的后繼是否可以被計(jì)算，因此代碼中嘗試啟動(dòng)它的所有后繼。

Fig.14　Class diagram of dynamic code圖14　動(dòng)態(tài)代碼類圖

類ThreadPool的代碼如下：

ThreadPool是所有cluster執(zhí)行調(diào)度的核心類，它包含一個(gè)隊(duì)列queue存儲(chǔ)所有的可以被執(zhí)行的任務(wù)。線程池中所有的線程存儲(chǔ)在變量thread中。方法execute將一個(gè)task放入到隊(duì)列的尾部。方法terminate-Task通知該任務(wù)已經(jīng)被執(zhí)行完畢，該方法在執(zhí)行線程中被調(diào)用（見類WorkerThread）。私有類Worker-Thread實(shí)現(xiàn)了一個(gè)線程，其中run方法總是在等待隊(duì)列中需要被執(zhí)行的任務(wù)。如果獲得一個(gè)任務(wù)，線程執(zhí)行該任務(wù)，否則等待線程池給其分配任務(wù)。整個(gè)調(diào)度類的具體執(zhí)行過程參見圖15。圖15表明在執(zhí)行過程中一個(gè)可以被執(zhí)行的task首先放入隊(duì)列的尾部，一組線程即worker，在隊(duì)列頭部等待給其分配任務(wù)。一個(gè)線程執(zhí)行完任務(wù)，繼續(xù)等待隊(duì)列給其分配任務(wù)。

Fig.15　Schedule policies of thread pool圖15　線程池的調(diào)度策略

下面討論第3、第4章中代碼生成技術(shù)在其他同步語言中重用的方法。本文的SIGNAL代碼生成的主要過程如下：SIGNAL模型→S-CGA→GA→GACL→多線程Java代碼。對(duì)于其他的同步語言，通過將該同步語言模型轉(zhuǎn)化到S-CGA，可以重用S-CGA到多線程Java代碼的生成過程，但是同步模型到S-CGA需要給出新的規(guī)則。

如果想生成C代碼或者其他語言代碼，只需要給出GACL到某種語言的代碼生成過程即可，而轉(zhuǎn)化過程SIGNAL模型→S-CGA→GA→GACL可以重用，不需要改變。但是具體的代碼生成需要考慮具體編程語言的特性和平臺(tái)特性：

（1）語言差異帶來的實(shí)現(xiàn)差異，例如多線程的實(shí)現(xiàn)方法、Java、C++、C、Python都不相同。面向?qū)ο笳Z言的特性和C語言等命令式語言特性的不同所帶來的實(shí)現(xiàn)方式也不相同。有的安全攸關(guān)軟件開發(fā)需要使用C語言安全子集。

（2）實(shí)現(xiàn)平臺(tái)，例如操作系統(tǒng)、Unix系統(tǒng)和Windows系統(tǒng)對(duì)硬件和系統(tǒng)任務(wù)管理的不同會(huì)導(dǎo)致具體的實(shí)現(xiàn)代碼不同。對(duì)于嵌入式實(shí)時(shí)系統(tǒng)，可能采用VxWorks，具體的實(shí)現(xiàn)又有不同。

因此代碼生成需要考慮具體的編程語言、運(yùn)行環(huán)境和平臺(tái)。本文目前尚沒有完全考慮所有的這些因素，代碼生成主要針對(duì)跨平臺(tái)語言Java。針對(duì)特定硬件平臺(tái)、特定操作系統(tǒng)和特定編程語言的代碼生成將作為未來工作。另外需要說明的是，SIGNAL模型代碼生成是完整的代碼生成，即生成的代碼可以運(yùn)行。這和已有UML（unified modeling language）模型只生成代碼框架的工作有所區(qū)別。

5　實(shí)例分析

本文通過對(duì)空客（Airbus）A340飛機(jī)的飛行警報(bào)系統(tǒng)的一個(gè)簡(jiǎn)化版本進(jìn)行實(shí)例分析來驗(yàn)證代碼生成的有效性。該警報(bào)系統(tǒng)任務(wù)是：當(dāng)系統(tǒng)中出現(xiàn)異常，它決定在什么時(shí)候和以什么方式輸出一個(gè)警告信號(hào)。該系統(tǒng)存在兩個(gè)并發(fā)的循環(huán)模塊：（1）警報(bào)管理模塊，該模塊負(fù)責(zé)對(duì)一個(gè)警報(bào)的確認(rèn)，并根據(jù)該警報(bào)是真實(shí)出現(xiàn)或缺失決定是否移除該警報(bào)。（2）警報(bào)通知模塊，該模塊負(fù)責(zé)輸出確認(rèn)后的警報(bào)信號(hào)。圖16給出了飛行警告系統(tǒng)的SIGNAL模型。其中Alarm_Manager為警報(bào)管理子系統(tǒng)，Alarm_Notifier為警報(bào)通知子系統(tǒng)。FW_System通過將兩個(gè)模塊進(jìn)行組合后得到飛行警報(bào)系統(tǒng)，通過變量tmp完成兩個(gè)模塊的交互。

Fig.16　Airplane alarm system圖16　飛行警報(bào)系統(tǒng)

在警告管理模塊中，信號(hào)cnt是一個(gè)邏輯時(shí)刻的計(jì)數(shù)器，該計(jì)數(shù)器逐步遞減，當(dāng)cnt的上一個(gè)值，即信號(hào)zcnt的值為0時(shí)，將cnt重置為參數(shù)k-1。信號(hào)start_confirm表示對(duì)一個(gè)警報(bào)進(jìn)行確認(rèn)的開始邏輯時(shí)刻。信號(hào)start_confirm出現(xiàn)當(dāng)且僅當(dāng)計(jì)數(shù)器等于延時(shí)參數(shù)delay。輸入的警報(bào)信號(hào)alarm_in與信號(hào)start_confirm的時(shí)鐘相同，也就是說，兩者出現(xiàn)的邏輯時(shí)刻相同。

在警報(bào)通知模塊中，信號(hào)cnt和zcnt與警報(bào)管理表達(dá)的含義相同。信號(hào)start_notif表示警報(bào)通知開始的邏輯時(shí)刻。當(dāng)輸入alarm為true，說明是一個(gè)真實(shí)警報(bào)信號(hào)，將其作為信號(hào)s輸出，否則不輸出警報(bào)信號(hào)。

模塊FW_System對(duì)上兩個(gè)模塊進(jìn)行組合，其中局部變量tmp作為臨時(shí)信號(hào)在兩個(gè)模塊之間傳輸數(shù)據(jù)。

Fig.17　Execution results of generated code圖17　生成代碼運(yùn)行結(jié)果

本文原型系統(tǒng)所采用的工具是OCaml[17]，一種函數(shù)式語言。該語言的特性是提供方便的語法分析（ocamlyacc）和詞法分析（ocamllex）。通過對(duì)參數(shù)k1、k2、d1、d2的設(shè)定，原型工具將以上SIGNAL模型轉(zhuǎn)化為Java代碼。對(duì)應(yīng)的Java代碼包含4個(gè)包（packages）：包ddg是所有的靜態(tài)結(jié)構(gòu)類圖的集合，包括衛(wèi)式操作、簇、劃分等；包task包含了Task接口和類的實(shí)現(xiàn)；包threadpool包含所有線程調(diào)度的類。生成的代碼可以直接在Eclipse中運(yùn)行。在Eclipse中運(yùn)行生成代碼結(jié)果如圖17所示。下面對(duì)運(yùn)行結(jié)果進(jìn)行說明。圖17中每一行數(shù)據(jù)為一次反應(yīng)計(jì)算每一個(gè)信號(hào)的值，展示10次反應(yīng)各個(gè)信號(hào)的值。每一列為對(duì)應(yīng)信號(hào)在10次反應(yīng)的值。信號(hào)標(biāo)記為（M）表示警報(bào)管理模塊的信號(hào)。信號(hào)標(biāo)記為（N）表示警報(bào)通知模塊的信號(hào)。AB表示信號(hào)在該反應(yīng)缺失。TR表示該信號(hào)值為true，F(xiàn)A表示該信號(hào)值為false。圖17（a）是參數(shù)設(shè)置為k1=k2=3，d1=d2=1的運(yùn)行結(jié)果，信號(hào)cnt從2開始計(jì)數(shù)，逐步遞減到0，之后重新設(shè)置為reset的值。信號(hào)reset只有在cnt為0時(shí)才出現(xiàn)。當(dāng)zcnt=delay（即cnt+1=delay）時(shí)，信號(hào)alarm_in有輸入值，并且start_confirm為true，即開始確認(rèn)。只有alarm_out，即警報(bào)通知模塊的alarm信號(hào)為真時(shí)，輸出信號(hào)s才有值，其他時(shí)刻缺失。修改參數(shù)k1=k2=5，d1=d2=3，重新運(yùn)行生成的Java代碼如圖17（b）所示，計(jì)數(shù)信號(hào)cnt從4遞減到0，當(dāng)cnt+1=delay時(shí)，即cnt為2時(shí)，開始確認(rèn)并輸入信號(hào)alarm_in。同時(shí)如果alarm信號(hào)為真，即警報(bào)為真，發(fā)布該警報(bào)通知。通過對(duì)生成代碼的運(yùn)行，可以看出Java代碼的運(yùn)行結(jié)果符合SIGNAL模型的運(yùn)行語義。

6　相關(guān)工作與結(jié)束語

模型的代碼自動(dòng)生成是減少人工編碼錯(cuò)誤的一種重要手段。已有的模型代碼生成包括半形式化模型代碼生成和形式化模型代碼生成。文獻(xiàn)[21]給出了半形式化UML模型中狀態(tài)圖和活動(dòng)圖的代碼自動(dòng)生成技術(shù)。通過建立這兩種圖之間的對(duì)應(yīng)關(guān)系，對(duì)結(jié)合后的模型進(jìn)行代碼生成，相比于其他的UML模型[22]代碼生成，該方法可以給出更完整的代碼。但是因?yàn)閁ML模型為半形式化模型，所以難以對(duì)代碼生成的正確性進(jìn)行驗(yàn)證。且對(duì)于有二義性的模型，無法生成精確的代碼。形式化模型的代碼生成是目前的一個(gè)研究熱點(diǎn)。文獻(xiàn)[23]給出了Event-B模型到Java代碼生成工具EventB2Java的介紹。Event-B是一種基于事件的軟件行為形式化建模。相比于本文工作，Event-B是一種異步模型，而SIGNAL是一種同步模型。安全協(xié)議模型是代碼生成又一個(gè)應(yīng)用領(lǐng)域。安全協(xié)議的實(shí)現(xiàn)必須保證無錯(cuò)誤，并且能夠驗(yàn)證。文獻(xiàn)[24]給出了一種安全協(xié)議的Java代碼生成技術(shù)。該技術(shù)能夠保證安全協(xié)議實(shí)現(xiàn)代碼的正確性。和本文相比，其應(yīng)用的領(lǐng)域不相同，本文更關(guān)注嵌入式軟件領(lǐng)域。

本文面向反應(yīng)式系統(tǒng)建模語言SIGNAL，給出了SIGNAL模型多線程Java代碼的生成過程。該轉(zhuǎn)化過程基于中間結(jié)構(gòu)S-CGA、GA和GACL將其分為4個(gè)步驟：（1）SIGNAL模型到S-CGA轉(zhuǎn)化；（2）S-CGA到GA的轉(zhuǎn)化；（3）GA到GACL的轉(zhuǎn)化；（4）GACL到多線程Java代碼的轉(zhuǎn)化。本文給出每一步的轉(zhuǎn)化規(guī)則和方法。SIGNAL模型多線程代碼自動(dòng)生成技術(shù)基于本文提出的可重用中間結(jié)構(gòu)S-CGA。其他同步語言可以通過轉(zhuǎn)化到該結(jié)構(gòu)，重用S-CGA到Java代碼的生成過程。另外本文的多線程代碼生成思路可以為SIGNAL語言在分布式和多核體系結(jié)構(gòu)下的應(yīng)用提供理論基礎(chǔ)和技術(shù)支撐。

本文的未來研究工作將是對(duì)所提出的轉(zhuǎn)化方法的正確性進(jìn)行驗(yàn)證。采用基于Event-B[25]的精化框架來證明，使用Event-B對(duì)轉(zhuǎn)化的每一種結(jié)構(gòu)進(jìn)行建模，轉(zhuǎn)化過程對(duì)應(yīng)精化過程，通過證明精化過程屬性的保持來證明轉(zhuǎn)化過程屬性的保持。

[1]Rushby J.Critical system properties:survey and taxonomy[J].Reliability Engineering&System Safety,1994,43(2):189-219.

[2]Gamatié A.Designing embedded systems with the SIGNAL[M].New York:Springer,2010:43-73.

[3]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.

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

[5]Abdulla PA,Deneaux J,St?lmarck G,et al.Designing safe,reliable systems using SCADE[C]//LNCS 4313:Proceedings of the 1st International Symposium on Leveraging Applications of Formal Methods,Paphos,Oct 30-Nov 2,2004.Berlin,Heidelberg:Springer,2004:115-129.

[6]Boussinot F,de Simone R.The ESTEREL language[J].Proceedings of the IEEE,1991,79(9):1293-1304.

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

[8]Maraninchi F.The ARGOS language:graphical representation of automata and description of reactive systems[C]//Proceedings of the 1991 IEEE Workshop on Visual Languages,Kobe,Oct 8-11,1991.Piscataway:IEEE,1991:101-107.

[9]André C.Computing SyncCharts reactions[J].Electronic Notes in Theoretical Computer Science,2004,88:3-19.

[10]Gonthier G.Sémantique et modèles d'exécution des langages réactifs synchrones:application à ESTEREL[D].Paris:Université d'Orsay,1988.

[11]Potop-Butucaru D,de Simone R.Optimizations for faster execution of ESTEREL programs[C]//Proceedings of the 1st ACM and IEEE International Conference on Formal Methods and Models for Co-Design,Mont Saint-Michel,Jun 24-26,2003.Washington:IEEE Computer Society,2003:227-236.

[12]Harel D,Naamad A.The STATEMATE semantics of statecharts[J].ACM Transactions on Software Engineering and Methodology,1996,5(4):293-333.

[13]Caspi P,Pouzet M.Synchronous Kahn networks[C]//Pro-ceedings of the 1st ACM SIGPLAN International Conference on Functional Programming,Philadelphia,May 24-26,1996.New York:ACM,1996:226-238.

[14]Le Guernic P,Talpin J P,Le Lann J C.Polychrony for system design[J].Journal for Circuits,Systems and Computers,2003,12(3):261-304.

[15]Dennis J B.First version of a data flow procedure language[C]//LNCS 19:Proceedings of the 1974 Symposium Programming,Paris,Apr 9-11,1974.Berlin,Heidelberg:Springer,1974:362-376.

[16]DO-178B/ED-12B RTCA:software considerations in airbone systems and equipment certification[S].Radio Technical Commission for Aeronautics,European Organization for CivilAviation Electronics,1992.

[17]Chailloux E,Manoury P,Pagano B.Developing applications with objective Caml[M].Paris:O'Reilly&Associates,2007.

[18]Yang Zhibin,Bodeveix J P,Fliali M,et al.Towards a verified compiler prototype for the synchronous language SIGNAL[J].Frontiers of Computer Science,2016,10(1):37-53.

[19]Yang Zhibin,Bodeveix J P,Filali M.Multi-core code generation from polychronous programs with time-predictable properties[C]//Proceedings of the 1st International Workshop on Architecture Centric Virtual Integration,Valencia,Sep 29,2014:1-10.

[20]Amagbegnon T,Besnard L,Le Guernic P.Arborescent canonical form of boolean expressions[R].Campus Universitaire de Beaulieu:Institut National de Recherche en Informatique et enAutomatique,1994.

[21]Viswanathan S E,Samuel P.Automatic code generation using unified modeling language activity and sequence models[J].IET Software,2016,10(6):164-172.

[22]Usman M,Nadeem A.Automatic generation of Java code from UML diagrams using UJECTOR[J].International Journal of Software Engineering and Its Applications,2009,3(2):21-37.

[23]Cata?o N,Rivera V.EventB2Java:a code generator for Event-B[C]//LNCS 9690:Proceedings of the8th International Symposium on NASA Formal Methods,Minneapolis,Jun 7-9,2016.Berlin,Heidelberg:Springer,2016:166-171.

[24]Modesti P.Efficient Java code generation of security protocols specified in AnB/AnBx[C]//LNCS 8743:Proceedings of the 10th International Workshop on Security and Trust Management,Wroclaw,Sep 10-11,2014.Berlin,Heidelberg:Springer,2014:204-208.

[25]Abrial J R.Modeling in Event-B system and software engineering[M].New York:Cambridge University Press,2010.