TLA +

لغة TLA ⁺ هي لغة مواصفات رسمية طورتها ليزلي لامبورت . تُستخدم لتصميم البرامج ونمذجتها وتوثيقها والتحقق منها، وخاصة الأنظمة المتزامنة والأنظمة الموزعة . تُعتبر TLA ⁺شبه كود قابل للاختبار الشامل ، ^{[ 4 ]} ويُشبه استخدامها رسم المخططات الأولية لأنظمة البرمجيات؛ ^{[ 5 ]} TLA هو اختصار لـ "المنطق الزمني للأفعال" .

لأغراض التصميم والتوثيق، يؤدي TLA ⁺ نفس الغرض الذي تؤديه المواصفات الفنية غير الرسمية . ومع ذلك، تُكتب مواصفات TLA ⁺ بلغة رسمية من المنطق والرياضيات، وتهدف دقة المواصفات المكتوبة بهذه اللغة إلى الكشف عن عيوب التصميم قبل بدء تنفيذ النظام. ^{[ 6 ]}

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

تُستخدم لغة TLA ⁺ أيضًا لكتابة براهين صحة مُدققة آليًا لكلٍ من الخوارزميات والنظريات الرياضية. تُكتب البراهين بأسلوب تصريحي هرمي مستقل عن أي نظام خلفي لإثبات النظريات. يمكن كتابة البراهين الرياضية الرسمية وغير الرسمية باستخدام TLA ⁺ ؛ فاللغة مشابهة للغة LaTeX ، وتتوفر أدوات لترجمة مواصفات TLA ⁺ إلى مستندات LaTeX. ^{[ 7 ]}

طُرحت لغة TLA ^{+ عام 1999، بعد عقود من البحث في أساليب التحقق من صحة الأنظمة المتزامنة. ومنذ ذلك الحين، جرى تطوير مجموعة أدوات متكاملة، تشمل بيئة تطوير متكاملة}(IDE) ومدقق نماذج موزع. وفي عام 2009، أُنشئت لغة PlusCal ، وهي لغة شبيهة بالشيفرة الزائفة ، تُترجم إلى TLA ⁺ وتُستخدم لتحديد الخوارزميات التسلسلية. وفي عام 2014، أُعلن عن TLA ⁺² ، مما وسّع دعم اللغة لبنى البرهان. ويُعدّ كتاب "The TLA ⁺ Hyperbook" للمؤلف ليزلي لامبورت المرجع الحالي للغة TLA ^{+ .}

تاريخ

طُوِّر المنطق الزمني الحديث على يد آرثر بريور عام 1957، وكان يُطلق عليه آنذاك اسم منطق الزمن. مع أن أمير بنويلي كان أول من درس تطبيقات المنطق الزمني في علوم الحاسوب دراسةً جادة ، إلا أن بريور تكهّن باستخدامه قبل ذلك بعقد من الزمن، أي في عام 1967.

إن فائدة الأنظمة من هذا النوع [في الزمن المنفصل] لا تعتمد على أي افتراض ميتافيزيقي جاد بأن الزمن منفصل؛ فهي قابلة للتطبيق في مجالات محدودة من الخطاب التي نهتم فيها فقط بما يحدث بعد ذلك في سلسلة من الحالات المنفصلة، على سبيل المثال في عمل جهاز كمبيوتر رقمي.

قام بنويلي ببحث استخدام المنطق الزمني في تحديد برامج الحاسوب والاستدلال عليها، وقدم المنطق الزمني الخطي في عام 1977. وأصبح LTL أداة مهمة لتحليل البرامج المتزامنة، حيث يعبر بسهولة عن خصائص مثل الاستبعاد المتبادل والتحرر من حالة الجمود . ^{[ 8 ]}

بالتزامن مع عمل بنويلي على منطق LTL، كان الأكاديميون يعملون على تعميم منطق هوار للتحقق من صحة برامج المعالجة المتعددة. وقد أبدى ليزلي لامبورت اهتمامًا بهذه المشكلة بعد أن كشف تقييم الأقران عن خطأ في ورقة بحثية قدمها حول الاستبعاد المتبادل. قدّم إد آش كروفت مفهوم الثبات في ورقته البحثية عام 1975 بعنوان "إثبات صحة الادعاءات المتعلقة بالبرامج المتوازية"، والذي استخدمه لامبورت لتعميم طريقة فلويد في ورقته البحثية عام 1977 بعنوان "إثبات صحة برامج المعالجة المتعددة". كما قدّمت ورقة لامبورت مفهومي السلامة والحيوية كتعميمات للصحة الجزئية والإنهاء ، على التوالي. ^[⁹^] استُخدمت هذه الطريقة للتحقق من صحة أول خوارزمية لجمع البيانات المهملة المتزامنة في ورقة بحثية نُشرت عام 1978 بالاشتراك مع إدسكار ديكسترا . ^[¹⁰^]

تعرّف لامبورت لأول مرة على منطق الزمن الخطي (LTL) لبنويلي خلال ندوة عام 1978 في جامعة ستانفورد نظمتها سوزان أويكي . يقول لامبورت: "كنت متأكدًا من أن منطق الزمن مجرد هراء مجرد لن يكون له أي تطبيق عملي، لكنه بدا ممتعًا، لذا حضرت الندوة". في عام 1980، نشر بحثًا بعنوان "أحيانًا" يعني أحيانًا "ليس أبدًا"، والذي أصبح من أكثر الأبحاث استشهادًا في أدبيات منطق الزمن. ^{[ 11 ]} عمل لامبورت على كتابة مواصفات منطق الزمن خلال فترة عمله في معهد ستانفورد للأبحاث (SRI) ، لكنه وجد هذا النهج غير عملي.

لكنني شعرت بخيبة أمل تجاه المنطق الزمني عندما رأيت كيف أمضى شوارتز وميلار-سميث وفريتز فوغت أيامًا في محاولة تحديد طابور FIFO بسيط ، وهم يتجادلون حول ما إذا كانت الخصائص التي ذكروها كافية. أدركت أنه على الرغم من جاذبيته الجمالية، فإن كتابة المواصفات على شكل اقتران للخصائص الزمنية لا تجدي نفعًا في الواقع. ^{[ 12 ]}

أسفر بحثه عن طريقة عملية للتحديد عن ورقة بحثية نُشرت عام 1983 بعنوان "تحديد وحدات البرمجة المتزامنة"، والتي قدمت فكرة وصف انتقالات الحالة كدوال منطقية لمتغيرات مُؤَشَّرة وغير مُؤَشَّرة. ^{[ 12 ]} استمر العمل طوال ثمانينيات القرن العشرين، وبدأ لامبورت بنشر أوراق بحثية حول المنطق الزمني للأفعال عام 1990؛ ومع ذلك، لم يُقدَّم رسميًا إلا بعد نشر "المنطق الزمني للأفعال" عام 1994. مكّن المنطق الزمني للأفعال من استخدام الأفعال في الصيغ الزمنية، والتي، وفقًا للامبورت، "تُوفر طريقة أنيقة لإضفاء الطابع الرسمي والمنهجي على جميع الاستدلالات المستخدمة في التحقق من الأنظمة المتزامنة". ^{[ 13 ]}

تألفت مواصفات TLA في الغالب من رياضيات عادية غير زمنية، وهو ما وجده لامبورت أقل تعقيدًا من المواصفات الزمنية البحتة. وقد وفرت TLA أساسًا رياضيًا للغة المواصفات TLA ⁺ ، التي طُرحت في ورقة بحثية بعنوان "تحديد الأنظمة المتزامنة باستخدام TLA ⁺ " عام 1999. ^{[ 1 ]} وفي وقت لاحق من العام نفسه، كتب يوان يو مدقق نموذج TLC لمواصفات TLA ⁺ ؛ وقد استُخدم TLC لاكتشاف الأخطاء في بروتوكول تماسك ذاكرة التخزين المؤقت لمعالج كومباك متعدد. ^{[ 14 ]}

نشر لامبورت كتابًا دراسيًا شاملًا عن لغة TLA ⁺ عام 2002 بعنوان "تحديد مواصفات الأنظمة: لغة TLA ⁺ وأدواتها لمهندسي البرمجيات". ^{[ 15 ]} وطُرحت لغة PlusCal عام 2009، ^{[ 16 ]} ونظام إثبات TLA ⁺ (TLAPS) عام 2012. ^{[ 17 ]} وأُعلن عن TLA ⁺² عام 2014، مضيفًا بعض البنى اللغوية الإضافية، فضلًا عن زيادة كبيرة في دعم نظام الإثبات داخل اللغة. ^{[ 2 ]} ويعمل لامبورت حاليًا على إنشاء مرجع مُحدّث للغة TLA ⁺ بعنوان "كتاب TLA ^{+ الإلكتروني".}ويمكن الاطلاع على هذا العمل غير المكتمل على موقعه الإلكتروني الرسمي. كما يعمل لامبورت على إنشاء دورة فيديو TLA ⁺ ، والتي وُصفت بأنها "عمل قيد التطوير، يتضمن بداية سلسلة من محاضرات الفيديو لتعليم المبرمجين ومهندسي البرمجيات كيفية كتابة مواصفات TLA ⁺ الخاصة بهم ".

لغة

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

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

أمان

يهتم TLA ⁺ بتحديد مجموعة جميع سلوكيات النظام الصحيحة. على سبيل المثال، يمكن تحديد ساعة أحادية البت تدق بلا نهاية بين 0 و1 على النحو التالي:

ساعة متغيرة Init == clock \in {0, 1} Tick == إذا كانت قيمة clock تساوي 0، فإن قيمة clock' تساوي 1، وإلا فإن قيمة clock' تساوي 0. المواصفات == تهيئة /\ [][النبضة]_<<الساعة>>

تُعيّن علاقة الحالة التالية Tick قيمة clock ′ (قيمة clock في الحالة التالية) إلى 1 إذا كانت clock تساوي 0، وإلى 0 إذا كانت clock تساوي 1. وتكون حالة Init صحيحة إذا كانت قيمة clock إما 0 أو 1. أما Spec فهي صيغة زمنية تُؤكد أن جميع سلوكيات ساعة أحادية البت يجب أن تُحقق Init مبدئيًا ، وأن جميع خطواتها إما أن تُطابق Tick أو تكون خطوات متقطعة. ومن هذه السلوكيات:

0 -> 1 -> 0 -> 1 -> 0 -> ... 1 -> 0 -> 1 -> 0 -> 1 -> ...

تم وصف خصائص السلامة لساعة البت الواحد - مجموعة حالات النظام التي يمكن الوصول إليها - بشكل كافٍ بواسطة المواصفات.

حيوية

تمنع المواصفات المذكورة أعلاه الحالات الشاذة لساعة البت الواحد، لكنها لا تنص على أن الساعة ستعمل أبدًا. على سبيل المثال، تُقبل السلوكيات المتقطعة التالية:

0 -> 0 -> 0 -> 0 -> 0 -> ... 1 -> 1 -> 1 -> 1 -> 1 -> ...

الساعة التي لا تعمل غير مفيدة، لذا يجب منع هذه السلوكيات. أحد الحلول هو تعطيل التقطيع، لكن TLA ⁺ يتطلب تفعيل التقطيع دائمًا؛ تمثل خطوة التقطيع تغييرًا في جزء من النظام غير موصوف في المواصفات، وهي مفيدة للتحسين . لضمان عمل الساعة في النهاية، يتم تطبيق مبدأ العدالة الضعيفة على Tick .

Spec == Init /\ [][Tick]_<<clock>> /\ WF_<<clock>>(Tick)

يعني مبدأ العدالة الضعيفة على إجراء ما أنه إذا كان هذا الإجراء مُفعّلاً باستمرار، فلا بد من تنفيذه في نهاية المطاف. مع مبدأ العدالة الضعيفة على دورة التحديث (Tick) ، يُسمح بعدد محدود فقط من الخطوات المتقطعة بين دورات التحديث. يُطلق على هذا البيان المنطقي الزمني حول دورة التحديث اسم تأكيد الحيوية. بشكل عام، يجب أن يكون تأكيد الحيوية مغلقًا آليًا : أي أنه لا ينبغي أن يُقيّد مجموعة الحالات التي يمكن الوصول إليها، بل مجموعة السلوكيات الممكنة فقط. ^{[ 18 ]}

لا تتطلب معظم المواصفات تأكيد خصائص الحيوية. تكفي خصائص السلامة للتحقق من النموذج وللتوجيه في تنفيذ النظام. ^{[ 19 ]}

المشغلون

تعتمد لغة TLA ^{+ على}ZF ، لذا فإن العمليات على المتغيرات تتضمن معالجة المجموعات. تتضمن اللغة عوامل عضوية المجموعة ، والاتحاد ، والتقاطع ، والفرق ، ومجموعة القوى ، والمجموعات الجزئية . كما تتضمن عوامل منطق الرتبة الأولى مثل $\lor$ ، $\land$ ، $\neg$ ، $\Rightarrow$ ، $\leftrightarrow$ ، $\equiv$ ، بالإضافة إلى المُكمِّمات الكلية والوجودية $\forall$ و∃ . يُقدَّم مُعامل هيلبرت $ε$ كعامل 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 ⁺² .

هياكل البيانات

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

تُسند الدوال في TLA ⁺ قيمةً لكل عنصر في نطاقها، وهو مجموعة. [S -> T]هي مجموعة جميع الدوال التي تحقق f[ x ] في T ، لكل x في مجموعة النطاق S. على سبيل المثال، الدالة ^fDouble[x \in Nat] == x*2 [x] في T هي عنصر من مجموعة النطاق S [Nat -> Nat]، لذا Double \in [Nat -> Nat]فهي عبارة صحيحة في TLA ⁺ . تُعرَّف الدوال أيضًا باستخدام [x \in S |-> e]تعبير ما e ، أو بتعديل دالة موجودة .[f EXCEPT ![v₁] = v₂]

تُعد السجلات نوعًا من أنواع الدوال في TLA ⁺ . السجل [name |-> "John", age |-> 35]هو سجل يحتوي على حقلين هما الاسم والعمر، ويتم الوصول إليهما باستخدام r.nameو r.age، وينتمي إلى مجموعة السجلات .[name : String, age : Nat]

تُضمَّن المجموعات المرتبة في TLA ⁺ . ويتم تعريفها صراحةً أو إنشاؤها باستخدام عوامل من وحدة التسلسلات القياسية. تُعرَّف مجموعات المجموعات المرتبة بواسطة الضرب الديكارتي ؛ على سبيل المثال، تُعرَّف مجموعة جميع أزواج الأعداد الطبيعية على النحو التالي .<<e₁,e₂,e₃>>Nat \X Nat

الوحدات النمطية القياسية

يحتوي TLA ⁺ على مجموعة من الوحدات النمطية القياسية التي تتضمن عوامل تشغيل شائعة. يتم توزيعها مع محلل التركيب النحوي. يستخدم مدقق نموذج TLC تطبيقات جافا لتحسين الأداء.

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

يتم استيراد الوحدات النمطية القياسية باستخدام عبارات " EXTENDSأو" INSTANCE.

أدوات

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

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

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

يتم توزيع بيئة التطوير المتكاملة (IDE) في مجموعة أدوات TLA .

مدقق النماذج

يقوم مدقق نموذج TLC ببناء نموذج حالة محدود لـ TLA ^{بالإضافة} إلى مواصفات للتحقق من خصائص الثبات . يُنشئ TLC مجموعة من الحالات الأولية التي تُحقق المواصفات، ثم يُجري بحثًا بالعرض أولًا على جميع انتقالات الحالة المُحددة. يتوقف التنفيذ عندما تؤدي جميع انتقالات الحالة إلى حالات تم اكتشافها مُسبقًا. إذا اكتشف TLC حالة تُخالف أحد ثوابت النظام، فإنه يتوقف ويُقدم مسار تتبع الحالة إلى الحالة المُخالفة. يُوفر TLC طريقة لإعلان تناظرات النموذج للحماية من الانفجار التوافقي . ^{[ 14 ]} كما أنه يُوازي خطوة استكشاف الحالة، ويمكن تشغيله في وضع مُوزع لتوزيع عبء العمل على عدد كبير من أجهزة الكمبيوتر. ^{[ 20 ]}

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

نظام إثبات

نظام إثبات TLA ^{+ ، أو TLAPS،}يتحقق آليًا من البراهين المكتوبة بلغة TLA ⁺ . طُوّر هذا النظام في المركز المشترك بين مايكروسوفت للأبحاث و INRIA لإثبات صحة الخوارزميات المتزامنة والموزعة. صُممت لغة البرهان لتكون مستقلة عن أي مُثبت نظريات مُحدد؛ حيث تُكتب البراهين بأسلوب تصريحي، وتُحوّل إلى التزامات فردية تُرسل إلى مُثبتات الواجهة الخلفية. مُثبتات الواجهة الخلفية الرئيسية هي Isabelle وZenon، مع إمكانية الرجوع إلى مُحللات SMT مثل CVC3 و Yices و Z3 . تتميز براهين TLAPS ببنية هرمية، مما يُسهّل إعادة هيكلة الكود ويُمكّن من التطوير غير الخطي: إذ يُمكن البدء بالعمل على الخطوات اللاحقة قبل التحقق من جميع الخطوات السابقة، كما تُقسّم الخطوات الصعبة إلى خطوات فرعية أصغر. يتوافق TLAPS بشكل جيد مع TLC، حيث يكتشف مُدقق النموذج الأخطاء الصغيرة بسرعة قبل بدء عملية التحقق. وبالتالي، يُمكن لـ TLAPS إثبات خصائص النظام التي تتجاوز قدرات التحقق من النموذج المحدود. ^{[ 17 ]}

لا يدعم TLAPS حاليًا الاستدلال بالأعداد الحقيقية، ولا معظم عوامل الزمن. ولا تستطيع إيزابيل وزينون عمومًا إثبات التزامات البرهان الحسابي، مما يستلزم استخدام حلول SMT. ^{[ 21 ]} وقد استُخدم TLAPS لإثبات صحة بروتوكول باكسوس البيزنطي ، وبنية أمان ميموار، ومكونات جدول التجزئة الموزع باستري ، ^{[ 17 ]} وخوارزمية توافق الآراء سباير. ^{[ 22 ]} وهو يُوزع بشكل منفصل عن بقية أدوات TLA ⁺ ، وهو برنامج مجاني، يُوزع بموجب ترخيص BSD . ^{[ 23 ]} وقد وسّع TLA ⁺² بشكل كبير دعم اللغة لبنى البرهان.

الاستخدام الصناعي

في شركة مايكروسوفت ، تم اكتشاف خلل حرج في وحدة ذاكرة جهاز إكس بوكس 360 أثناء عملية كتابة مواصفات بلغة TLA ⁺ . ^{[ 24 ]} وقد استُخدمت لغة TLA ⁺ لكتابة براهين رسمية لصحة بروتوكول باكسوس البيزنطي ومكونات جدول التجزئة الموزع باستري . ^{[ 17 ]}

تستخدم خدمات أمازون السحابية (AWS) بروتوكول TLA ⁺ منذ عام 2011. وقد كشف فحص نماذج TLA ⁺ عن أخطاء في DynamoDB و S3 و EBS ، بالإضافة إلى مدير أقفال داخلي موزّع؛ تطلّب اكتشاف بعض هذه الأخطاء تتبّع حالة النظام لـ 35 خطوة. كما استُخدم فحص النماذج للتحقق من التحسينات المُكثّفة. علاوة على ذلك، وُجد أن مواصفات TLA ^{+ قيّمة كوثائق وأدوات مساعدة في التصميم.}^{[ 4 ]}^{[ 25 ]}

استخدمت مايكروسوفت أزور TLA ⁺ لتصميم Cosmos DB ، وهي قاعدة بيانات موزعة عالميًا بخمسة نماذج اتساق مختلفة . ^{[ 26 ]}^{[ 27 ]}

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

أمثلة

مخزن القيم الرئيسية مع عزل اللقطات :

--------------------------- وحدة تخزين القيم الرئيسية --------------------------- الثوابت المفتاح، * مجموعة جميع المفاتيح. Val, \* مجموعة جميع القيم. TxId * مجموعة جميع معرفات المعاملات. مخزن المتغيرات، * مخزن بيانات يربط المفاتيح بالقيم. tx، * مجموعة معاملات اللقطة المفتوحة. snapshotStore، * لقطات من المتجر لكل معاملة. مكتوب، * سجل عمليات الكتابة التي تم تنفيذها داخل كل معاملة. مفقودة * مجموعة عمليات الكتابة غير المرئية لكل معاملة. ---------------------------------------------------------------------------- NoVal == \* اختر شيئًا لتمثيل غياب القيمة. اختر v : v \notin Val Store == \* مجموعة جميع مخازن القيم الرئيسية. [المفتاح -> القيمة \cup {لا قيمة}] Init == \* المسند الأولي. /\ store = [k \in Key |-> NoVal] \* جميع قيم المتجر تكون في البداية NoVal. /\ tx = {} \* مجموعة المعاملات المفتوحة تكون فارغة في البداية. /\ snapshotStore = \* جميع قيم snapshotStore تكون مبدئيًا NoVal. [t \in TxId |-> [k \in Key |-> NoVal]] /\ written = [t \in TxId |-> {}] \* جميع سجلات الكتابة فارغة في البداية. /\ missing = [t \in TxId |-> {}] \* جميع عمليات الكتابة الفائتة تكون فارغة في البداية. TypeInvariant == \* النوع الثابت. /\ store \in Store /\ tx \subseteq TxId /\ snapshotStore \in [TxId -> Store] /\ مكتوب \in [TxId -> SUBSET Key] /\ مفقود \in [TxId -> SUBSET Key] دورة حياة المعاملة == /\ \A t \in tx : \* إذا كان store != snapshot ولم نقم بالكتابة إليه، فلا بد أننا أغفلنا عملية كتابة. \A k \in Key : (store[k] /= snapshotStore[t][k] /\ k \notin written[t]) => k \in missing[t] /\ \A t \in TxId \ tx : \* يتم تنظيف المعاملات بعد التخلص منها. /\ \A k \in Key : snapshotStore[t][k] = NoVal /\ written[t] = {} /\ missing[t] = {} OpenTx(t) == \* فتح معاملة جديدة. /\ t \notin tx tx' = tx \cup {t} /\ snapshotStore' = [snapshotStore EXCEPT ![t] = store] /\ غير مُغيّر <<مكتوب، مفقود، مخزن>> Add(t, k, v) == \* باستخدام المعاملة t، أضف القيمة v إلى المخزن تحت المفتاح k. /\ t \in tx snapshotStore[t][k] = NoVal /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v] /\ مكتوب' = [مكتوب باستثناء ![t] = @ \cup {k}] /\ غير مُغيّر <<tx, missing, store>> Update(t, k, v) == \* باستخدام المعاملة t، قم بتحديث القيمة المرتبطة بالمفتاح k إلى v. /\ t \in tx /\ snapshotStore[t][k] \notin {NoVal, v} /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v] /\ مكتوب' = [مكتوب باستثناء ![t] = @ \cup {k}] /\ غير مُغيّر <<tx, missing, store>> Remove(t, k) == \* باستخدام المعاملة t، قم بإزالة المفتاح k من المخزن. /\ t \in tx /\ snapshotStore[t][k] /= NoVal /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = NoVal] /\ مكتوب' = [مكتوب باستثناء ![t] = @ \cup {k}] /\ غير مُغيّر <<tx, missing, store>> RollbackTx(t) == \* إغلاق المعاملة دون دمج عمليات الكتابة في المخزن. /\ t \in tx tx' = tx \ {t} /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]] /\ مكتوب' = [مكتوب باستثناء ![t] = {}] /\ missing' = [missed EXCEPT ![t] = {}] متجر غير مُغيّر CloseTx(t) == \* إغلاق المعاملة t، ودمج عمليات الكتابة في المخزن. /\ t \in tx /\ missing[t] \cap written[t] = {} \* اكتشاف تعارضات الكتابة. /\ store' = \* دمج عمليات الكتابة في snapshotStore في المتجر. [k \in Key |-> IF k \in written[t] THEN snapshotStore[t][k] ELSE store[k]] tx' = tx \ {t} /\ missing' = \* تحديث عمليات الكتابة الفائتة للمعاملات المفتوحة الأخرى. [otherTx \in TxId |-> IF otherTx \in tx' THEN missing[otherTx] \cup written[t] ELSE {}] /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]] /\ مكتوب' = [مكتوب باستثناء ![t] = {}] التالي == * علاقة الحالة التالية. \/ \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 == \* تهيئة الحالة باستخدام Init والانتقال باستخدام Next. تهيئة /\ [][التالي]_<<تخزين، معاملة، تخزين اللقطات، مكتوب، مفقود>> ---------------------------------------------------------------------------- نظرية Spec => [](TypeInvariant /\ TxLifecycle) =============================================================================

انظر أيضاً

مراجع

1 2 لامبورت، ليزلي (يناير 2000). تحديد الأنظمة المتزامنة باستخدام TLA ⁺ (ملف PDF) . سلسلة علوم الناتو، الجزء الثالث: علوم الحاسوب والأنظمة. المجلد 173. أمستردام: دار نشر IOS. الصفحات 183-247 . ISBN 978-90-5199-459-9تم الاطلاع عليه بتاريخ 22 مايو 2015 .
1 2 لامبورت، ليزلي (15 يناير 2014). "TLA ⁺² : دليل تمهيدي" (ملف PDF) . تم الاطلاع عليه في 2 مايو 2015 .
↑ "أدوات تلابلس - الترخيص" . كود بليكس . مايكروسوفت ، كومباك . 8 أبريل 2013. تم الاطلاع عليه في 10 مايو 2015 .https://tlaplus.codeplex.com/license
1 2 نيوكومب، كريس؛ راث، تيم؛ تشانغ، فان؛ مونتيانو، بوغدان؛ بروكر، مارك؛ ديردوف، مايكل (29 سبتمبر 2014). "استخدام الأساليب الرسمية في خدمات أمازون السحابية" (ملف PDF) . أمازون . تم الاطلاع عليه بتاريخ 8 مايو 2015 .
↑ لامبورت، ليزلي (25 يناير 2013). "لماذا يجب أن نبني البرمجيات كما نبني المنازل؟" . وايرد . تم الاطلاع عليه في 7 مايو 2015 .
↑ لامبورت، ليزلي (18 يونيو 2002). "7.1 لماذا التحديد؟" . تحديد الأنظمة: لغة وأدوات TLA ⁺ لمهندسي الأجهزة والبرمجيات . أديسون-ويسلي . ص 75. ISBN 978-0-321-14306-8إن الاضطرار إلى وصف التصميم بدقة غالباً ما يكشف عن مشاكل - تفاعلات دقيقة و"حالات خاصة" يسهل التغاضي عنها.
↑ لامبورت، ليزلي (2012). "كيفية كتابة برهان القرن الحادي والعشرين" (ملف PDF) . مجلة نظرية النقطة الثابتة وتطبيقاتها . 11 : 43-63 . doi : 10.1007/s11784-012-0071-6 . ISSN 1661-7738 . S2CID 121557270. تاريخ الاسترجاع: 23 مايو 2015 .
↑ أورستروم، بيتر؛ هاسل، بير (1995). "3.7 المنطق الزمني وعلوم الحاسوب". المنطق الزمني: من الأفكار القديمة إلى الذكاء الاصطناعي . دراسات في اللغويات والفلسفة. المجلد 57. سبرينغر هولندا . الصفحات 344-365 . doi : 10.1007/978-0-585-37463-5 . ISBN 978-0-7923-3586-3.
↑ لامبورت، ليزلي . "كتابات ليزلي لامبورت: إثبات صحة برامج المعالجة المتعددة" . تم الاطلاع عليه بتاريخ 22 مايو 2015 .
↑ لامبورت، ليزلي . "كتابات ليزلي لامبورت: جمع القمامة على الفور: تمرين في التعاون" . تم الاسترجاع في 22 مايو 2015 .
↑ لامبورت، ليزلي . "كتابات ليزلي لامبورت: 'أحيانًا' تعني أحيانًا 'ليس أبدًا'"تم الاطلاع عليه بتاريخ 22 مايو 2015 .
1 2 لامبورت، ليزلي . "كتابات ليزلي لامبورت: تحديد وحدات البرمجة المتزامنة" . تم الاسترجاع في 22 مايو 2015 .
↑ لامبورت، ليزلي . "كتابات ليزلي لامبورت: المنطق الزمني للأفعال" . تم الاطلاع عليه بتاريخ 22 مايو 2015 .
1 2 يو، يوان؛ مانوليوس، بانايوتيس؛ لامبورت، ليزلي (1999). "التحقق من نموذج TLA ⁺ المواصفات". تصميم الأجهزة الصحيح وطرق التحقق (PDF) . سلسلة محاضرات في علوم الحاسوب. المجلد 1703. سبرينغر-فيرلاغ . الصفحات 54-66 . doi : 10.1007/3-540-48153-2_6 . ISBN 978-3-540-66559-5تم الاطلاع عليه بتاريخ 14 مايو 2015 .
↑ لامبورت، ليزلي (18 يونيو 2002). تحديد مواصفات الأنظمة: لغة وأدوات TLA ⁺ لمهندسي الأجهزة والبرمجيات . أديسون-ويسلي . ISBN 978-0-321-14306-8.
↑ لامبورت، ليزلي (2 يناير 2009). "لغة خوارزمية بلس كال" (ملف PDF) . الجوانب النظرية للحوسبة - المؤتمر الدولي لتكنولوجيا المعلومات والاتصالات 2009. سلسلة محاضرات في علوم الحاسوب. المجلد 5684. سبرينغر برلين هايدلبرغ . الصفحات 36-60 . doi : 10.1007/978-3-642-03466-4_2 . ISBN 978-3-642-03465-7تم الاطلاع عليه بتاريخ 10 مايو 2015 .
1 2 3 4 كوزينو، دينيس؛ دوليجيز، داميان؛ الأماكن القريبة : ميرز، ستيفان. ريكيتس، دانيال. ^ فانزيتو ، هيرنان (1 يناير 2012). "TLA ⁺ البراهين". FM 2012: الأساليب الرسمية (PDF) . ملاحظات محاضرة في علوم الكمبيوتر. المجلد. 7436. سبرينغر برلين هايدلبرغ . ص 147 – 154. دوى : 10.1007 / 978-3-642-32759-9_14 . رقم ISBN 978-3-642-32758-2S2CID 5243433. تم الاطلاع عليه بتاريخ 14 مايو 2015 .
↑ لامبورت، ليزلي (18 يونيو 2002). "8.9.2 إغلاق الآلة" . تحديد الأنظمة: لغة وأدوات TLA ⁺ لمهندسي الأجهزة والبرمجيات . أديسون-ويسلي . ص 112. ISBN 978-0-321-14306-8نادراً ما نرغب في كتابة مواصفات غير مغلقة آلياً. وإذا كتبنا واحدة، فغالباً ما يكون ذلك عن طريق الخطأ.
↑ لامبورت، ليزلي (18 يونيو 2002). "8.9.6 المنطق الزمني يُعتبر مُربكًا" . تحديد الأنظمة: لغة وأدوات TLA ⁺ لمهندسي الأجهزة والبرمجيات . أديسون-ويسلي . ص 116. ISBN 978-0-321-14306-8في الواقع ، يمكن لمعظم المهندسين التعامل بشكل جيد مع المواصفات من الشكل (8.38) التي تعبر فقط عن خصائص السلامة ولا تخفي أي متغيرات.
↑ ماركوس أ. كوب (3 يونيو 2014). تسجيل محاضرة تقنية موزعة^{. فعالية TLA +} Community Event 2014، تولوز، فرنسا.{{cite AV media}}: CS1 maint: location ( link )
↑ "ميزات TLAPS غير المدعومة" . نظام TLA ⁺ Proof . مركز مايكروسوفت للأبحاث - المركز المشترك INRIA . تم الاطلاع عليه بتاريخ 14 مايو 2015 .
↑ كوتانوف، إميل ( 12 يوليو 2021). "سباير: حل تعاوني متناظر الطور للتوافق الموزع" . IEEE Access . 9. IEEE : 101702–101717 . Bibcode : 2021IEEEA...9j1702K . doi : 10.1109/ACCESS.2021.3096326 . S2CID 236480167 .
↑ نظام إثبات TLA ⁺
↑ ليزلي لامبورت (3 أبريل 2014). التفكير للمبرمجين (عند الدقيقة 21 و46 ثانية) (تسجيل لمحاضرة تقنية). سان فرانسيسكو: مايكروسوفت . تم الاطلاع عليه بتاريخ 14 مايو 2015 .
↑ كريس، نيوكومب (2014). "لماذا اختارت أمازون TLA ^+؟ ". آلات الحالة المجردة، Alloy، B، TLA، VDM، وZ. سلسلة محاضرات في علوم الحاسوب. المجلد 8477. سبرينغر برلين هايدلبرغ . الصفحات 25-39 . doi : 10.1007/978-3-662-43652-3_3 . ISBN 978-3-662-43651-6.
↑ لاردينوا، فريدريك (10 مايو 2017). "مع Cosmos DB، تريد مايكروسوفت بناء قاعدة بيانات واحدة شاملة" . TechCrunch . تم الاطلاع عليه بتاريخ 10 مايو 2017 .
↑ ليزلي لامبورت (10 مايو 2017). أساسيات Azure Cosmos DB مع الدكتور ليزلي لامبورت (تسجيل مقابلة). مايكروسوفت أزور . تم الاطلاع عليه بتاريخ 10 مايو 2017 .

[tlaplus-original-1] 1 2 لامبورت، ليزلي (يناير 2000). تحديد الأنظمة المتزامنة باستخدام TLA ⁺ (ملف PDF) . سلسلة علوم الناتو، الجزء الثالث: علوم الحاسوب والأنظمة. المجلد 173. أمستردام: دار نشر IOS. الصفحات 183-247 . ISBN 978-90-5199-459-9تم الاطلاع عليه بتاريخ 22 مايو 2015 .

[tla2guide-2] 1 2 لامبورت، ليزلي (15 يناير 2014). "TLA ⁺² : دليل تمهيدي" (ملف PDF) . تم الاطلاع عليه في 2 مايو 2015 .

[toolboxlicense-3] "أدوات تلابلس - الترخيص" . كود بليكس . مايكروسوفت ، كومباك . 8 أبريل 2013. تم الاطلاع عليه في 10 مايو 2015 .https://tlaplus.codeplex.com/license

[awsorig-4] 1 2 نيوكومب، كريس؛ راث، تيم؛ تشانغ، فان؛ مونتيانو، بوغدان؛ بروكر، مارك؛ ديردوف، مايكل (29 سبتمبر 2014). "استخدام الأساليب الرسمية في خدمات أمازون السحابية" (ملف PDF) . أمازون . تم الاطلاع عليه بتاريخ 8 مايو 2015 .

[wired-5] لامبورت، ليزلي (25 يناير 2013). "لماذا يجب أن نبني البرمجيات كما نبني المنازل؟" . وايرد . تم الاطلاع عليه في 7 مايو 2015 .

[precise-spec-6] لامبورت، ليزلي (18 يونيو 2002). "7.1 لماذا التحديد؟" . تحديد الأنظمة: لغة وأدوات TLA ⁺ لمهندسي الأجهزة والبرمجيات . أديسون-ويسلي . ص 75. ISBN 978-0-321-14306-8إن الاضطرار إلى وصف التصميم بدقة غالباً ما يكشف عن مشاكل - تفاعلات دقيقة و"حالات خاصة" يسهل التغاضي عنها.

[lamport-proofs-7] لامبورت، ليزلي (2012). "كيفية كتابة برهان القرن الحادي والعشرين" (ملف PDF) . مجلة نظرية النقطة الثابتة وتطبيقاتها . 11 : 43-63 . doi : 10.1007/s11784-012-0071-6 . ISSN 1661-7738 . S2CID 121557270. تاريخ الاسترجاع: 23 مايو 2015 .

[temporal-logic-history-8] أورستروم، بيتر؛ هاسل، بير (1995). "3.7 المنطق الزمني وعلوم الحاسوب". المنطق الزمني: من الأفكار القديمة إلى الذكاء الاصطناعي . دراسات في اللغويات والفلسفة. المجلد 57. سبرينغر هولندا . الصفحات 344-365 . doi : 10.1007/978-0-585-37463-5 . ISBN 978-0-7923-3586-3.

[lamport-proving-9] لامبورت، ليزلي . "كتابات ليزلي لامبورت: إثبات صحة برامج المعالجة المتعددة" . تم الاطلاع عليه بتاريخ 22 مايو 2015 .

[lamport-garbage-10] لامبورت، ليزلي . "كتابات ليزلي لامبورت: جمع القمامة على الفور: تمرين في التعاون" . تم الاسترجاع في 22 مايو 2015 .

[lamport-sometime-11] لامبورت، ليزلي . "كتابات ليزلي لامبورت: 'أحيانًا' تعني أحيانًا 'ليس أبدًا'"تم الاطلاع عليه بتاريخ 22 مايو 2015 .

[lamport-spec-12] 1 2 لامبورت، ليزلي . "كتابات ليزلي لامبورت: تحديد وحدات البرمجة المتزامنة" . تم الاسترجاع في 22 مايو 2015 .

[lamport-actions-13] لامبورت، ليزلي . "كتابات ليزلي لامبورت: المنطق الزمني للأفعال" . تم الاطلاع عليه بتاريخ 22 مايو 2015 .

[tlcoriginal-14] 1 2 يو، يوان؛ مانوليوس، بانايوتيس؛ لامبورت، ليزلي (1999). "التحقق من نموذج TLA ⁺ المواصفات". تصميم الأجهزة الصحيح وطرق التحقق (PDF) . سلسلة محاضرات في علوم الحاسوب. المجلد 1703. سبرينغر-فيرلاغ . الصفحات 54-66 . doi : 10.1007/3-540-48153-2_6 . ISBN 978-3-540-66559-5تم الاطلاع عليه بتاريخ 14 مايو 2015 .

[specsystems-15] لامبورت، ليزلي (18 يونيو 2002). تحديد مواصفات الأنظمة: لغة وأدوات TLA ⁺ لمهندسي الأجهزة والبرمجيات . أديسون-ويسلي . ISBN 978-0-321-14306-8.

[pluscal-original-16] لامبورت، ليزلي (2 يناير 2009). "لغة خوارزمية بلس كال" (ملف PDF) . الجوانب النظرية للحوسبة - المؤتمر الدولي لتكنولوجيا المعلومات والاتصالات 2009. سلسلة محاضرات في علوم الحاسوب. المجلد 5684. سبرينغر برلين هايدلبرغ . الصفحات 36-60 . doi : 10.1007/978-3-642-03466-4_2 . ISBN 978-3-642-03465-7تم الاطلاع عليه بتاريخ 10 مايو 2015 .

[tlaps-survey-17] 1 2 3 4 كوزينو، دينيس؛ دوليجيز، داميان؛ الأماكن القريبة : ميرز، ستيفان. ريكيتس، دانيال. ^ فانزيتو ، هيرنان (1 يناير 2012). "TLA ⁺ البراهين". FM 2012: الأساليب الرسمية (PDF) . ملاحظات محاضرة في علوم الكمبيوتر. المجلد. 7436. سبرينغر برلين هايدلبرغ . ص 147 – 154. دوى : 10.1007 / 978-3-642-32759-9_14 . رقم ISBN 978-3-642-32758-2S2CID 5243433. تم الاطلاع عليه بتاريخ 14 مايو 2015 .

[machine-closure-18] لامبورت، ليزلي (18 يونيو 2002). "8.9.2 إغلاق الآلة" . تحديد الأنظمة: لغة وأدوات TLA ⁺ لمهندسي الأجهزة والبرمجيات . أديسون-ويسلي . ص 112. ISBN 978-0-321-14306-8نادراً ما نرغب في كتابة مواصفات غير مغلقة آلياً. وإذا كتبنا واحدة، فغالباً ما يكون ذلك عن طريق الخطأ.

[temporal-logic-confusing-19] لامبورت، ليزلي (18 يونيو 2002). "8.9.6 المنطق الزمني يُعتبر مُربكًا" . تحديد الأنظمة: لغة وأدوات TLA ⁺ لمهندسي الأجهزة والبرمجيات . أديسون-ويسلي . ص 116. ISBN 978-0-321-14306-8في الواقع ، يمكن لمعظم المهندسين التعامل بشكل جيد مع المواصفات من الشكل (8.38) التي تعبر فقط عن خصائص السلامة ولا تخفي أي متغيرات.

[tlcdistributed-20] ماركوس أ. كوب (3 يونيو 2014). تسجيل محاضرة تقنية موزعة^{. فعالية TLA +} Community Event 2014، تولوز، فرنسا.{{cite AV media}}: CS1 maint: location ( link )

[tlaps-unsupported-21] "ميزات TLAPS غير المدعومة" . نظام TLA ⁺ Proof . مركز مايكروسوفت للأبحاث - المركز المشترك INRIA . تم الاطلاع عليه بتاريخ 14 مايو 2015 .

[spire-22] كوتانوف، إميل ( 12 يوليو 2021). "سباير: حل تعاوني متناظر الطور للتوافق الموزع" . IEEE Access . 9. IEEE : 101702–101717 . Bibcode : 2021IEEEA...9j1702K . doi : 10.1109/ACCESS.2021.3096326 . S2CID 236480167 .

[23] نظام إثبات TLA ⁺

[lamportbuild-24] ليزلي لامبورت (3 أبريل 2014). التفكير للمبرمجين (عند الدقيقة 21 و46 ثانية) (تسجيل لمحاضرة تقنية). سان فرانسيسكو: مايكروسوفت . تم الاطلاع عليه بتاريخ 14 مايو 2015 .

[awschose-25] كريس، نيوكومب (2014). "لماذا اختارت أمازون TLA ^+؟ ". آلات الحالة المجردة، Alloy، B، TLA، VDM، وZ. سلسلة محاضرات في علوم الحاسوب. المجلد 8477. سبرينغر برلين هايدلبرغ . الصفحات 25-39 . doi : 10.1007/978-3-662-43652-3_3 . ISBN 978-3-662-43651-6.

[cosmos-26] لاردينوا، فريدريك (10 مايو 2017). "مع Cosmos DB، تريد مايكروسوفت بناء قاعدة بيانات واحدة شاملة" . TechCrunch . تم الاطلاع عليه بتاريخ 10 مايو 2017 .

[lamportcosmos-27] ليزلي لامبورت (10 مايو 2017). أساسيات Azure Cosmos DB مع الدكتور ليزلي لامبورت (تسجيل مقابلة). مايكروسوفت أزور . تم الاطلاع عليه بتاريخ 10 مايو 2017 .

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[

[

[ 11 ]

[ 12 ]

[ 13 ]

[ 1 ]

[ 14 ]

[ 15 ]

[ 16 ]

[ 17 ]

[ 2 ]

[ 18 ]

[ 19 ]

[ 20 ]

[ 21 ]

[ 22 ]

[ 23 ]

[ 24 ]

[ 25 ]

[ 26 ]

[ 27 ]