در مایکروسافت، تعداد فزاینده‌ای از تیم‌های مهندسی برای مشخص کردن و تأیید صحت الگوریتم‌ها و سیستم‌های نرم‌افزاری خود به TLA+ تکیه کرده‌اند. تیم‌های مهندسی با استفاده از TLA+ ارزش فوق‌العاده‌ای را در تعریف دقیق سیستم‌ها و اعتبارسنجی آنها در چرخه عمر مهندسی TLA+ ابزار گزارش کرده‌اند. دارما شوکلا، عضو فنی مایکروسافت، گفت: با پیوستن به بنیاد TLA+، هدف ما این است که جامعه ای از متخصصان TLA+ را که عمیقاً به طراحی درست سیستم های توزیع شده اهمیت می دهند، تقویت کنیم.
“بنیاد TLA+ از بسیاری جهات به موقع است. تفکر سیستماتیک و تحلیلی در مورد توسعه نرم افزار بیش از هر زمان دیگری مورد نیاز است. پیچیدگی سیستم های نرم افزاری اغلب شبکه ای در حال افزایش است و ما برای تحقق آن به ابزارهایی مانند TLA+ نیاز داریم.” وینت سرف، معاون رئیس جمهور و مبشر اصلی اینترنت در گوگل گفت.
“سرویس‌های ابری توزیع‌شده در مقیاس بزرگ، ستون فقرات همه پلت‌فرم‌های ابری ابر مقیاس، از جمله Oracle Cloud Infrastructure (OCI) هستند. هنگامی که ما در سال 2016 راه‌اندازی کردیم، OCI اولین ابری بود که از ابتدا با استفاده از روش‌های رسمی برای ارائه کیفیت بالا طراحی شد. خدمات ابری در OCI، ما از TLA+ در بیش از 25 مورد از حیاتی‌ترین سرویس‌های خود، از جمله سرویس‌های ذخیره‌سازی بلوکی و ذخیره‌سازی فایل، استفاده می‌کنیم تا صحت سناریوهای طراحی پیچیده از جمله تکرار توزیع‌شده، failover و پارتیشن‌بندی زنده را تأیید کنیم. به عنوان یک عضو موسس با هدف توسعه جعبه ابزار TLA+ و بهبود کیفیت خدمات ابری توزیع شده در سال های آینده.” پرادیپ وینسنت، SVP و معمار فنی ارشد OCI، Oracle گفت.
“اینریا متعهد به ترویج تحقیقات در بالاترین سطح بین المللی و انتقال نتایج این تحقیق به گونه ای است که آنها بر صنعت و جامعه تأثیر بگذارند. محققان اینریا در تکامل زبان TLA+ و طراحی ابزارهای تأیید برای TLA+ مشارکت داشته اند. استفان مرز، مدیر تحقیقات Inria و رئیس اینریا، گفت: ایجاد بنیاد TLA+ کمک می کند تا اطمینان حاصل شود که توسعه بیشتر زبان و ابزارهای آن، تلاش مشترک جامعه دانشگاهی و صنعتی گسترده تر علاقه مند به طراحی سیستم های توزیع شده قابل اعتماد خواهد بود. تیم پروژه VeriDis.
بنیاد TLA+ پذیرش را تشویق می‌کند، منابع آموزشی و آموزشی را فراهم می‌کند، تحقیقات را تأمین مالی می‌کند، ابزارها را توسعه می‌دهد و جامعه‌ای از پزشکان TLA+ ایجاد می‌کند. نقش بنیاد TLA+ به عنوان یک کمیته زبان، بهبود مستمر و تکامل زبان TLA+ را تضمین خواهد کرد. بنیاد TLA+ در مورد بهبود زبان تصمیم‌گیری می‌کند، به بازخوردها و نیازهای کاربران پاسخ می‌دهد، استانداردهای امنیتی و قابلیت اطمینان بالایی را حفظ می‌کند، و تکامل زبان را برای خدمت بهتر به پایگاه کاربر هدایت می‌کند.
به اعضای بنیاد TLA+ برای وبینار آموزشی “تسلط بر الگوریتم‌های همزمان با TLA+” در 14 ژوئن ساعت 8:00 صبح به وقت محلی بپیوندید. اینجا ثبت نام کنید.
مرجع اخبار سخت افزار کامپیوترایران
TLA+ و ابزارهای آن برای از بین بردن خطاهای اساسی طراحی که یافتن آنها سخت است و رفع آنها در کد هزینه بر است، مفید هستند. این زبان مبتنی بر این ایده است که بهترین راه برای توصیف دقیق چیزها، ریاضیات ساده است. این زبان ده ها سال پیش توسط دانشمند پیشگام کامپیوتر لزلی لمپورت، که اکنون دانشمندی برجسته در موسسه تحقیقاتی مایکروسافت است، اختراع شد. پس از سالها سرپرستی Lamport و پشتیبانی مایکروسافت، TLA+ خانه جدیدی در بنیاد لینوکس پیدا کرده است.
جیم زملین، مدیر اجرایی بنیاد لینوکس گفت: «تاسیس بنیاد TLA+ نشان دهنده تعهد به پیشبرد استفاده و توسعه زبان TLA+ به نفع کل صنعت نرم افزار است. “از آنجایی که جهان به طور فزاینده ای به سیستم های توزیع شده وابسته است، مهم است که توسعه دهندگان قابلیت های TLA+ را برای مدل سازی و تأیید رسمی اینکه سیستم ها مطابق انتظار عمل می کنند را داشته باشند.”
NVIDIA به طور فعال از روش‌های رسمی در توسعه نرم‌افزار و سخت‌افزار حیاتی ایمنی/امنیتی، از جمله TLA+ استفاده می‌کند، که ما از آن برای رسمی کردن طرح‌ها و الزامات خود استفاده می‌کنیم. مشارکت‌ها، تجربیات و بهترین شیوه‌ها را به اشتراک بگذارید. این می‌تواند به نیروی محرکه‌ای برای بهبود بیشتر محصول TLA+ تبدیل شود: زبان TLA+ را بهبود ببخشید، بررسی مدل را قوی‌تر کنید و استفاده از ابزارها را آسان‌تر کنید. همکاری مستقل و باز درون بنیاد برای ایمن‌سازی ضروری است. آینده TLA+ به‌عنوان یک اکوسیستم فعال و پرطرفدار. بنیاد TLA+ نیاز مهم دیگری را برآورده می‌کند؛ ترویج استفاده گسترده‌تر از روش‌های رسمی در صنعت برای بهبود کیفیت محصول، به ویژه در مواردی که ایمنی و امنیت ضروری هستند. تام مک‌رینولدز، مدیر ارشد DRIVE OS SW، NVIDIA گفت.
“از زمان آغاز به کار خود در سال 2020، سیستم های غیررسمی از TLA+ برای تعیین پروتکل های بلاک چین مانند Tendermint Consensus، Thin Client Protocol و پروتکل ارتباطات بین بلاک چین (IBC) استفاده کرده است. در ترکیب با Apalache Model Checker، این مشخصات اعتماد به نفس را تقویت کرده است. جامعه Cosmos در این پروتکل ها. ایگور کونوف، محقق اصلی در Informal گفت: انعطاف پذیری TLA+ همچنین به ما امکان می دهد برنامه ممیزی امنیتی را در مدت زمان کوتاهی شروع کنیم. سیستم های.
سان فرانسیسکو، 21 آوریل 2023 – بنیاد لینوکس، سازمان غیرانتفاعی که نوآوری انبوه را از طریق منبع باز امکان پذیر می کند، امروز راه اندازی بنیاد TLA+ را برای ترویج پذیرش و توسعه زبان برنامه نویسی TLA+ و جامعه پزشکان TLA+ آن اعلام کرد. اعضای افتتاحیه شامل خدمات وب آمازون (AWS)، اوراکل و مایکروسافت هستند. TLA+ یک زبان سطح بالا برای مدل‌سازی برنامه‌ها و سیستم‌ها، به‌ویژه برنامه‌های همزمان و توزیع‌شده است. TLA+ با موفقیت توسط شرکت ها برای تأیید سیستم های نرم افزاری پیچیده، کاهش خطاها و بهبود قابلیت اطمینان استفاده شده است. این زبان به شناسایی نقص های طراحی در مراحل اولیه توسعه کمک می کند و در زمان و منابع صرفه جویی می کند.
“AWS متعهد به ارائه خدمات با کیفیت بالا به مشتریان خود است، به همین دلیل است که تیم استدلال خودکار ما سال ها برای حل مشکلات طراحی به تکنیک هایی مانند مشخصات رسمی و بررسی مدل تکیه کرده است. در سیستم های حیاتی. TLA+ یک ابزار قدرتمند در ما است. بایرون کوک، معاون رئیس جمهور گفت: مجموعه ابزاری که به ما کمک می کند تا صحت سیستم های نرم افزاری خود را تحت فرضیات تأیید کنیم. با پیوستن به بنیاد TLA+، هدف ما حمایت از پیشرفت ابزار TLA+ و پیشرفت بیشتر در طراحی سیستم های توزیع شده است. و دانشمند بازنشسته در AWS.
بنیاد TLA+ از شرکت‌های فناوری دعوت می‌کند تا به مأموریت خود برای ترویج توسعه TLA+ در صنعت نرم‌افزار بپیوندند و از آن حمایت کنند. با همکاری، بنیاد TLA+ می‌تواند به بهبود قابلیت‌های این زبان مهم ادامه دهد و به اطمینان حاصل شود که مزایای TLA+ در دسترس همه است. برای اطلاعات بیشتر در مورد بنیاد TLA+، به foundation.tlapl.us مراجعه کنید
تحریریه Techpowerup
