بنیاد لینوکس سازمان جدیدی را برای حفظ TLA+ راه اندازی کرد
به گزارش اپ خونه، بنیاد لینوکس ، کنسرسیوم فناوری غیرانتفاعی که تلاشهای متنباز مختلف را مدیریت میکند، راهاندازی بنیاد TLA+ را برای ترویج پذیرش و توسعه زبان برنامهنویسی TLA+ اعلام کرد.
AWS، Oracle و Microsoft از جمله اعضای افتتاحیه هستند.
زبان برنامه نویسی TLA+ چیست؟ این یک زبان رسمی “مشخصات” است که توسط دانشمند کامپیوتر و ریاضیدان Leslie Lamport توسعه یافته است.
Lamport – که اکنون دانشمندی در مایکروسافت ریسرچ است – که بیشتر به خاطر کار مهم خود در سیستم های توزیع شده شناخته شده است، TLA+ را برای طراحی، مدل سازی، مستندسازی و تأیید برنامه های نرم افزاری – به ویژه برنامه های مختلف همزمان و توزیع شده- ایجاد کرد.
برای ارائه چند مثال، ElasticSearch، سازمانی که در پشت موتور جستجویی به همین نام قرار دارد، از TLA+ برای تأیید صحت الگوریتمهای سیستمهای توزیعشده خود استفاده کرد.
در جای دیگر، Thales، شرکت تولید کننده سیستمهای الکتریکی، از TLA+ برای مدلسازی و توسعه ماژولهای مقاوم در برابر خطا برای پلت فرم کنترل صنعتی خود استفاده کرد.
یکی از سخنگویان بنیاد لینوکس گفت :
« TLA+ از این نظر منحصر به فرد است که برای تعیین یک سیستم در نظر گرفته شده است، نه برای پیاده سازی نرم افزار».
“بر اساس مفاهیم ریاضی، بهویژه نظریه مجموعهها و منطق زمانی، TLA+ اجازه میدهد تا ویژگیهای صحت مورد نظر یک سیستم را به شیوهای رسمی و دقیق بیان کند.”
TLA+ شامل یک بررسی کننده مدل و اثبات قضیه برای بررسی اینکه آیا مشخصات یک سیستم دارای ویژگی های مورد نظر آن است یا خیر.
هدف کمک به توسعه دهندگان با استدلال در مورد سیستم های بالاتر از سطح کد، کشف و جلوگیری از نقص های طراحی (امیدوارم) قبل از تبدیل شدن به اشکالات در مراحل بعدی مهندسی نرم افزار است.
تا آخرین نقطه، شکست در طراحی نرمافزار بهطور شگفتآوری رایج و مخرب است.
گزارش سال ۲۰۲۰ از گروه Standish نشان داد که حدود ۶۶ درصد از پروژه های نرم افزاری با شکست مواجه می شوند و با توجه به کنسرسیوم برای اطلاعات و کیفیت نرم افزار، کیفیت ضعیف نرم افزار برای شرکت ها بیش از ۲ تریلیون دلار در سال ۲۰۲۰ هزینه دارد.
با تأسیس بنیاد TLA+، بنیاد لینوکس میگوید که منابع آموزشی را در مورد TLA+ فراهم میکند، تحقیقات را تأمین میکند و ابزارهایی را برای آن توسعه میدهد و برای پرورش جامعهای از پزشکان TLA+ تلاش میکند.
بنیاد TLA+ همچنین در مورد بهبود زبان، پاسخگویی به بازخورد کاربران و هدایت تکامل زبان تصمیم گیری خواهد کرد.
سخنگو ادامه داد:
«TLA+ قبلاً با موفقیت توسط شرکتهای فناوری بزرگ مانند آمازون، اوراکل و مایکروسافت برای تأیید و طراحی سیستمهای در مقیاس سیارهای استفاده شده است».
با ایجاد یک بنیاد TLA+ تحت چتر بنیاد لینوکس، TLA+ دید و پشتیبانی بیشتری به دست خواهد آورد و پذیرش گستردهتر آن را در صنعت فناوری ارتقا میدهد.
ماموریت بنیاد برای حمایت از پروژههای منبع باز تضمین میکند که TLA+ همچنان به تکامل خود ادامه میدهد و برای جامعه فناوری گستردهتر قابل دسترسی باقی میماند.
علاوه بر این، این بنیاد همکاری بیشتر بین صنعت و دانشگاه را تسهیل میکند، و وضعیت هنر را در روشهای رسمی و تحقیقات سیستمهای همزمان و توزیعشده پیش میبرد.