1991年,《IEEE论文集》专门对同步语言[1]、[2]进行了专门的讨论。其中包括描述三种法国同步语言Esterel[3]、Lustre[4]和Signal[5]的论文,这也是本文的主题。当时,这三种语言已经有了很好的定义,并在工业上得到了一些应用,但仍处于开发阶段。在此期间,这些语言得到了改进,获得了更大的用户社区,并成功地实现了商业化。现在,同步语言已经成为建模、指定、验证和实现实时嵌入式应用程序的首选技术。同步模式已经成为一种基于数学工具的工程师友好的设计方法。
本文讨论了自1991年以来同步语言的改进、困难和成功。它首先讨论了同步原理,以及在将瞬时通信的同步概念与确定性并发性结合起来时,维护功能性的、确定性的系统行为所面临的挑战。第二部分描述了这些语言在工业上的成功应用,以及它们是如何被商业化的。第三节讨论了为编译这些语言而开发的新技术,这些语言比我们最初认为的要困难得多。第四节介绍了过去12年所吸取的一些主要教训。第五部分讨论了一些未来的挑战,包括同步的局限性。最后,第六部分对同步语言的发展前景进行了展望。
同步语言Signal、Esterel和Lustre是建立在一个共同的数学框架上,该框架结合了同步性(时间与一个或多个时钟同步前进)具有确定性并发性。本节探讨选择这种方法的理由及其后果。
A.同步基础
安全关键型嵌入式系统的设计者的主要目标是使他或她自己、客户和认证机构相信设计和实现是正确的。与此同时,他或她必须控制开发和维护成本,并满足系统设计的非功能约束,如成本、功率、重量或系统架构本身(例如,由智能传感器和执行器组成的物理分布式系统,由中央计算机监控)。满足这些目标需要设计方法和工具与现有的设计流无缝集成,并建立在坚实的数学基础上。
使用坚实的数学基础的主要优点是能够对系统的运行进行形式化的推理。这有助于认证,因为它减少了不确定性,并使其有可能构建有关系统运行的证明。这还改进了实现过程,因为它支持自动构造不同实现所需的程序操作,例如,对于满足非功能约束非常有用。
在20世纪80年代,这些观察导致了对同步语言的以下决定。
- 1)并发性——这些语言必须支持函数式并发性,并且它们必须依赖于以用户友好的方式表达并发性的表示法。因此,根据目标应用领域的不同,这些语言应该提供一种符号块图(也称为数据流图),或者层次自动机,或者目标工程社区熟悉的某种命令式语法。后来,在90年代早期,出现了混合这些不同风格的表示法的需要。这显然要求它们具有相同的数学语义。
- 2)简单性——语言必须具有尽可能简单的形式模型,以使形式推理易于处理。特别是,两个进程的并行组合的语义必须是最干净的。
- 3)同步——语言必须支持图1中简单且常用的实现模型,图1中所有提到的操作都假定占用有限的内存和时间。
Fig.1:两个常见的同步执行方案:事件驱动(左)和示例驱动(右)
B.同步和并发
同步把时间分成离散的瞬间。这种模型在数学和工程中很普遍。它出现在自动机中,出现在控制工程师熟悉的离散时间动态系统中,出现在硬件设计师熟悉的同步数字逻辑中。因此,根据连续的原子反应来决定同步程序的进展是很自然的。为了方便起见,我们使用“伪数学”表述,其中R表示所有可能反应的集合,上标
表示无限次迭代。
在控制工程方框图中,整个系统的第个反应是每个本构块的第
个反应的组合。对于块
:
因此,整个反应仅仅是每个块的反应(1)和块之间的连接(2)的连接。
在硬件中连接两个有限状态机(FSMs)也是类似的。图2(a)显示了有限状态系统通常是如何在同步数字逻辑中实现的:一个无环(因此是功能)逻辑块计算输出和下一个状态作为输入和当前状态的函数。图2(b)显示了同时运行两个这样的FSMs并让它们通信的最自然的方式,即,通过将一个有限状态机的一些输出连接到另一个有限状态机的输入,反之亦然。
因此,选择同步语言中并行组合的自然定义为:,其中
为连接词。请注意,并行组合的这个定义也适用于自动机的同步产品的几个变体。因此,同步模型可以总结为以下两个伪方程:
Fig.2:(a)在硬件上实施的有限状态机的一般结构。(b)连接两个FSMs。虚线显示了一条包含瞬时反馈的路径,该反馈来自于连接这两个功能FSMs。
然而,天下没有免费的午餐。平行组合的定义(4)要求各组分的反应形成连接。众所周知,这样的连接通常不是一个函数,而是一种关系,或者同样是一种约束。
自动机的产品是一个熟悉的例子:两个自动机在执行共享转换时必须同步;这是一个约束条件。同样,众所周知,在一个方框图中,允许块之间的任意连接可以产生隐式动力系统,在这个系统中,一个反应将“输入、状态和输出”联系起来(我们用引号表示输入和输出之间的区别变得很细微)。这种隐式模型(在控制系统中也称为描述符或行为模型)实际上对于从基本原理建模系统非常方便,因为在基本原理中自然会遇到平衡方程。同样的情况也发生在硬件上:将两个系统组合成图2(b)中的系统并不总是生成图2(a)中的系统,因为可以创建一个无延迟的系统(即(循环的)路径,如用虚线绘制的路径。
这个功能系统在同步、并发组合下不被关闭的问题可以通过至少四种不同的方法来解决。
- 1)微步——通过将反应定义为一系列基本的微步,人们可以坚持认为它是可操作的。在这种方法中,基本系统组件被假定为这样一个基本序列微步骤,以及原语组件的并行组合是通过以某种适当的方式交错计算来执行的。这是一种操作性语义,它破坏了美观和简单连接的数学运算。然而,这是在超高速集成电路硬件描述语言(VHDL)[6]和Verilog[7]建模语言中采用的方法,在Harel的Statecharts[8]中,Grafcet[9]的旧形式中,[10]用于在控制系统中编写可编程逻辑控制器。它也符合计算机科学和工程的观点,即程序执行是一个受保护的序列行动。然而,微步语义是混乱的,并倾向于许多相互冲突的解释[11],[12]。
- 2)无周期——通常,控制工程师只是坚持他们的框图不包含零延迟循环。在这种情况下,可以保证系统功能正常。这种方法非常适合图1中的样本驱动方法。Lustre采纳了这一观点。
- 3)唯一不动点—该方法承认每个反应都是不动点方程的解,但坚持系统始终按功能运行,即,即每个反应都是形式
的确定性函数。使用这些语义编译程序变得困难,因为有必要证明程序所隐含的关系总是有唯一的形式解
。尽管有这些困难,
语言还是采用了这种方法。
- 4)关系或约束——这种方法接受反应作为约束,并允许每个反应有0个解(“程序被阻塞,没有反应”),一个形式的解(5),或者多个一致的解被解释为不确定性行为。实现通常需要一个独特的解决方案,但其他情况下可能需要部分设计或高级规范。在这种方法中,所有程序都有一个语义。但是,检查程序是否是表单(5)的确定性函数仍然是生成可执行代码之前的问题。Signal采用了这种方法。
C.同步化的基础是如何在同步语言中实例化的
在下面几节中,我们将进一步详细介绍如何在同步语言Lustre、Esterel和Signal中实例化前面讨论的同步基本原理。
.....................................................................................待续.......................................................................................................................