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.