| dbo:abstract
|
- TLA+, acronyme de « Temporal Logic of Actions » (« logique temporelle des actions » en anglais), est un système de méthode formelle pour les algorithmes parallèles et distribués. (fr)
- TLA+ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems. TLA+ is considered to be exhaustively-testable pseudocode, and its use likened to drawing blueprints for software systems; TLA is an acronym for Temporal Logic of Actions. For design and documentation, TLA+ fulfills the same purpose as informal technical specifications. However, TLA+ specifications are written in a formal language of logic and mathematics, and the precision of specifications written in this language is intended to uncover design flaws before system implementation is underway. Since TLA+ specifications are written in a formal language, they are amenable to finite model checking. The model checker finds all possible system behaviours up to some number of execution steps, and examines them for violations of desired invariance properties such as safety and liveness. TLA+ specifications use basic set theory to define safety (bad things won't happen) and temporal logic to define liveness (good things eventually happen). TLA+ is also used to write machine-checked proofs of correctness both for algorithms and mathematical theorems. The proofs are written in a declarative, hierarchical style independent of any single theorem prover backend. Both formal and informal structured mathematical proofs can be written in TLA+; the language is similar to LaTeX, and tools exist to translate TLA+ specifications to LaTeX documents. TLA+ was introduced in 1999, following several decades of research into a verification method for concurrent systems. Ever since, a toolchain has been developed, including an IDE and a distributed model checker. The pseudocode-like language PlusCal was created in 2009; it transpiles to TLA+ and is useful for specifying sequential algorithms. TLA+2 was announced in 2014, expanding language support for proof constructs. The current TLA+ reference is The TLA+ Hyperbook by Leslie Lamport. (en)
- TLA+は、Leslie Lamportによって開発された形式仕様言語。並行システムと分散システムの設計、モデル化、文書化、および検証に使用される。 TLA+は、網羅的にテスト可能な擬似コードとして説明されており、その使用はソフトウェアシステムの設計図を描くことに喩えられる。 TLAはTemporal Logic of Actionsの頭字語である。 設計と文書化に関して、TLA+ は非公式の技術仕様と同じ目的を果たす。ただし、TLA+の仕様は論理学と数学の形式言語で記述されており、この言語で記述された仕様の精度は、システムの実装が始まる前に設計上の欠陥を明らかにすることを目的としている。 TLA+のコードは形式言語で記述するため、有限モデル検査に適する。モデルチェッカーは、いくつかの実行ステップまでのすべての可能なシステム動作を見つけ、安全性や活性などの望ましい不変性プロパティの違反を調べる。 TLA+のコードでは、基本的な集合論を使用して安全性（悪いことが起こらない事）を定義し、時相論理を使用して活性（良いことがいずれ起こる事）を定義する。 TLA+は、アルゴリズムと数学的定理の両方について、マシンでチェックされた正確性の証明を作成するためにも使用される。証明は、単一の定理証明者バックエンドに依存しない宣言型の階層スタイルで記述される。公式および非公式の構造化された数学的証明は、TLA+で記述できる。言語はLaTeXに似ており、TLA+のコードをLaTeXドキュメントに翻訳するためのツールが存在する。 TLA+は、並行システムの検証方法に関する数十年の研究の後、1999年に公開された。その後、IDEや分散モデルチェッカーなどのツールチェーンが開発された。擬似コードのような言語PlusCalは2009年に作成され、TLA+にトランスパイルされ、シーケンシャルアルゴリズムを記述する際に有用とされる。 TLA+2は2014年に発表され、プルーフコンストラクトの言語サポートを拡張した。現在のTLA+リファレンスは、LeslieLamportによるTLA+Hyperbookである。 (ja)
- TLA+ — формальна мова специфікації, розроблена Леслі Лампортом і використовується для проектування, моделювання, документування й перевірки програм, особливо розподілених систем. TLA+ описана як вичерпно перевірений псевдокод, і її використання подібне до креслення; TLA є англійською абревіатурою для часової логіки дій. Що стосується дизайну та документації, TLA + виконує ту саму мету, що й неофіційні технічні умови. Однак специфікації TLA+ написані мовою логіки та математики, і точність специфікацій, написаних цією мовою, призначена для виявлення вад дизайну до початку впровадження системи. Оскільки специфікації TLA + написані офіційною мовою, вони піддаються перевірці з обмеженою моделлю. Модель перевірки знаходить усі можливі поведінки системи до деякої кількості етапів виконання та вивчає їх на порушення бажаних властивостей інваріантності, таких як безпека та життєздатність. Технічні характеристики TLA+ використовують базову теорію множин для визначення безпеки та часову логіку для визначення життєдіяльності. TLA+ також використовується для написання перевірених машиною доказів правильності як алгоритмів, так і математичних теорем. Докази написані в декларативному, ієрархічному стилі, незалежному від теореми. Як формальні, так і неофіційні структуровані математичні докази можуть бути записані у TLA+; мова схожа на LaTeX, і існують інструменти для перекладу специфікацій TLA+ до документів LaTeX. TLA+ була введена в 1999 році, після кількох десятиліть досліджень методу верифікації для одночасних систем. З тих пір було розроблено ланцюжок інструментів, що включає IDE та розподілену перевірку моделей. TLA+2 було оголошено у 2014 році, розширивши мовну підтримку для конструкцій із підтвердженням. (uk)
- TLA+ — язык спецификаций, основанный на теории множеств, логике первого порядка и темпоральной логике действий (англ. TLA, temporal logic of actions). Разработан Лесли Лэмпортом, исследователем теории распределённых систем. (ru)
|
| rdfs:comment
|
- TLA+, acronyme de « Temporal Logic of Actions » (« logique temporelle des actions » en anglais), est un système de méthode formelle pour les algorithmes parallèles et distribués. (fr)
- TLA+ — язык спецификаций, основанный на теории множеств, логике первого порядка и темпоральной логике действий (англ. TLA, temporal logic of actions). Разработан Лесли Лэмпортом, исследователем теории распределённых систем. (ru)
- TLA+ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems. TLA+ is considered to be exhaustively-testable pseudocode, and its use likened to drawing blueprints for software systems; TLA is an acronym for Temporal Logic of Actions. (en)
- TLA+は、Leslie Lamportによって開発された形式仕様言語。並行システムと分散システムの設計、モデル化、文書化、および検証に使用される。 TLA+は、網羅的にテスト可能な擬似コードとして説明されており、その使用はソフトウェアシステムの設計図を描くことに喩えられる。 TLAはTemporal Logic of Actionsの頭字語である。 設計と文書化に関して、TLA+ は非公式の技術仕様と同じ目的を果たす。ただし、TLA+の仕様は論理学と数学の形式言語で記述されており、この言語で記述された仕様の精度は、システムの実装が始まる前に設計上の欠陥を明らかにすることを目的としている。 TLA+のコードは形式言語で記述するため、有限モデル検査に適する。モデルチェッカーは、いくつかの実行ステップまでのすべての可能なシステム動作を見つけ、安全性や活性などの望ましい不変性プロパティの違反を調べる。 TLA+のコードでは、基本的な集合論を使用して安全性（悪いことが起こらない事）を定義し、時相論理を使用して活性（良いことがいずれ起こる事）を定義する。 (ja)
- TLA+ — формальна мова специфікації, розроблена Леслі Лампортом і використовується для проектування, моделювання, документування й перевірки програм, особливо розподілених систем. TLA+ описана як вичерпно перевірений псевдокод, і її використання подібне до креслення; TLA є англійською абревіатурою для часової логіки дій. Що стосується дизайну та документації, TLA + виконує ту саму мету, що й неофіційні технічні умови. Однак специфікації TLA+ написані мовою логіки та математики, і точність специфікацій, написаних цією мовою, призначена для виявлення вад дизайну до початку впровадження системи. (uk)
|
