從 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)顯著不同的選擇：

• MBD技術平權，將MBD技術從少數高安全領域向更廣泛的安全嵌入式軟件普及。csdn.net
• 可視化編程與文本編程的統一。csdn.net及csdn.net
• 以及在建模技術和對外集成技術方面，下一時代的著力點選擇為.NET和Python(PyScadeOne)。csdn.net