لغة التحقق الرسمية من أنظمة البرمجيات

**TLA <sup>+</sup>** هي لغة مواصفات رسمية طورها Leslie Lamport . تُستخدم لتصميم ونمذجة وتوثيق والتحقق من البرامج، خاصة الأنظمة المتزامنة والأنظمة المُوزعة . يُعتبر TLA + شيفرة زائفة قابلة للاختبار بشكل شامل،  ويُشبه استخدامه برسم المخططات لأنظمة البرمجيات؛  *TLA* هو اختصار لـ Temporal Logic of Actions .في مجال التصميم والتوثيق، تؤدي لغة TLA + نفس دور المواصفات الفنية غير الرسمية.ومع ذلك، تُكتب مواصفات TLA +بلغة رسمية قائمة على المنطق والرياضيات، وتهدف دقة المواصفات المكتوبة بهذه اللغة إلى الكشف عن عيوب التصميم قبل البدء في تنفيذ النظام. 

نظرًا لأن مواصفات TLA + تُكتب بلغة رسمية، فهي قابلة للفحص باستخدام تقنيات التحقق من النماذج المنتهية. يقوم مدقق النموذج باكتشاف جميع سلوكيات النظام الممكنة حتى عدد معين من خطوات التنفيذ، ويفحصها للكشف عن أي انتهاكات لخصائص الثبات المطلوبة مثل الأمان والحيوية . تستخدم مواصفات TLA + نظرية المجموعة الأساسية لتحديد الأمان (لن تحدث أشياء سيئة) والمنطق الزمني لتحديد الحيوية (تحدث أشياء جيدة في النهاية).تُستخدم لغة TLA + أيضًا لكتابة براهين صحة يتم التحقق منها آليًا لكل من الخوارزميات والنظريات الرياضية. تُكتب هذه البراهين بأسلوب إعلاني هرمي مستقل عن أي نظام إثبات معين. يمكن كتابة البراهين الرياضية المنظمة الرسمية وغير الرسمية بلغة TLA + ؛ حيث تشبه اللغة لغة LaTeX ، وتوجد أدوات لترجمة مواصفات TLA + إلى مستندات LaTeX. 

تم تقديم لغة TLA + في عام 1999، بعد عدة عقود من البحث في طرق التحقق من صحة الأنظمة المتزامنة. ومُنذ ذلك الحين، تَم تطوير مجموعة أدوات متكاملة تشمل بيئة تطوير متكاملة IDE ومدقق النموذج الموزع.في عام 2009، تم إنشاء لغة البرمجة الشبيهة بالرمز PlusCal، وهي تنتقل إلى TLA + وهي مفيدة لتحديد الخوارزميات المتسلسلة. تم الإعلان عن TLA +2 في عام 2014، مما أدى إلى توسيع دعم اللغة لبناءات الإثبات. المرجع الحالي لـ TLA + هو The TLA <sup>+</sup> Hyperbook من تأليف Leslie Lamport.

## تاريخ
[بديل=Portrait of an Israeli man in his sixties. His hair is short and balding, and he is wearing glasses with a dress shirt and jacket.|تصغير| قام [أمير بنولي|أمير بنويلي بتطبيق المنطق الزمني على علوم الكمبيوتر، مما أدى إلى حصوله على جائزة تورينج عام 1996.]]
تم تطوير المنطق الزمني الحديث بواسطةآرثر براير في عام 1957، وكان يُعرف آنذاك بمنطق الزمن.

وعلى الرغم من أن أمير بنويلي كان أول من درس بجدية تطبيقات المنطق الزمني في علوم الحاسوب ، فقد تكهن براير باستخدامه قبل ذلك بعقد كامل في عام 1967:

أجرى بنويلي أبحاثًا حول استخدام المنطق الزمني في توصيف البرامج الحاسوبية، وقدم المنطق الزمني الخطي في عام 1977. أصبحت LTL أداة مهمة لتحليل البرامج المتزامنة، حيث تعبر بسهولة عن خصائص مثل الاستبعاد المتبادل والتحرر من الجمود . 

بالتزامن مع عمل بنويلي على منطق الزمن الخطيLTL، كان الباحثون الأكاديميون يعملون على تعميم منطق هوار للتحقق من صحة البرامج متعددة المعالجات. وقد بدأ ليزلي لامبورت اهتمامًا بالمشكلة بعد أن اكتشفوا في مراجعة الأقران خطأً في ورقة قدمها حول الاستبعاد المتبادل.

في عام 1975،قدّم إد أشكروفت مفهوم "الثبات" في ورقته البحثية، بعنوان "إثبات العبارات حول البرامج المتوازية"، وهو المفهوم الذي استخدمه لامبورت لتعميم طريقة فلويد في ورقته البحثية عام 1977 بعنوان "إثبات صحة برامج العمليات المتعددة". قدمت ورقة لامبورت أيضًا السلامة والحيوية كتعميمات للصحة الجزئية والإنهاء على التوالي.  تم استخدام هذه الطريقة للتحقق من أول خوارزمية لجمع القمامة المتزامنة في ورقة بحثية عام 1978 مع إدجر ديكسترا . 

اطّلع لامبورت لأول مرة على منطق الزمن الخطي (LTL) الخاص بـ Pnueli أثناء ندوة في جامعة ستانفورد عام 1978 نظمتها سوزان أويكي .

وفقًا للامبورت، "كنتُ متأكدًا أن منطق الزمن مجرد هراء نظري لا يمكن أن تكون له أي تطبيقات عملية، لكنه بدا ممتعًا، فحضرتُ."

و في عام1980، نشر مقالًا بعنوان "أحيانًا يكون أحيانًا ليس أبدًا"، والذي أصبح من أكثر الأوراق البحثية استشهادًا في أدبيات المنطق الزمني.  عمل لامبورت على كتابة مواصفات المنطق الزمني أثناء عمله في معهد SRI ، لكنه وجد أن النهج غير عملي:
[بديل=Portrait of a Caucasian man in his seventies with medium-length gray hair and a full gray beard, wearing glasses and a T-shirt.|تصغير| تم تطوير TLA <sup>+</sup> بواسطة عالم الكمبيوتر والحائز على جائزة تورينج لعام 2013 [ليسلي لامبورت|ليزلي لامبورت .]]

أثمر بحث لامبورت عن طريقة عملية لكتابة المواصفات عن ورقته البحثية عام 1983 بعنوان "تحديد وحدات البرمجة المتزامنة"، والتي قدّمت فكرة وصف تحولات الحالة على أنها دوال منطقية تعتمد على المتغيرات الأولية وغير الأولية. 

استمر العمل طوال ثمانينيات القرن العشرين، وبدأ لامبورت في نشر أوراقه البحثية حول المنطق الزمني للأفعال في عام 1990؛ ومع ذلك، لم يتم تقديمه رسميًا حتى نشر "المنطق الزمني للأفعال" في عام 1994. لقد مكّن TLA من استخدام الإجراءات في الصيغ الزمنية، والتي وفقًا لـ Lamport "توفر طريقة أنيقة لتنظيم وتنظيم كل الاستدلالات المستخدمة في التحقق المتزامن من النظام." 

تتكوَّن مواصفات TLA في الغالب من رياضيات غير زمنية، وهو ما وجده لامبورت أقل تعقيدًا من المواصفات الزمنية البحتة. وقد وفَّر TLA أساسًا رياضيًا للغة المواصفات TLA + ، التي قُدِمت في الورقة البحثية "تحديد الأنظمة المتزامنة باستخدام TLA + " في عام 1999. وفي نفس العام، كتب يوان يو أداة التحقق النموذجي TLC الخاصة بمواصفات TLA + ؛ وقد استُخدامت TLC لاكتشاف أخطاء في بروتوكول تماسك ذاكرة المخبئية في معالج متعدد الأنوية تابع لشركة من Compaq . 

نشر لامبورت كتابًا دراسيًا شاملًا حول TLA + في عام 2002، بعنوان "تحديد الأنظمة: لغة وأدوات TLA + لمهندسي البرمجيات". في عام 2009، قدّم لغة PlusCal  وتليها أداة إثبات المعروفة باسم TLA + proof (TLAPS) في عام 2012.  تم الإعلان عن TLA +2 في عام 2014، حيث أضاف بعض التراكيب اللغوية الإضافية بالإضافة إلى زيادة الدعم داخل اللغة لنظام الإثبات بشكل كبير.

لامبورت يعمل حاليًا على إعداد مرجع محدّث للغة تحت عنوان TLA + "The TLA + Hyperbook". وهو عمل غير مكتمل متاح على موقعه الرسمي. كما يقوم Lamport أيضًا بإنشاء دورة فيديو TLA <sup>+</sup> ، والتي تم وصفها فيها بأنها "عمل قيد التقدم يتكون من بداية سلسلة من محاضرات الفيديو لتعليم المبرمجين ومهندسي البرمجيات كيفية كتابة مواصفات TLA + بأنفسهم".

## اللغة
تُنظَّم مُواصفات TLA + فِي وحدات. حيث يمكن لكل وحدة النمطية أن تمتد أو تستورد وحدات أخرى لاستخدام وظائفها. على الرغم من أن معيار TLA + محدد في رموز رياضية منسقة، فإن أدوات TLA + الحالية تستخدم تعريفات رموز شبيهة بـ LaTeX في ASCII . يستخدم TLA + العديد من المصطلحات التي تتطلب التعريف:

* *الحالة* - تعيين القيم للمتغيرات
* *السلوك* – سلسلة من الحالات
* *الخطوة* - زوج من الحالات المتتالية في السلوك
* *خطوة التأتأة* - وهي خطوة لا تتغير فيها المتغيرات
* *علاقة الحالة التالية* - علاقة تصف كيف يمكن للمتغيرات أن تتغير في أي خطوة
* *دالة الحالة* - تعبير يحتوي على متغيرات وثوابت ليست علاقة حالة تالية
* *مسند الحالة* – دالة حالة ذات قيمة منطقية
* *ثابت* - مسند حالة صحيح في جميع الحالات التي يمكن الوصول إليها
* *الصيغة الزمنية* - عبارة تحتوي على عبارات في المنطق الزمني

## أمان

تهتم TLA + بتعريف مجموعة جميع السلوكيات الصحيحة للنظام. على سبيل المثال، يمكن تحديد ساعة ذات بت واحد تدق بلا نهاية بين 0 و1 على النحو التالي:
```text
الساعة المتغيرة 

Init == clock \in {0, 1}

Tick == IF clock = 0 THEN clock' = 1 ELSE clock' = 0

Spec == Init /\ [][Tick]_<<clock>>
```
علاقة الحالة التالية **Tick** تحدد قيمة *clock* ′ (قيمة *clock* في الحالة التالية) إلى 1 إذا كانت *clock* تساوي 0، و0 إذا كانت *clock* تساوي 1.

المتغير الشرطي **Init** يكون صحيحًا إذا كانت قيمة *clock* إما 0 أو 1.

المواصفة **Spec** هي صيغة زمنية تنص على أن جميع سلوكيات ساعة البت الواحد يجب أن تحقق بداية **شرط Init** وأن كل خطوة إما متطابقة مع **Tick** أو خطوات متقطعة. ومن بين هذه السلوكيات:
```text
0 -> 1 -> 0 -> 1 -> 0 -> ...

1 -> 0 -> 1 -> 0 -> 1 -> ...
```
خصائص السلامة لساعة البت الواحد&nbsp;- أي مجموعة الحالات النظامية الممكن الوصول إليها&nbsp;- يتم وصفها بشكل مناسب بالمواصفات.

## الحيوية

المواصفة السابقة تمنع الحالات الغريبة للساعة ذات البت الواحد، ولكنها لا تقول إن الساعة سوف تدق على الإطلاق. على سبيل المثال، يتم قبول السلوكيات التالية التي تؤدي إلى التأتأة بشكل دائم:
```text
وهما: 
 0 -> 0 -> 0 -> 0 -> 0 -> ... 

1 -> 1 -> 1 -> 1 -> 1 -> ...
```
الساعة التي لا تدقّ ليست مفيدة، لذا يجب استبعاد هذه السلوكيات. إحدى الحلول هي تعطيل التوقف، لكن TLA + يشترط أن يكون التوقف ممكنًا دائمًا؛ تمثل خطوة التلعثم تغييرًا في جزء من النظام غير الموصوف في المواصفات، وهي مفيدة للتحسين . ولضمان أن عقارب الساعة يجب أن تدق في النهاية، يتم التأكيد على ضعف العدالة فيما يتعلق بـ **Tick** :
```text
Spec == Init /\ [][Tick]_<<clock>> /\ WF_<<clock>>(Tick)
```
العدالة الضعيفة بالنسبة لفعل معين تعني أنه إذا كان هذا الفعل ممكنًا بشكل مستمر، فلا بد أن يتم تنفيذه في نهاية المطاف. في حالة الإنصاف الضعيف في **علامة التجزئة،** يُسمح فقط بعدد محدود من خطوات التلعثم بين العلامات. يُطلق على هذه العبارة المنطقية الزمنية حول **تيك** اسم تأكيد الحيوية. بشكل عام، يجب أن يكون تأكيد الحيوية *مغلقًا آليًا* : لا ينبغي أن يقيد مجموعة الحالات التي يمكن الوصول إليها، بل مجموعة السلوكيات الممكنة فقط. 

معظم المواصفات لا تتطلب إثبات خصائص الحيوية. إذ تكفي خصائص السلامة لكل من التحقق من النموذج التوجيه في تنفيذ النظام. 

## المشغلين
تعتمد لغة TLA + على نظام زيرميلو-فرانكل ZF ، لذا تتضمن العمليات على المتغيرات التعامل مع المجموعات. تشمل اللغة مجموعة العضوية ، والاتحاد ، والتقاطع ، والفرق ، ومجموعة القوى ، ومشغلات المجموعة الفرعية . كما تتضمن اللغة أيضًا مشغلات المنطق من الدرجة الأولى مثل  و  و  و  و  و  ، بالإضافة إلى الكميات العالمية والوجودية  و  . كما تتوفر أداة هيلبرت كعامل CHOOSE، الذي يختار عنصرًا فريدًا وعشوائيًا من مجموعة معينة. وتحتوي العمليات الحسابية على الأعداد الحقيقية ، والأعداد الصحيحة ، والأعداد الطبيعية من الوحدات النمطية القياسية.

تحتوي لغة TLA + على مُشغلات زمنية مدمجة. تستخدم الصيغ الزمنية الرموز التالية: \Box P تعني أن العبارة *P* صحيحة دائمًا، و \Diamond P تعني أن *P* صحيح في النهاية. ويمكن دمج هذه المُشغّلات مثل:

\Box \Diamond P تعني أن العبارة *P* صحيحة بشكل متكرر إلى ما لا نهاية، أو \Diamond \Box P أن يعني في النهاية أن *P* سوف يكون صحيحًا دائمًا.

تشمل المشغلات الزمنية الأخرى العدل الضعيف والعادل القوي. إن العدالة الضعيفة WF e ( *A* ) تعني أنه إذا تم تمكين الإجراء *A* *بشكل مستمر* (أي بدون انقطاعات)، فيجب اتخاذه في النهاية. العدالة القوية SF e ( *A* ) تعني أنه إذا تم تمكين الإجراء *A* *بشكل مستمر* (بشكل متكرر، مع أو بدون انقطاعات)، فيجب اتخاذه في النهاية.

تتضمن لغة TLA + ، على الرغم من عدم وجود دعم من الأدوات.

المعاملات المعرفة من قبل المستخدم تشبه الماكرو . وتختلف المعاملات عن الوظائف في أن مجالها لا يشترط أن يكون مجموعة: فعلى سبيل المثال، معامل عضوية المجموعة لديه فئة المجموعات كمجال له، وهي ليست مجموعة صالحة في ZFC (نظرًا لأن وجودها يؤدي إلى مفارقة راسل ). تمت إضافة مشغلات محددة من قبل المستخدم متكررة ومجهولة في TLA +2 .

## هياكل البيانات
البنية الأساسية للبيانات في TLA + هي المجموعة. تُنشأ المجموعات إما بالتعداد الصريح لعناصرها، أو من مجموعات أخرى باستخدام معاملات، أو بصيغة 
```tex
{x \in S : p}
```
 حيث *p* هو شرط على *x* ، أو بصيغة 
```tex
{e : x \in S}
```
 حيث *e* دالة على *x* . المجموعة الفارغة الفريدة تُمثَّل بـ `{}` .

الوظائف في TLA + تُسنِد قيمة لكل عنصر في مجالها، والذي يكون مجموعة. التعبير `[S -> T]`يمثل مجموعة جميع الدوال التي يكون فيها f[ *x* ] منتمية إلى *T* ، لكل *x* في مجموعة المجال *S.*

على سبيل المثال، الدالة في TLA + `Double[x \in Nat] == x*2` هي عنصر من المجموعة `[Nat -> Nat]` وبالتالي فإن العبارة `Double \in [Nat -> Nat]` هي عبارة صحيحة في TLA + . كما يمكن تعريف الوظائف باستخدام الصيغة `[x \in S |-> e]` لبعض التعبيرات *e* ، أو عن طريق تعديل وظيفة موجودة `[f EXCEPT ![v <sub>1</sub> ] = v <sub>2</sub> ]` .

السجلات هِي نَوُع من الوظائف في TLA + . السجل `[name |-> "John", age |-> 35]` هو سجل يحتوي على الحقول name وage، ويمكن الوصول إليه باستخدام `r.name` و `r.age` .

هذا السجل ينتمي إلى مجموعة السجلات المعرفة بالشكل `[name : String, age : Nat]` .

تتضمّن العناصر في TLA + . يتم تعريفها صراحةً هذه باستخدام الصيغة `<<e <sub>1</sub> ,e <sub>2</sub> ,e <sub>3</sub> >>` أو يمكن إنشاؤها باستخدام المعاملات الموجودة في التسلسلات القياسية. يتم تعريف مجموعات الكائنات المرتبة من خلال حاصل الضرب الديكارتي ؛ على سبيل المثال، تُعرَّف مجموعة جميع أزواج الأعداد الطبيعية بـ `Nat \X Nat` .

## الوحدات القياسية
تمتلك TLA + مجموعة من الوحدات القياسية التي تحتوي على المعاملات الشائعة. يتم توزيع هذه الوحدات من محلل الصياغة. ويستخدم مدقق النماذج TLC نسخًا مُنفذة بلغة Java لتحسين الأداء.

* **FiniteSets** : وحدة للعمل مع المجموعات المحدودة . يوفر مشغلي *IsFiniteSet(S)* و *Cardinality(S)* .
* **التسلسلات** : تحدد المشغلات على الثنائيات مثل *Len(S)* ، *و Head(S)* ، و *Tail(S)* ، و *Append(S, E)* ، و concatenation ، و filter .
* **الحقائب** : وحدة للعمل مع مجموعات متعددة . يوفر نظائر تشغيل المجموعة البدائية والعد المكرر.
* **الأعداد الطبيعية** : تحدد الأعداد الطبيعية إلى جانب المتباينات والعمليات الحسابية.
* **الأعداد الصحيحة** : تُعرَّف الأعداد الصحيحة .
* **الأعداد الحقيقية** : تحدد الأعداد الحقيقية إلى جانب القسمة واللانهاية .
* **الوقت الحقيقي** : يوفر تعريفات مفيدة في مواصفات النظام في الوقت الحقيقي .
* **TLC** : توفر وظائف مفيدة للمواصفات التي تم فحصها بواسطة النموذج، مثل التسجيل والتأكيدات.

يتم استيراد الوحدات القياسية في TLA+ باستخدام عبارتي `EXTENDS` أو `INSTANCE` .

## الأدوات

### بيئة تطوير متكاملة

بيئة تطوير متكاملة تم تنفيذها على منصة Eclipse . تتضمن محررًا مع تمييز الأخطاء والنحو ، بالإضافة إلى واجهة رسومية أمامية لعدة أدوات أخرى من TLA + :

* محلل بناء الجملة SANY، الذي يقوم بتحليل المواصفات والتحقق منها بحثًا عن أخطاء بناء الجملة.
* مترجم LaTeX ، لتوليد مواصفات مطبوعة بشكل جميل .
* مترجم PlusCal.
* مدقق نموذج TLC.
* نظام إثبات TLAPS.

يتم توزيع IDE في The TLA Toolbox .

### فاحص النموذج
بديل=Finite state machine diagram of one-bit clock|تصغير| الحالات والانتقالات التي تم اكتشافها بواسطة TLC للساعة ذات البت الواحد.
نماذج فاحص نموذج TLC يقوم ببناء نموذج ذو حالة محدودة من المواصفات TLA + لفحص خصائص الثبات . يقوم TLC بتوليد مجموعة من الحالات الابتدائية التي تحقق المواصفة، ثم ينفذ بحثًا بعرض الأولوية على جميع انتقالات بين الحالات المعرفة. تتوقف العملية عندما تؤدي جميع انتقالات الحالة إلى حالات تم اكتشافها بالفعل. إذا اكتشف TLC حالة تنتهك أحد الثوابت في النظام، فإنه يتوقف ويوفر مسار تتبع الحالة إلى الحالة المخالفة. توفر TLC طريقة لإعلان تماثلات النموذج للدفاع ضد الانفجار التركيبي .  كما أنه يقوم بموازاة خطوة استكشاف الحالة، ويمكن تشغيله في وضع موزع لتوزيع عبء العمل عبر عدد كبير من أجهزة الكمبيوتر. 

كبديل للبحث الشامل بعرض الأولية، يمكن لـ TLC استخدام البحث بعمق الأولوية أو توليد سلوكيات عشوائية. يعمل TLC على مجموعة فرعية من TLA + ؛ حيث يجب أن يكون النموذج محدودًا وقابلًا للعد، كما أن بعض المشغلات الزمنية غير مدعومة. في الوضع الموزع، لا يمكن لـ TLC التحقق من خصائص الحيوية، ولا التحقق من السلوكيات العشوائية أو السلوكيات التي تركز على العمق أولاً. يتوفر TLC كأداة لسطر الأوامر أو مضمنًا مع مجموعة أدوات TLA.

### نظام الإثبات
نظام إثبات TLA +،المعروف بـ TLAPS، يقوم بالتحقق الميكانيكي من البراهين المكتوبة بلغة TLA + . تم تطويره في المركز Microsoft Research - INRIA المشترك لإثبات صحة الخوارزميات المتزامنة والموزعة. لغة الإثبات مصممة لتكون مستقلة عن أي مُثبت نظريات محدد؛ حيثُ تُكتب البراهين بأسلوب تصريحي، وتُحوّل إلى التزامات فردية تُرسل إلى مُثبتات خلفية. المثبتات الخلفية الرئيسية هي Isabelle وZenon، مع الرجوع إلى حلول SMT CVC3 و Yices و Z3 . تتميز أدلة TLAPS بأنها منظمة بشكل هرمي، مما يسهل إعادة الهيكلة وتمكين التطوير غير الخطي: يمكن أن يبدأ العمل في الخطوات اللاحقة قبل التحقق من جميع الخطوات السابقة، ويتم تقسيم الخطوات الصعبة إلى خطوات فرعية أصغر. يعمل TLAPS بشكل جيد مع TLC، حيث يكتشف مدقق النموذج بسرعة الأخطاء الصغيرة قبل بدء التحقق. في المقابل، يمكن لـ TLAPS إثبات خصائص النظام التي تتجاوز قدرات فحص النموذج المحدود. 

نظام إثبات TLAPS لا يدعم حاليًا الاستدلال بالأعداد الحقيقية، ولا معظم العمليات الزمنية. عادةً ما لا يستطيع إيزابيل وزينون إثبات التزامات الإثبات الحسابية، مما يتطلب استخدام مثبتات SMT.  تم استخدام TLAPS لإثبات صحة Byzantine Paxos ، وهندسة أمان Memoir، ومكونات جدول التجزئة الموزع Pastry ،  وخوارزمية إجماع Spire.  يتم توزيعه بشكل منفصل عن باقي أدوات TLA + وهو برنامج حر يُوزع تحت ترخيص BSD . وقد وسع TLA +2 بشكل كبير في دعم اللغة لبناءات الإثبات.

## استخدام الصناعة
في شركة Microsoft ، تَمَ اكتشاف خطأ حرج في وحدة ذاكرة Xbox 360 أثناء عملية كتابة المواصفات باستخدام TLA + .  استُخدام TLA + أيضًا لكتابة براهين رسمية لصحة Byzantine Paxos ومكونات جدول التجزئة الموزع Pastry . 

تستخدم Amazon Web Services تقنية TLA + منذ عام 2011. كشف التحقق من النماذج باستخدام TLA + عن أخطاء في DynamoDB و S3 و EBS ومدير القفل الموزع الداخلي؛ بعض هذه الأخطاء تطلّب تتبع حالة يتضمن 35 خطوة. كما استُخدم التحقق من النماذج للتحقق من صحة تحسينات متقدمة. بالإضافة إلى ذلك، وُجد أن مواصفات TLA + تحمل قيمة كبيرة كوثائق ومساعدات في التصميم.  

استخدمت Microsoft Azure تقنية TLA + لتصميم Cosmos DB ، وهي قاعدة بيانات موزعة عالميًا تدعم خمسة نماذج مختلفة للاتساق.  

استخدمت شركة Altreonic NV أداة TLA+ للتحقق من نموذج OpenComRTOS .

## الأمثلة
متجر القيمة الرئيسية مع عزل اللقطة :
```text
--------------------------- MODULE KeyValueStore ---------------------------
CONSTANTS  Key,      \* The set of all keys.
      Val,      \* The set of all values.
      TxId      \* The set of all transaction IDs.
VARIABLES  store,     \* A data store mapping keys to values.
      tx,       \* The set of open snapshot transactions.
      snapshotStore, \* Snapshots of the store for each transaction.
      written,    \* A log of writes performed within each transaction.
      missed     \* The set of writes invisible to each transaction.
----------------------------------------------------------------------------
NoVal ==  \* Choose something to represent the absence of a value.
  CHOOSE v : v \notin Val

Store ==  \* The set of all key-value stores.
  [Key -> Val \cup {NoVal}]

Init == \* The initial predicate.
  /\ store = [k \in Key |-> NoVal]    \* All store values are initially NoVal.
  /\ tx = {}               \* The set of open transactions is initially empty.
  /\ snapshotStore =           \* All snapshotStore values are initially NoVal.
    [t \in TxId |-> [k \in Key |-> NoVal]]
  /\ written = [t \in TxId |-> {}]    \* All write logs are initially empty.
  /\ missed = [t \in TxId |-> {}]     \* All missed writes are initially empty.
  
TypeInvariant ==  \* The type invariant.
  /\ store \in Store
  /\ tx \subseteq TxId
  /\ snapshotStore \in [TxId -> Store]
  /\ written \in [TxId -> SUBSET Key]
  /\ missed \in [TxId -> SUBSET Key]
  
TxLifecycle ==
  /\ \A t \in tx :  \* If store != snapshot & we haven't written it, we must have missed a write.
    \A k \in Key : (store[k] /= snapshotStore[t][k] /\ k \notin written[t]) => k \in missed[t]
  /\ \A t \in TxId \ tx : \* Checks transactions are cleaned up after disposal.
    /\ \A k \in Key : snapshotStore[t][k] = NoVal
    /\ written[t] = {}
    /\ missed[t] = {}

OpenTx(t) ==  \* Open a new transaction.
  /\ t \notin tx
  /\ tx' = tx \cup {t}
  /\ snapshotStore' = [snapshotStore EXCEPT ![t] = store]
  /\ UNCHANGED <<written, missed, store>>

Add(t, k, v) == \* Using transaction t, add value v to the store under key k.
  /\ t \in tx
  /\ snapshotStore[t][k] = NoVal
  /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v]
  /\ written' = [written EXCEPT ![t] = @ \cup {k}]
  /\ UNCHANGED <<tx, missed, store>>
  
Update(t, k, v) == \* Using transaction t, update the value associated with key k to v.
  /\ t \in tx
  /\ snapshotStore[t][k] \notin {NoVal, v}
  /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v]
  /\ written' = [written EXCEPT ![t] = @ \cup {k}]
  /\ UNCHANGED <<tx, missed, store>>
  
Remove(t, k) == \* Using transaction t, remove key k from the store.
  /\ t \in tx
  /\ snapshotStore[t][k] /= NoVal
  /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = NoVal]
  /\ written' = [written EXCEPT ![t] = @ \cup {k}]
  /\ UNCHANGED <<tx, missed, store>>
  
RollbackTx(t) ==  \* Close the transaction without merging writes into store.
  /\ t \in tx
  /\ tx' = tx \ {t}
  /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]]
  /\ written' = [written EXCEPT ![t] = {}]
  /\ missed' = [missed EXCEPT ![t] = {}]
  /\ UNCHANGED store

CloseTx(t) ==  \* Close transaction t, merging writes into store.
  /\ t \in tx
  /\ missed[t] \cap written[t] = {}  \* Detection of write-write conflicts.
  /\ store' =             \* Merge snapshotStore writes into store.
    [k \in Key |-> IF k \in written[t] THEN snapshotStore[t][k] ELSE store[k]]
  /\ tx' = tx \ {t}
  /\ missed' =  \* Update the missed writes for other open transactions.
    [otherTx \in TxId |-> IF otherTx \in tx' THEN missed[otherTx] \cup written[t] ELSE {}]
  /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]]
  /\ written' = [written EXCEPT ![t] = {}]

Next == \* The next-state relation.
  \/ \E t \in TxId : OpenTx(t)
  \/ \E t \in tx : \E k \in Key : \E v \in Val : Add(t, k, v)
  \/ \E t \in tx : \E k \in Key : \E v \in Val : Update(t, k, v)
  \/ \E t \in tx : \E k \in Key : Remove(t, k)
  \/ \E t \in tx : RollbackTx(t)
  \/ \E t \in tx : CloseTx(t)
    
Spec == \* Initialize state with Init and transition with Next.
  Init /\ [][Next]_<<store, tx, snapshotStore, written, missed>>
----------------------------------------------------------------------------
THEOREM Spec => [](TypeInvariant /\ TxLifecycle)
=============================================================================
```


## انظر أيضًا

* التواصل بشأن العمليات المتسلسلة
* سبيكة (لغة المواصفات)
* الطريقة ب
* منطق شجرة الحساب
* بلس كال
* المنطق الزمني
* المنطق الزمني للأفعال
* تدوين Z

## المراجع



تصنيف:تزامن (حوسبة)
تصنيف:لغات المواصفات
تصنيف:برمجيات تسخدم رخصة بي إس دي
تصنيف:طرق شكلية
تصنيف:جميع المقالات ذات الوصلات الخارجية المكسورة