بنیاد لینوکس سازمان جدیدی را برای حفظ TLA+ راه اندازی کرد

را لینوکس پایهکنسرسیوم فناوری غیرانتفاعی که تلاش‌های منبع باز مختلف را مدیریت می‌کند، امروز راه اندازی TLA+ را اعلام کرد پایه برای ترویج پذیرش و توسعه زبان برنامه نویسی TLA+. AWS، Oracle و Microsoft از جمله اعضای افتتاحیه هستند.

می پرسید زبان برنامه نویسی TLA+ چیست؟ این یک زبان رسمی “مشخصات” است که توسط دانشمند کامپیوتر و ریاضیدان Leslie Lamport توسعه یافته است. لامپورت – که اکنون دانشمندی در مایکروسافت ریسرچ است – که بیشتر به خاطر کار مهم خود در سیستم های توزیع شده شناخته شده است، TLA+ را برای طراحی، مدل سازی، مستندسازی و تأیید برنامه های نرم افزاری – به ویژه برنامه های مختلف همزمان و توزیع شده- ایجاد کرد.

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

“یکی از سخنگویان بنیاد لینوکس از طریق ایمیل به TechCrunch گفت: TLA+ از این نظر منحصر به فرد است که برای تعیین یک سیستم در نظر گرفته شده است، نه برای پیاده سازی نرم افزار. بر اساس مفاهیم ریاضی، به‌ویژه نظریه مجموعه‌ها و منطق زمانی، TLA+ اجازه می‌دهد تا ویژگی‌های صحت مورد نظر یک سیستم را به شیوه‌ای رسمی و دقیق بیان کند.

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

تا آخرین نقطه، شکست در طراحی نرم‌افزار به‌طور شگفت‌آوری رایج و مخرب است. گزارش سال 2020 از گروه Standish نشان داد که حدود 66 درصد از پروژه های نرم افزاری با شکست مواجه می شوند. و با توجه به کنسرسیوم برای اطلاعات و کیفیت نرم افزار، کیفیت ضعیف نرم افزار برای شرکت ها بیش از 2 تریلیون دلار در سال 2020 هزینه دارد.

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

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