导读 Linux 基金会宣布成立 TLA+ 基金会 (TLAF),以促进 TLA+ 编程语言及其 TLA+ 从业者社区的采用和发展。TLA+ 基金会的创始成员包括 AWS、甲骨文和微软。

TLA+ (Temporal Logic of Actions) 是一种用于对程序和系统 (尤其是并发和分布式程序和系统) 进行建模的高级语言。Linux 基金会表示,TLA+ 语言已被成功用于验证复杂的软件系统、减少错误并提高可靠性;其有助于在开发过程的早期发现设计缺陷,节省时间和资源。“TLA+ Foundation 的成立旨在推动采用经过验证的形式化方法来构建稳健的软件。”

该语言在几十年前由现任 Microsoft Research 杰出科学家 Leslie Lamport 发明,基于 “精确描述事物的最佳方式是使用简单的数学” 的理念。时至今日,其管辖权逐渐从微软转移到 Linux 基金会,并获得了自己独立的基金会来推广发展。

根据介绍,TLA+ 基金会是一个独立的非营利组织,致力于促进 TLA+ 规范语言在工业界、学术界和教育界的采用,其总体目标是推进软件工程中的数学思维。TLAF 资助与 TLA+ 相关的开发,以扩大其用途并促进繁荣的 TLA+ 社区,鼓励该社区成员之间的合作。

TLA+ 基金会将促进采用、提供教育和培训资源、资助研究、开发工具并建立 TLA+ 从业者社区。TLA+ 基金会作为语言委员会的角色将确保 TLA+ 语言的不断完善和演进。TLA+ 基金会将就语言增强做出决策,解决用户反馈和需求,保持高安全性和可靠性标准,并引导语言的发展以更好地服务于其用户群。

基金会的行为准则包括:开源,全心全意地拥抱开源精神;赋予社区权力,最大限度地为 TLA+ 用户带来利益;透明性,所有正式的决策都将公开;以及秉承开放、友好、多元的精神。

Linux 基金会执行董事 Jim Zemlin 称:“TLA+ 基金会的成立表明了我们致力于推进 TLA+ 语言的使用和开发,以造福整个软件行业。随着世界对分布式系统的依赖程度不断提高,对于开发人员来说,拥有 TLA+ 的功能来正式建模和验证系统的行为是否符合预期非常重要。”

原文来自:

本文地址://lrxjmw.cn/linux-logic-temporal.html编辑:向云艳,审核员:清蒸github

Linux大全:

Linux系统大全:

红帽认证RHCE考试心得: