当前位置：首页 > news >正文

如何掌握 Lustre/Scade 同步数据流语言

news 来源：原创 2025/5/3 7:56:37

从 KPN 的萌芽开始，到 Lustre/Scade 的发展，再到 Velus/Zelus/Swan 在形式化编译、连续时间建模、MBD 平权等各方面的边界拓展，同步数据流语言已经历许多。现在，我们讨论如何掌握 Lustre/Scade 这类法式技术，从语言基础，到当前发展。

对掌握 Lustre/Scade 的方法讨论，将从三方面展开：

Lustre/Scade 语言基础和相关技术。
Lustre/Scade 技术的发展演变过程。
Lustre/Scade 当前的拓展方向。

从以上三方面将分别掌握 Lustre/Scade 的基础、历史演变、未来发展。

Lustre/Scade 语言基础和相关技术

对Lustre/Scade的语言基础和相关技术，可从巴黎高师2024Q4至2025Q1开设的《同步反应式系统》课程进行掌握。课程网站可访问wikimpri.dptinfo.ens-cachan.fr。

在该课程中，将介绍Lustre/Scade等同步语言的数学原理、其语义和逻辑基础、编译成软件的相关技术、通过模型检测进行形式化验证的方法。该课程的大纲由如下部分构成：

第一节至第三节中，将讨论Lustre v4/Lustre v6/Heptagon/Scade 6等语言特性中的数据流部分与控制流部分，将涉及到时序算子与形式化方法之间的关联，以及采样操作中的时钟概念对支持控制流特性的关键作用；以及相关的SMT模型检测技术及Kind 2工具。
在第四节中，将讨论在 Velus 编译器中使用证明辅助工具进行语义形式化和编译算法的端到端正确性证明。
在第五节至第八节中，聚焦于从 Lustre 出发的同步语言，并从类型化函数式语言的视角进行探讨：将研究高阶、控制结构（例如模块化重置、分层自动机）等特性对语义的影响，包括其静态语义和动态语义。将讨论例如某些属性（如确定性）可以通过专门的类型系统以模块化方式描述和验证。
在第九节中，将讨论混合模型编写，将同步语言（离散时间）的构造与常微分方程（ODE）结合，用以描述软件与其物理环境之间的交互。将讨论这一设计在静态和动态语义、编译以及运行时系统（与 ODE 求解器对接）方面所带来的问题。

Lustre/Scade 技术的演变发展过程

对 Lustre/Scade 的技术演变，通过 A Brief History of Synchronous Programming (Marc Pouzet, SYNCHRON 22) csdn.net 以及 The Synchronous Languages 12 Years Later (Albert Benveniste, 2022) csdn.net 可得到了解。

对更加具体的信息，有若干途径进行了解：

浏览 SYNCRHON 会议历年的主题变化。csdn.net
浏览 ERTS 会议每双年的主题变化。csdn.net
Lustre/Scade 技术全明星的工作，比如 Albert Benveniste, Baptiste Pauget, Basile Pensin, Bruno Pagano, Cedric Pasteur, Erwan Jahier, Jean Louis Colaco, Leonard Gerard, Lelio Brun, Marc Pouzet, Nicolas Halbwachs, Pascal Raymond, Paul Jeanmaire, Paul Caspi, Timothy Bouke 等人。

Lustre/Scade 当前的拓展方向

在巴黎高师2024Q4至2025Q1开设的《同步反应式系统》课程中，提到了 Lustre/Scade 的若干发展方向。

在第四节中，讨论的使用证明辅助工具进行语义形式化和编译算法的端到端正确性证明。
在第九节中讨论的向连续时间建模的拓展。该方向在2015年Scade hybrid中已有试验性实践，但10年后的2025年，未出现在Scade Suite系列中。然而，值得注意的是，在下一代Scade技术(Scade One)中，已为该拓展做好了铺垫csdn.net。

除语言特性的改变外，在商业策略和具体实现技术方面，Scade技术也作出了相比过去30年(95-25)显著不同的选择：