闞雙龍，黃志球，楊志斌

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

1　引言

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

同步語言[3]是針對反應(yīng)式系統(tǒng)提出的一種系統(tǒng)建模語言。該語言將一次反應(yīng)計算的時間抽象為一個邏輯時刻。系統(tǒng)的計算就是一條邏輯時刻的序列。同步語言是一種具有精確語義的形式化語言，目前已經(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)命令式語言的順序、迭代等特性，同時又支持反應(yīng)式系統(tǒng)對每一次反應(yīng)計算的規(guī)約。對ESTEREL的編譯可以生成自動機[10]和控制流圖[11]等。ESTEREL的典型應(yīng)用包括自動化交通、航空航天、國防、鐵路交通等領(lǐng)域的嵌入式設(shè)計。狀態(tài)圖是一種圖形化的設(shè)計語言，它的基本特征包括對嵌入式系統(tǒng)的通信、并發(fā)和層次性進行建模。但是狀態(tài)圖本身是一種半形式化的建模語言，已有工作對其形式語義進行定義[12]。Argos是狀態(tài)圖的一種擴展，它的特點是比狀態(tài)圖支持更嚴(yán)格的同步語義。SyncCharts同步語言同時受到ESTEREL和狀態(tài)圖的影響，因此它具有兩者的特征。

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

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

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

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

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

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

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

Fig.1　Synchronous time model圖1　同步時間模型

同步語言SIGNAL也是基于以上同步時間模型。SIGNAL包含兩個重要的概念：信號和信號的抽象時鐘。

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

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

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

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

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

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

Fig.2　An instance of instantaneous operation圖2　瞬時操作實例

（2）延時操作

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

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

Fig.3　An instance of delay operation圖3　延時操作實例

（3）條件采樣操作

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

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

Fig.4　An instance of undersampling operation圖4　條件采樣運行實例

（4）確定性合并

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

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

Fig.5　An instance of deterministic merging圖5　確定性合并運行實例

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

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

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

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

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

Fig.6　Process framework and an instance圖6　進程框架及其實例

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

本文代碼自動生成技術(shù)給出從SIGNAL模型到多線程Java代碼的轉(zhuǎn)化過程。整個轉(zhuǎn)化過程涉及如下3個中間結(jié)構(gòu)：同步時鐘衛(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)。整個轉(zhuǎn)化過程分為以下幾個步驟：

（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章進行詳細介紹。為了更好地對轉(zhuǎn)化過程進行說明，本文以圖7的運行實例對整個轉(zhuǎn)化過程進行說明。圖7中需要說明的是符號“^=”，該符號表示兩個信號的時鐘相同。實際上它們可以使用基本操作表達。例如可以表示為以下3個瞬時函數(shù)操作：

Fig.7　Arunning example of SIGNAL model圖7　一個SIGNAL運行實例

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

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

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

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

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

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

Fig.8　S-CGAof running example圖8　運行實例的S-CGA

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

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

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

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

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

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

Fig.9　Clock hierarchy of running example圖9　運行實例的時鐘層次

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

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

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

Fig.10　GAof running example圖10　運行實例的GA

3.3　GA到GACL轉(zhuǎn)化

在消除了時鐘變量、next和init符號之后，可以得到GA。GA中的每一個衛(wèi)式操作，都可以用程序設(shè)計語言的變量和操作表達。衛(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)系）對于一個表達式e，F(xiàn)V(e)表示出現(xiàn)在e中的自由變量（free variable）的集合。衛(wèi)式操作對變量的讀寫依賴關(guān)系定義如下：

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

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

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

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

衛(wèi)式操作ga1依賴于衛(wèi)式操作ga2，表明ga1的執(zhí)行必須在ga2之后。圖11給出了運行實例數(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。該變量是一個狀態(tài)變量，它存儲的是之前計算的當(dāng)前反應(yīng)的y2的值。而衛(wèi)式操作（b）計算的next_y2的值是下一個反應(yīng)y2的值。因此這里必須首先對y2進行賦值然后再計算next_y2的值。另外衛(wèi)式操作x1?x=s1在圖中簡化為x=s1。因為該衛(wèi)式操作依賴于x1?s1=y1，所依賴的衛(wèi)式操作已經(jīng)可以保證x1一定為真，所以對依賴圖可以進行簡化。

Fig.11　Thread partition of running example圖11　運行實例的線程劃分

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

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

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

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

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

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

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

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

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

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

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

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

接口IGuardedAction的代碼如下：

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

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

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

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

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

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

類Task的代碼如下：

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

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

類ThreadPool的代碼如下：

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

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

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

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

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

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

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

5　實例分析

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

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

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

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

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

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

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

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

模型的代碼自動生成是減少人工編碼錯誤的一種重要手段。已有的模型代碼生成包括半形式化模型代碼生成和形式化模型代碼生成。文獻[21]給出了半形式化UML模型中狀態(tài)圖和活動圖的代碼自動生成技術(shù)。通過建立這兩種圖之間的對應(yīng)關(guān)系，對結(jié)合后的模型進行代碼生成，相比于其他的UML模型[22]代碼生成，該方法可以給出更完整的代碼。但是因為UML模型為半形式化模型，所以難以對代碼生成的正確性進行驗證。且對于有二義性的模型，無法生成精確的代碼。形式化模型的代碼生成是目前的一個研究熱點。文獻[23]給出了Event-B模型到Java代碼生成工具EventB2Java的介紹。Event-B是一種基于事件的軟件行為形式化建模。相比于本文工作，Event-B是一種異步模型，而SIGNAL是一種同步模型。安全協(xié)議模型是代碼生成又一個應(yīng)用領(lǐng)域。安全協(xié)議的實現(xiàn)必須保證無錯誤，并且能夠驗證。文獻[24]給出了一種安全協(xié)議的Java代碼生成技術(shù)。該技術(shù)能夠保證安全協(xié)議實現(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個步驟：（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模型多線程代碼自動生成技術(shù)基于本文提出的可重用中間結(jié)構(gòu)S-CGA。其他同步語言可以通過轉(zhuǎn)化到該結(jié)構(gòu)，重用S-CGA到Java代碼的生成過程。另外本文的多線程代碼生成思路可以為SIGNAL語言在分布式和多核體系結(jié)構(gòu)下的應(yīng)用提供理論基礎(chǔ)和技術(shù)支撐。

本文的未來研究工作將是對所提出的轉(zhuǎn)化方法的正確性進行驗證。采用基于Event-B[25]的精化框架來證明，使用Event-B對轉(zhuǎn)化的每一種結(jié)構(gòu)進行建模，轉(zhuǎn)化過程對應(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.