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

闞雙龍，黃志球，楊志斌

南京航空航天大學 計算機科學與技術學院，南京 210016

1　引言

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

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

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

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

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

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

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

本文組織結構如下：第2章給出了SIGNAL語言的基本語法和語義；第3章給出了SIGNAL模型到帶劃分衛式操作的轉化過程；第4章給出了帶劃分衛式操作到Java代碼的生成過程；第5章給出了空客A340警報系統的實例分析；第6章為本文相關工作和結束語。

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

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

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

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

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

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

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

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

（1）瞬時函數操作

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

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

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

（2）延時操作

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

與瞬時函數相同，延時操作的兩個信號具有相同的時鐘，圖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出現且值為true的時鐘。信號s2的時鐘定義為信號s1的時鐘和[b]的交，即在任意時刻如果s2出現，當且僅當s1和[b]同時出現。圖4給出了條件采樣操作s2:=s1whenb的運行實例。從圖中可以看出，當s2出現的時候s1和b同時出現，并且當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出現，那么s3出現，并且s1比s2有更高的優先級。

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

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

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

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

“高校固定資產管理平臺”的使用，推進了固定資產管理工作的信息化進程，也促進了高校數字校園的建設，實現對固定資產的動態管理，同時也真實反映學校的固定資產及財務狀況。

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

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

3　SIGNAL到帶劃分衛式操作轉化

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

（1）SIGNAL模型到S-CGA的轉化；

（2）S-CGA到GA的轉化；

（3）GA到GACL的轉化；

（4）GACL到多線程Java代碼的轉化。

本章只關注步驟（1）、（2）、（3）。步驟（4）在第4章進行詳細介紹。為了更好地對轉化過程進行說明，本文以圖7的運行實例對整個轉化過程進行說明。圖7中需要說明的是符號“^=”，該符號表示兩個信號的時鐘相同。實際上它們可以使用基本操作表達。例如可以表示為以下3個瞬時函數操作：

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

3.1　SIGNAL到S-CGA轉化

本節給出SIGNAL模型到中間結構S-CGA的轉化過程。首先給出S-CGA的定義，然后針對每一個SIGNAL操作給出對應的S-CGA轉化規則。

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

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

Table 1　Translation rules from SIGNAL to S-CGA表1　SIGNAL到S-CGA轉化規則

圖7的SIGNAL運行實例經過該步的轉化可以得到對應的S-CGA。具體的S-CGA如圖8所示。這里需要解釋的是（13）、（14）行它們分別對應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的轉化

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

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

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

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

（2）針對每一個S-CGA中的衛式操作，用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設置為真，那么4個時鐘等價類可以表示為：C0=true,C1=true∧x1=x1，C2=true∧x2=x2，C3=true∧?x1∧x2=?x1∧x2。可以看出C0、C1、C2、C3都可以用普通變量來表示，而不需要時鐘變量。實際上時鐘變量可以分別用x1和x2替換。

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

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

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

3.3　GA到GACL轉化

在消除了時鐘變量、next和init符號之后，可以得到GA。GA中的每一個衛式操作，都可以用程序設計語言的變量和操作表達。衛式操作之間存在某些依賴關系，這些依賴關系決定了GA中衛式操作的執行順序。本文使用數據依賴圖（data dependence graph，DDG）描述衛士操作的依賴關系。衛式操作之間的依賴關系可以通過衛式操作和變量之間的讀寫依賴來定義。

定義5（衛式操作和變量之間的依賴關系）對于一個表達式e，FV(e)表示出現在e中的自由變量（free variable）的集合。衛式操作對變量的讀寫依賴關系定義如下：

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

定義6（數據依賴圖）GA的數據依賴圖定義為，其中V是圖節點的集合，每一個節點對應一個衛式操作；E?V×V是有向邊的集合，表示節點之間的依賴關系。對于兩個衛式操作ga1和ga2，如果它們滿足如下兩個條件之一：

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

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

衛式操作ga1依賴于衛式操作ga2，表明ga1的執行必須在ga2之后。圖11給出了運行實例數據依賴圖的例子（數據依賴圖為除去虛線框之后的圖）。這里解釋一下衛式操作（a）y2=next_y2與衛式操作（b）next_y2=y3之間的關系。如圖11所示，衛式操作（b）必須在衛式操作（a）之后執行，但是衛式操作（a）需要使用變量next_y2。該變量是一個狀態變量，它存儲的是之前計算的當前反應的y2的值。而衛式操作（b）計算的next_y2的值是下一個反應y2的值。因此這里必須首先對y2進行賦值然后再計算next_y2的值。另外衛式操作x1?x=s1在圖中簡化為x=s1。因為該衛式操作依賴于x1?s1=y1，所依賴的衛式操作已經可以保證x1一定為真，所以對依賴圖可以進行簡化。

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

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

這里阻塞的含義是當線程內的一個衛式操作被執行，它所有依賴的變量都已經被計算過，從而不需要等待其他變量被計算。

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

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

步驟2對于兩個簇c1、c2，如果滿足c1是c2的唯一父節點，則將這兩個簇合成一個簇。重復步驟2直到沒有可以合并的簇為止。

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

4　帶劃分衛式操作到Java代碼生成

從GACL到多線程Java代碼的自動生成包括兩方面：（1）對GACL靜態結構的自動生成，即衛式操作和衛式操作的劃分等；（2）靜態結構在執行過程中的動態調用。圖12給出了生成Java代碼的結構。

Fig.12　Structure of code generation圖12　代碼生成結構

圖12中Java代碼靜態部分負責表示GACL中的衛式操作、簇和劃分的概念。Java代碼動態部分負責對以上劃分進行計算的調度。兩部分通過Cluster和Task進行關聯，一個計算任務關聯到一個劃分的計算。下面對這兩部分進行詳細介紹。

4.1　Java代碼靜態結構

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

接口IGuardedAction的代碼如下：

該接口包含3個方法：guard、action和isReady。這3個方法分別對應衛式操作的衛式條件、操作和依賴關系。IsReady表示該衛式操作是否可以被執行，即該衛式操作所有讀變量是否已經被計算，讀變量已經有值。

Fig.13　Class diagram of static code圖13　靜態代碼類圖

針對本文運行實例中的衛式操作x1?s1=y1，它對應的衛式操作類如下：

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

4.2　Java代碼動態結構

圖14給出了動態部分代碼的類圖。包含了兩個接口：ITask和IThreadPool。ITask對應一個任務，它將分配給一個線程去執行。IThreadPool對應一個線程池的概念，它負責線程的創建和任務的分配。類WorkerThread對一個線程進行了實現。這里對類Task、ThreadPool和WorkerThread進行詳細介紹。

類Task的代碼如下：

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

Fig.14　Class diagram of dynamic code圖14　動態代碼類圖

類ThreadPool的代碼如下：

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

Fig.15　Schedule policies of thread pool圖15　線程池的調度策略

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

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

（1）語言差異帶來的實現差異，例如多線程的實現方法、Java、C++、C、Python都不相同。面向對象語言的特性和C語言等命令式語言特性的不同所帶來的實現方式也不相同。有的安全攸關軟件開發需要使用C語言安全子集。

（2）實現平臺，例如操作系統、Unix系統和Windows系統對硬件和系統任務管理的不同會導致具體的實現代碼不同。對于嵌入式實時系統，可能采用VxWorks，具體的實現又有不同。

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

5　實例分析

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

Fig.16　Airplane alarm system圖16　飛行警報系統

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

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

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

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

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

6　相關工作與結束語

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

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

本文的未來研究工作將是對所提出的轉化方法的正確性進行驗證。采用基于Event-B[25]的精化框架來證明，使用Event-B對轉化的每一種結構進行建模，轉化過程對應精化過程，通過證明精化過程屬性的保持來證明轉化過程屬性的保持。

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