本アナウンスは Linux Foundation Announces Launch of TLA+ Foundation の参考訳です
頑強なソフトウェアのための実証済みの形式手法の普及を促進するため、TLA+ Foundationを設立
2023年4月21日 サンフランシスコ発 ― オープンソースを通じて大規模イノベーションを推進する非営利団体Linux Foundationは、TLA+プログラミング言語およびTLA+実践者コミュニティの採用と開発を促進するため、TLA+ Foundationの発足を発表しました。発足メンバーには、Amazon Web Services(AWS)、Oracle、Microsoftが名を連ねています。
TLA+は、プログラムやシステム、特に並列および分散されたものをモデリングするための高水準言語です。TLA+は、複雑なソフトウェア システムを検証し、エラーを減らし、信頼性を向上させるために企業によって成功裏に使用されてきました。この言語は、開発プロセスの初期段階で設計上の欠陥を検出し、時間とリソースを節約するのに役立ちます。
TLA+とそのツールは、コード内で見つけるのが難しく、修正にコストがかかる基本的な設計エラーを排除するのに役立ちます。この言語は、物事を正確に記述する最善の方法は単純な数学であるという考えに基づいています。
この言語は、数十年前に先駆的なコンピューター科学者であり、現在はMicrosoft Researchの著名な科学者であるLeslie Lamport氏によって発明されました。Lamport氏の長年の管理とMicrosoftの支援の後、TLA+はLinux Foundationに新たな拠点を見つけました。
Linux Foundationのエグゼクティブ ディレクターであるJim Zemlinは、次のように述べています。
「TLA+ Foundationの設立は、ソフトウェア業界全体の利益のためにTLA+言語の使用と開発を推進するというコミットメントを示すものです。世界の分散システムへの依存度が高まるにつれて、システムが意図したとおりに動作することを正式にモデル化し、検証するTLA+の機能を開発者が持つことが重要になっています。」
TLA+ Foundationは、TLA+の採用を促進し、教育とトレーニングのリソースを提供し、研究に資金を提供し、ツールを開発し、TLA+実践者のコミュニティを構築します。言語委員会としてのTLA+ Foundationの役割は、TLA+言語の継続的な改善と進化を保証することです。TLA+ Foundationは、言語の拡張に関する決定を行い、ユーザーのフィードバックとニーズに対応し、高い安全性と信頼性の基準を維持し、ユーザー ベースにより良いサービスを提供するために言語の進化を導きます。
参加メンバーの声 : 正確な記述に関しては原文をご参照ください
AWSのVice PresidentでDistinguished ScientistであるByron Cook氏は、次のように述べています。”AWSは、お客様に高品質のサービスを提供することに尽力しています。そのため、Automated Reasoning teamは、重要なシステムにおける困難な設計問題を解決するために、長年にわたって形式仕様やモデル チェックなどの技術に依存してきました。TLA+は、仮定の下でソフトウェア システムの正確性を検証するのに役立つ、ツールボックス内の強力なツールです。TLA+ Foundationに参加することで、TLA+ツールの進歩をサポートし、分散システム設計における最先端技術をさらに向上させることを目指しています。”
MicrosoftのTechnical FellowであるDharma Shukla氏は次のように述べています。”Microsoft全体で、ますます多くのエンジニアリング チームが、アルゴリズムとソフトウェア システムの正確性を明示し、検証するためにTLA+に依存しています。TLA+を使用するエンジニアリング チームは、システムを正確に定義し、エンジニアリング ライフサイクルの早い段階で検証することに大きな価値があると報告しています。TLA+ツールは、1行のコードを作成する前に設計の問題を特定するのに役立っています。TLA+ Foundationに参加することで、正しい分散システムの設計に深く関心を持つTLA+実践者のコミュニティを育成することを目指しています。”
OracleのSVPでOCI Chief Technical ArchitectであるPradeep Vincent氏は次のように述べています。”大規模な分散クラウド サービスは、Oracle Cloud Infrastructure(OCI)を含むすべてのハイパースケーラ クラウド プラットフォームのバックボーンを形成しています。2016年にローンチしたとき、OCIは、高品質のクラウド サービスを提供するために、最初から形式手法を使用して設計された最初のクラウドでした。OCIでは、ブロック ストレージやファイル ストレージ サービスを含む25以上の最も重要なサービスでTLA+を使用して、分散レプリケーション、フェイルオーバ、ライブ リシャーディングなどの複雑な設計シナリオの正確性を検証しています。TLA+ツールキットを推進し、今後数年間の分散クラウド サービスの品質を向上させることを目的として、TLA+ Foundationに設立メンバーとして参加できることを嬉しく思います。”
GoogleのVice PresidentでChief Internet EvangelistであるVint Cerf氏は次のように述べています。”TLA+ Foundationは非常に多くの点で時宜を得ています。ソフトウェア開発について体系的かつ分析的に考えることは、今まで以上に必要とされています。しばしばネットワークで使用されるソフトウェア システムの複雑さは増しており、TLA+のようなツールが必要です。”
”2020年の開始以来、Informal SystemsはTLA+を使用して、Tendermint Consensus、light client protocol、Inter-blockchain Communication Protocol(IBC)などのブロックチェーン プロトコルを記述してきました。Apalacheモデル チェッカーとの組み合わせにより、これらの仕様は、これらのプロトコルにおけるCosmosコミュニティの信頼を強化しました。TLA+の柔軟性により、セキュリティ監査プログラムを短期間で立ち上げることもできます。Cosmos Technologyを搭載した分散アプリケーションでセキュリティ問題を検出するためにApalacheを適用しました。”と、Informal SystemsのPrincipal Research ScientistであるIgor Konnov氏は述べています。
InriaのSenior Researcherであり、VeriDis project teamのHeadであるStephan Merz氏は次のように述べています。”Inriaは、最高の国際レベルでの研究を促進するとともに、その研究結果を産業や社会に影響を与えるように移転することにコミットしています。Inriaの研究者は、TLA+言語の進化とTLA+の検証ツールの設計に貢献してきました。TLA+ Foundationの設立は、TLA+言語とそのツールのさらなる開発が、信頼できる分散システムの設計に関心を持つ、より大きな学術および産業コミュニティの共同作業となることを確実にするのに役立ちます。”
NVIDIAのSenior Director DRIVE OS SWであるTom McReynolds氏は、次のように述べています。”NVIDIAは、安全／セキュリティに重要なソフトウェアやハードウェアの開発において、TLA+を含む形式手法を積極的に使用しており、設計や要件の形式化に利用しています。TLA+ Foundationは、貢献、経験、およびベストプラクティスを共有するための専門的に管理されたプラットフォームを提供することによって、重要なギャップを埋めると考えています。TLA+ Foundationは、TLA+製品をさらに向上させる原動力となることができます：TLA+言語を強化し、モデル チェックをより強力にし、ツールを使いやすくします。積極的に開発され、人気のあるエコ システムとしてのTLA+の将来を確保するためには、TLA+ Foundation内の独立したオープンなコラボレーションが必要です。TLA+ Foundationは、もう1つの重要なニーズを満たしています。それは、製品の品質を向上させるために、業界で形式方法をより広く使用することを促進することです。特に、安全とセキュリティが重要な場合にはそうです。”
TLA+ Foundationは、ソフトウェア業界におけるTLA+の開発を促進するという使命を果たすために、テクノロジー企業の参加と支援を呼びかけています。TLA+ Foundationが協力することで、この重要な言語の機能が強化され、TLA+のメリットをすべての人が利用できるようになります。
TLA+ Foundationの詳細については、https://foundation.tlapl.usをご覧ください。
TLA+ Foundationのメンバーは、6月14日午前8:00 PT（太平洋時間）に開催される教育ウェビナー”Mastering Concurrent Algorithms with TLA+”にご参加ください。こちらから登録可能です。
翻訳協力：橋本修太
