Linux基金會成立系統建模語言TLA+基金會

Linux基金會宣布成立專門支援和發展TLA+（Temporal Logic of Actions）語言的基金會，主要創始會員為微軟、甲骨文和AWS。TLA+是一種形式化的規範語言，可用於描述和檢驗分散式系統的行為、演算法和協定。

TLA+語言最初是由Leslie Lamport在1990年代發明，其目的是要發展一個工具，協助工程師設計、理解和驗證大型軟體系統，特別是對那些具有高可性要求的系統。該語言的核心概念，是形式化數學公理，透過使用數學表示法描述系統的狀態行為，讓開發人員能夠捕捉系統的重要屬性，並且檢驗其是否滿足特定需求，簡單來說，TLA+語言讓開發人員用簡單的數學來描述系統。

支援時間邏輯（Temporal Logic）是TLA+的重要特性，允許開發人員能夠表示和分析，系統在一段時間內變化的邏輯，利用這項特性，開發人員便能夠更簡單地發現，分散式系統中的競爭條件和死鎖等常見問題。由於部分系統中的基本錯誤，很難從程式碼中發現，而且修正起來成本高昂，因此TLA+語言的價值，便是讓開發者更簡單地消除這些基本但是關鍵的錯誤。

TLA+語言發命者Leslie Lamport，目前是微軟研究院的傑出科學家，在Leslie Lamport發明TLA+語言之後，受微軟的支援和管理，現在微軟決定將該專案貢獻出來，在Linux基金會旗下成立TLA+語言基金會，以促進該語言推廣、研究資助和工具開發等工作。