بنیاد لینوکس پایه زبان TLA+ را راه اندازی کرد

TLA+ یک زبان برنامه نویسی سطح بالا است که برای مدل سازی برنامه ها و سیستم های پیچیده، همزمان و توزیع شده استفاده می شود. توسط Leslie Lamport ایجاد شده است و توسط Amazon Web Services، Microsoft و Oracle پشتیبانی می شود.

TLA+ (Temporal Logic of Actions)، یک زبان برنامه‌نویسی برای مدل‌سازی برنامه‌ها و سیستم‌ها، به‌ویژه برنامه‌های همزمان و توزیع‌شده، در حال انتقال از حوزه قضایی مایکروسافت به بنیاد لینوکس است و پایه جداگانه‌ای برای ارتقای آن ایجاد می‌کند.

بنیاد TLA+، یک سازمان غیرانتفاعی مستقل که به ترویج پذیرش و توسعه زبان اختصاص دارد، توسط بنیاد لینوکس در ۲۱ آوریل راه اندازی شد. بنیاد TLA+ آموزش و آموزش، تحقیقات مالی، توسعه ابزارها، و ایجاد جامعه ای از پزشکان را ارائه خواهد کرد. اعضای افتتاحیه بنیاد TLA+ شامل Oracle، Microsoft و Amazon Web Services (AWS) هستند.

بنیاد لینوکس گفت از زبان TLA+ برای تأیید سیستم های نرم افزاری پیچیده، کاهش خطاها و بهبود قابلیت اطمینان استفاده شده است. این زبان قصد دارد نقص‌های طراحی را در مراحل اولیه توسعه شناسایی کند تا در منابع و زمان صرفه‌جویی شود.

زیربنای TLA+ این مفهوم است که بهترین راه برای توصیف دقیق چیزها با ریاضیات ساده است. طبق گفته بنیاد لینوکس، TLA+ و ابزارهای آن برای از بین بردن خطاهای اساسی طراحی که یافتن آنها سخت است و تصحیح آن در کد هزینه بر است، مفید است. این زبان توسط دانشمند کامپیوتر لزلی لمپورت اختراع شد که اکنون یک دانشمند برجسته در تحقیقات مایکروسافت است.

در میان کاربران TLA+ Oracle است که از این زبان برای مدل‌سازی بیش از ۲۵ سرویس Oracle Cloud Infrastructure، از جمله سرویس‌های ذخیره‌سازی بلوکی و ذخیره‌سازی فایل، و تأیید صحت سناریوهای طراحی پیچیده از جمله تکرار توزیع‌شده، failover، استفاده کرده است. و اشتراک‌گذاری مجدد زنده.