首页 > 系统相关 >Linux 基金会宣布成立 TLA+ 语言基金会

Linux 基金会宣布成立 TLA+ 语言基金会

时间:2023-05-07 22:56:16浏览次数:47  
标签:社区 基金会 语言 TLA Linux 成立

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

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

Linux 基金会宣布成立 TLA+ 语言基金会Linux 基金会宣布成立 TLA+ 语言基金会

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

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

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

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

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

标签:社区,基金会,语言,TLA,Linux,成立
From: https://www.cnblogs.com/x1-c2/p/17380391.html

相关文章

  • Linux 基金会宣布成立 TLA+ 语言基金会
    Linux 基金会宣布成立TLA+基金会(TLAF),以促进TLA+编程语言及其TLA+从业者社区的采用和发展。TLA+基金会的创始成员包括AWS、甲骨文和微软。TLA+(TemporalLogicofActions)是一种用于对程序和系统(尤其是并发和分布式程序和系统)进行建模的高级语言。Linux......
  • linux 内核空间内存分布
    虚拟地址空间划分linux通过宏“PAGE_OFFSET”将4GB的虚拟地址空间(32bit平台)划分成内核地址空间和进程地址空间两部分。“PAGE_OFFSET”的值支持通过Kconfig配置,其默认的值是“0xC0000000”。下面以经典的“PAGE_OFFSET=0xC0000000”来看下linux对虚拟地址空间的详细划分。Linux......
  • 在linux上使用Qt开发动态库项目,怎么只生成一个so文件
     背景:在linux系统上,我们使用Qt开发动态库项目时,会默认生成四个文件:x.so 、x.so.1、x.so.1.0、x.so.1.0.0四个文件,只有一个真实的so库,剩下的三个都是链接文件。我们交付的时候,不可能发一堆文件出去,所以我们需要对Qt项目进行设置,保证输入的只有一个so文件......
  • 如何在Linux中查找一个文件
    《Linux就该这么学》-必读的Linux系统与红帽RHCE认证免费自学书籍免费电子版下载地址:https://www.linuxprobe.com/book导读对于新手而言,在Linux中使用命令行可能会非常不方便。没有图形界面,很难在不同文件夹间浏览,找到需要的文件。本篇教程中,我会展示如何在Linux中查找特......
  • Linux运维实战项⽬进阶
    项⽬描述项⽬需求近年来为适应业务发展的需求,世界500强XX企业准备进⾏⼤规模的电⼦商务建设,同时,希望能通过Linux平台,利⽤开源技术,来实现⼤型互联⽹电⼦商务⽹站架构建设和业务⽀撑,现要求成⽴运维技术保障部门,并邀请你担当运维部门经理,对整个运维部门进⾏部署和规划。当你拿到该......
  • Linux知识点
    LinuxLinux没有盘符这个概念,只有一个根目录/,所有文件都在它下面。./当前目录../上一级目录Linux主要目录速查表/根目录,一般根目录下只存放目录,在linux下有且只有一个根目录,所有的东西都是从这里开始。在终端里输入/home,其实是在告诉电脑,先从/(根目录)开始,再进入到hom......
  • linux 中查看各个子目录占用磁盘的大小
     001、[root@PC1test]#lsdir1dir2dir3[root@PC1test]#du-h##查看所有子目录占用磁盘的大小100M./dir1300M./dir230M./dir3430M. ......
  • 基于双目图像三维建模算法的测量目标物体体积计算matlab仿真
    1.算法仿真效果matlab2022a仿真结果如下:   2.算法涉及理论知识概要         双目立体视觉(BinocularStereoVision)是机器视觉的一种重要形式,它是基于视差原理并利用成像设备从不同的位置获取被测物体的两幅图像,通过计算图像对应点间的位置偏差,来获取物体三......
  • 高密度城市路线规划的遗传优化算法的matlab仿真,城市点数量达到500个
    1.算法仿真效果matlab2022a仿真结果如下:  2.算法涉及理论知识概要       遗传算法GA把问题的解表示成“染色体”,在算法中也即是以二进制编码的串。并且,在执行遗传算法之前,给出一群“染色体”,也即是假设解。然后,把这些假设解置于问题的“环境”中,并按适者生存的原......
  • MFSK调制方式的频谱效率,误码率,频谱等matlab仿真
    1.算法仿真效果matlab2022a仿真结果如下:2.算法涉及理论知识概要数字信号传输系统分为基带传输系统和频带传输系统.频带传输系统也叫数字调制系统。数字调制信号又称为键控信号,数字调制过程中处理的是数字信号,而载波有振幅、频率和相位3个变量,且二进制的信号只有高低电平两个逻......