بناء وتحليل العمليات الموزعة

📅 آخر تحديث: ٢٦ يوليو ٢٠٢٦
✍️ نُشر في: ٢٦ يوليو ٢٠٢٦
الموسوعة الحرة

CADP [ 1 ] ( بناء وتحليل العمليات الموزعة ) هي مجموعة أدوات لتصميم بروتوكولات الاتصال والأنظمة الموزعة. طُوّرت CADP بواسطة فريق CONVECS (الذي كان سابقًا من فريق VASY) في INRIA Rhone-Alpes، وهي مرتبطة بالعديد من الأدوات التكميلية. تخضع CADP للصيانة والتحسين المستمر، وتُستخدم في العديد من المشاريع الصناعية.

الغرض من مجموعة أدوات CADP هو تسهيل تصميم الأنظمة الموثوقة باستخدام تقنيات الوصف الرسمي جنبًا إلى جنب مع أدوات البرمجيات للمحاكاة والتطوير السريع للتطبيقات والتحقق وتوليد الاختبارات.

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

يتضمن برنامج CADP أدوات لدعم استخدام نهجين في الأساليب الرسمية، وكلاهما ضروري لتصميم أنظمة موثوقة :

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

تاريخ

بدأ العمل على CADP في عام 1986، عندما تم تطوير أول أداتين، وهما CAESAR وALDEBARAN. وفي عام 1989، تم ابتكار اختصار CADP، والذي يرمز إلى CAESAR/ALDEBARAN Distribution Package (حزمة توزيع CAESAR/ALDEBARAN ). ومع مرور الوقت، أُضيفت العديد من الأدوات، بما في ذلك واجهات برمجة التطبيقات التي أتاحت المساهمة في تطوير الأدوات، ليصبح اختصار CADP حينها CAESAR/ALDEBARAN Development Package (حزمة تطوير CAESAR/ALDEBARAN) . يحتوي CADP حاليًا على أكثر من 50 أداة. وبينما احتفظ الاختصار نفسه، تم تغيير اسم مجموعة الأدوات ليعكس غرضها بشكل أفضل: بناء وتحليل العمليات الموزعة .

إصدارات رئيسية

تمت تسمية إصدارات CADP تباعاً بالأحرف الأبجدية (من "A" إلى "Z")، ثم بأسماء المدن التي تستضيف مجموعات البحث الأكاديمية التي تعمل بنشاط على لغة LOTOS ، وبشكل عام، بأسماء المدن التي قدمت مساهمات كبيرة في نظرية التزامن .

الاسم الرمزيتاريخ
"أ" ... "ي"يناير 1990 – ديسمبر 1996
توينتييونيو 1997
لييجيناير 1999
أوتاوايوليو 2001
إدنبرةديسمبر 2006
زيورخديسمبر 2013
أمستردامديسمبر 2014
ستوني بروكديسمبر 2015
أكسفوردديسمبر 2016
صوفيا أنتيبوليسديسمبر 2017
أوبسالاديسمبر 2018
بيزاديسمبر 2019
آلبورغديسمبر 2020
ساربروكينديسمبر 2021
كيستاديسمبر 2022
آخنديسمبر 2023
أيندهوفنديسمبر 2024

بين الإصدارات الرئيسية، تتوفر عادةً إصدارات فرعية تتيح الوصول المبكر إلى الميزات والتحسينات الجديدة. لمزيد من المعلومات، راجع صفحة قائمة التغييرات على موقع CADP الإلكتروني.

ميزات CADP

يوفر برنامج CADP مجموعة واسعة من الوظائف، تتراوح من المحاكاة خطوة بخطوة إلى التحقق من النماذج المتوازية على نطاق واسع . ويتضمن ما يلي:

  • برامج تجميع لعدة أشكال إدخال:
    • [ 2 ] تحتوي مجموعة الأدوات على وصف بروتوكول عالي المستوى مكتوب بلغة ISO LOTOS . [2] تحتوي مجموعة الأدوات على مترجمين (CAESAR و CAESAR.ADT) يقومان بترجمة أوصاف LOTOS إلى كود C لاستخدامه في أغراض المحاكاة والتحقق والاختبار.
    • وصف البروتوكولات منخفضة المستوى المحددة كآلات حالة محدودة.
    • شبكات من الآلات المتصلة، أي آلات الحالة المحدودة التي تعمل بالتوازي والمتزامنة (إما باستخدام عوامل تشغيل جبر العمليات أو متجهات التزامن).
  • العديد من أدوات التحقق من التكافؤ (التقليل والمقارنات modulo علاقات المحاكاة الثنائية)، مثل BCG_MIN و BISIMULATOR.
  • العديد من أدوات التحقق من النماذج لمختلف أنواع المنطق الزمني وحساب التفاضل والتكامل، مثل EVALUATOR و XTL.
  • تم دمج العديد من خوارزميات التحقق: التحقق التعدادي، والتحقق الفوري، والتحقق الرمزي باستخدام مخططات القرار الثنائية، والتقليل التركيبي، والترتيبات الجزئية، والتحقق من النموذج الموزع، وما إلى ذلك.
  • بالإضافة إلى أدوات أخرى ذات وظائف متقدمة مثل الفحص المرئي وتقييم الأداء وما إلى ذلك.

تم تصميم CADP بطريقة معيارية ويركز على التنسيقات الوسيطة وواجهات البرمجة (مثل بيئات برامج BCG و OPEN/CAESAR)، مما يسمح بدمج أدوات CADP مع أدوات أخرى وتكييفها مع لغات المواصفات المختلفة.

النماذج وتقنيات التحقق

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

تعتمد معظم خوارزميات التحقق في CADP على نموذج أنظمة الانتقال المصنفة (أو ببساطة، الأوتوماتا أو الرسوم البيانية)، والذي يتكون من مجموعة من الحالات، وحالة ابتدائية، وعلاقة انتقال بين الحالات. غالبًا ما يُولّد هذا النموذج تلقائيًا من أوصاف عالية المستوى للنظام قيد الدراسة، ثم يُقارن بخصائص النظام باستخدام إجراءات اتخاذ قرار متنوعة. اعتمادًا على الصيغة المستخدمة للتعبير عن الخصائص، يُمكن اتباع نهجين:

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

على الرغم من كفاءة هذه التقنيات وأتمتتها، إلا أن عيبها الرئيسي يكمن في مشكلة تضخم البيانات، والتي تحدث عندما تكون النماذج كبيرة جدًا بحيث لا تتسع لها ذاكرة الحاسوب . يوفر برنامج CADP تقنيات برمجية للتعامل مع النماذج بطريقتين متكاملتين:

  • يمكن تمثيل النماذج الصغيرة بشكل صريح، عن طريق تخزين جميع حالاتها وانتقالاتها في الذاكرة (التحقق الشامل)؛
  • يتم تمثيل النماذج الأكبر حجماً ضمنياً، من خلال استكشاف حالات النموذج والانتقالات اللازمة للتحقق فقط (التحقق أثناء التشغيل).

اللغات وتقنيات التجميع

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

يعتمد بروتوكول CADP على وصف LOTOS للنظام. LOTOS هو معيار دولي لوصف البروتوكولات (معيار ISO/IEC 8807:1989)، يجمع بين مفاهيم جبر العمليات (وخاصةً CCS و CSP) وأنواع البيانات الجبرية المجردة. وبالتالي، يمكن لـ LOTOS وصف كلٍ من العمليات المتزامنة غير المتزامنة وهياكل البيانات المعقدة.

تمت مراجعة LOTOS بشكل كبير في عام 2001، مما أدى إلى نشر E-LOTOS (Enhanced-Lotos، معيار ISO/IEC 15437:2001)، والذي يحاول توفير قدرة تعبيرية أكبر (على سبيل المثال، من خلال إدخال الوقت الكمي لوصف الأنظمة ذات القيود الزمنية الحقيقية) إلى جانب سهولة استخدام أفضل.

توجد العديد من الأدوات لتحويل الأوصاف في حسابات العمليات الأخرى أو التنسيق الوسيط إلى LOTOS، بحيث يمكن بعد ذلك استخدام أدوات CADP للتحقق.

الترخيص والتركيب

يُوزَّع برنامج CADP مجانًا على الجامعات ومراكز البحوث العامة. يمكن للمستخدمين في القطاع الصناعي الحصول على ترخيص تجريبي للاستخدام غير التجاري لفترة محدودة، وبعدها يلزم الحصول على ترخيص كامل. لطلب نسخة من CADP، يُرجى تعبئة نموذج التسجيل على الرابط [ 3 ] . بعد توقيع اتفاقية الترخيص، ستتلقى تفاصيل حول كيفية تنزيل وتثبيت CADP.

ملخص الأدوات

تحتوي مجموعة الأدوات على عدة أدوات:

  • CAESAR.ADT [ 4 ] هو مُترجم يُحوّل أنواع البيانات المجردة في لغة LOTOS إلى أنواع ووظائف لغة C. تتضمن عملية التحويل تقنيات مطابقة الأنماط والتعرف التلقائي على الأنواع الشائعة (الأعداد الصحيحة، والتعدادات، والصفوف، وما إلى ذلك)، والتي يتم تنفيذها على النحو الأمثل.
  • CAESAR [ 5 ] هو مُترجم يُحوّل عمليات LOTOS إما إلى كود C (لأغراض النماذج الأولية السريعة والاختبار) أو إلى رسوم بيانية محدودة (للتحقق). تتم عملية التحويل باستخدام عدة خطوات وسيطة، من بينها بناء شبكة بتري مُوسّعة بمتغيرات مُحددة النوع، وميزات معالجة البيانات، وانتقالات ذرية.
  • OPEN/CAESAR [ 6 ] هي بيئة برمجية عامة لتطوير أدوات تستكشف الرسوم البيانية بشكل فوري (مثل أدوات المحاكاة والتحقق وتوليد الاختبارات). يمكن تطوير هذه الأدوات بشكل مستقل عن أي لغة برمجة عالية المستوى. في هذا السياق، تلعب OPEN/CAESAR دورًا محوريًا في CADP من خلال ربط الأدوات الموجهة نحو اللغة بالأدوات الموجهة نحو النموذج. تتكون OPEN/CAESAR من مجموعة من 16 مكتبة برمجية مع واجهات البرمجة الخاصة بها، مثل:
    • يحتوي Caesar_Hash على العديد من دوال التجزئة
    • Caesar_Solve، الذي يحل أنظمة المعادلات المنطقية أثناء التشغيل
    • Caesar_Stack، الذي يُنفذ المكدسات لاستكشاف البحث العميق أولاً
    • Caesar_Table، الذي يتعامل مع جداول الحالات والانتقالات والتسميات وما إلى ذلك.

تم تطوير عدد من الأدوات ضمن بيئة OPEN/CAESAR:

    • برنامج BISIMULATOR، الذي يتحقق من تكافؤات المحاكاة الثنائية والترتيبات المسبقة.
    • برنامج CUNCTATOR، الذي يقوم بمحاكاة الحالة المستقرة أثناء التشغيل
    • المحدد، الذي يزيل عدم الحتمية العشوائية في الأنظمة العادية أو الاحتمالية أو العشوائية
    • الموزع، الذي يُنشئ الرسم البياني للحالات التي يمكن الوصول إليها باستخدام عدة آلات
    • المُقيِّم، الذي يُقيِّم صيغ حساب التفاضل والتكامل العادية الخالية من التناوب.
    • المنفذ، الذي يقوم بتنفيذ التعليمات البرمجية بشكل عشوائي
    • برنامج EXHIBITOR، الذي يبحث عن تسلسلات التنفيذ التي تطابق تعبيرًا نمطيًا معينًا
    • المولد، الذي يقوم بإنشاء الرسم البياني للحالات التي يمكن الوصول إليها
    • المتنبئ، الذي يتنبأ بجدوى تحليل إمكانية الوصول ،
    • برنامج PROJECTOR، الذي يحسب تجريدات أنظمة الاتصال
    • المُختزل، الذي يقوم بإنشاء وتقليل الرسم البياني للحالات التي يمكن الوصول إليها بتردد علاقات التكافؤ المختلفة
    • برنامج المحاكاة، وبرنامج المحاكاة X، وبرنامج OCIS، والتي تتيح المحاكاة التفاعلية
    • برنامج TERMINATOR، الذي يبحث عن حالات الجمود
  • BCG (الرسوم البيانية المشفرة ثنائيًا) هو تنسيق ملفات لتخزين الرسوم البيانية الضخمة جدًا على القرص (باستخدام تقنيات ضغط فعالة)، وبيئة برمجية للتعامل مع هذا التنسيق، بما في ذلك تقسيم الرسوم البيانية للمعالجة الموزعة. كما يلعب BCG دورًا محوريًا في CADP، حيث تعتمد العديد من الأدوات على هذا التنسيق في مدخلاتها ومخرجاتها. تتكون بيئة BCG من مكتبات متنوعة بواجهات برمجة التطبيقات الخاصة بها، بالإضافة إلى العديد من الأدوات، منها:
    • BCG_DRAW، الذي يبني عرضًا ثنائي الأبعاد للرسم البياني،
    • BCG_EDIT الذي يسمح بتعديل تخطيط الرسم البياني الذي ينتجه Bcg_Draw بشكل تفاعلي
    • BCG_GRAPH، الذي يُنشئ أشكالًا مختلفة من الرسوم البيانية المفيدة عمليًا
    • BCG_INFO، الذي يعرض معلومات إحصائية متنوعة حول الرسم البياني
    • BCG_IO، الذي يقوم بتحويل البيانات بين BCG والعديد من تنسيقات الرسوم البيانية الأخرى.
    • BCG_LABELS، التي تخفي و/أو تعيد تسمية تسميات الانتقال في الرسم البياني (باستخدام التعابير النمطية).
    • BCG_MERGE، الذي يجمع أجزاء الرسم البياني التي تم الحصول عليها من بناء الرسم البياني الموزع
    • BCG_MIN، الذي يقلل من قيمة الرسم البياني modulo التكافؤات القوية أو المتفرعة (ويمكنه أيضًا التعامل مع الأنظمة الاحتمالية والعشوائية).
    • BCG_STEADY، الذي يقوم بإجراء تحليل عددي للحالة المستقرة لسلاسل ماركوف المستمرة (الممتدة)
    • BCG_TRANSIENT، الذي يقوم بإجراء تحليل عددي عابر لسلاسل ماركوف المستمرة (الممتدة)
    • PBG_CP، الذي ينسخ رسم بياني BCG مقسم
    • PBG_INFO، الذي يعرض معلومات حول رسم بياني BCG مقسم
    • PBG_MV الذي ينقل رسم بياني BCG مقسم
    • PBG_RM، الذي يزيل الرسم البياني BCG المقسم
    • لغة XTL (لغة زمنية قابلة للتنفيذ)، هي لغة وظيفية عالية المستوى لبرمجة خوارزميات الاستكشاف على رسوم بيانية BCG. توفر XTL عناصر أساسية للتعامل مع الحالات، والانتقالات، والتسميات، ووظائف الخلف والسابق، وما إلى ذلك. على سبيل المثال، يمكن تعريف دوال تكرارية على مجموعات من الحالات، مما يسمح بتحديد خوارزميات النقطة الثابتة للتقييم والتشخيص في XTL للمنطق الزمني المعتاد (مثل HML، [ 7 ] CTL، [ 8 ] ACTL، [ 9 ] وما إلى ذلك).

يتم ضمان الربط بين النماذج الصريحة (مثل رسوم بيانية BCG) والنماذج الضمنية (التي يتم استكشافها أثناء التشغيل) بواسطة مترجمات متوافقة مع OPEN/CAESAR، بما في ذلك:

    • CAESAR.OPEN، للنماذج المعبر عنها بأوصاف LOTOS
    • BCG.OPEN، للنماذج المُمثلة كرسوم بيانية BCG
    • EXP.OPEN، للنماذج المعبر عنها كآلات متصلة
    • FSP.OPEN، للنماذج المعبر عنها كأوصاف FSP
    • LNT.OPEN، للنماذج المعبر عنها بأوصاف LNT
    • SEQ.OPEN، للنماذج المُمثلة كمجموعات من آثار التنفيذ

تتضمن مجموعة أدوات CADP أيضًا أدوات إضافية، مثل ALDEBARAN و TGV (توليد الاختبار بناءً على التحقق) التي طورها مختبر Verimag (غرونوبل) وفريق مشروع Vertecs التابع لـ INRIA رين.

أدوات CADP متكاملة بشكل جيد ويمكن الوصول إليها بسهولة باستخدام واجهة EUCALYPTUS الرسومية أو لغة البرمجة النصية SVL [ 10 ] . يوفر كل من EUCALYPTUS وSVL للمستخدمين وصولاً سهلاً وموحداً إلى أدوات CADP من خلال إجراء تحويلات تنسيق الملفات تلقائياً عند الحاجة، وتوفير خيارات سطر الأوامر المناسبة عند استدعاء الأدوات.

الجوائز

  • في عام 2002، حصل رادو ماتيسكو، الذي صمم وطور مدقق نموذج EVALUATOR الخاص بـ CADP، على جائزة تكنولوجيا المعلومات التي مُنحت خلال الدورة العاشرة من الندوة السنوية التي نظمتها مؤسسة Rhône-Alpes Futur. [ 11 ]
  • في عام 2019، فاز فريدريك لانغ وفرانكو مازنتي بجميع الميداليات الذهبية في مسابقة RERS للمسائل المتوازية، وذلك باستخدام CADP لتقييم 360 صيغة منطقية شجرية حسابية (CTL) ومنطق زمني خطي (LTL) بنجاح ودقة على مجموعات متنوعة من آلات الحالة المتصلة. [ 13 ] [ 14 ]
  • في عام 2020، فاز فريدريك لانغ وفرانكو مازنتي وويندلين سيروي بثلاث ميداليات ذهبية في تحدي RERS'2020 من خلال حل 88% من مسائل "Parallel CTL" بشكل صحيح، ولم يقدموا سوى إجابات "لا أعرف" لـ 11 صيغة فقط من أصل 90. [ 15 ] [ 16 ] [ 17 ]
  • في عام 2021، فاز كل من هيوبرت جارافيل، وفريديريك لانج، ورادو ماتيسكو، وويندلين سيروي معًا بجائزة الابتكار من Inria – Académie des Sciences – Dassault Systèmes لعملهم العلمي الذي أدى إلى تطوير مجموعة أدوات CADP. [ 18 ]
  • في عام 2023، حصل كل من هوبرت غارافيل، وفريدريك لانغ، ورادو ماتيسكو، وويندلين سيروي، بشكل مشترك، على جائزة "أداة اختبار الزمن" الأولى من نوعها من ETAPS ، المنتدى الأوروبي الرائد لعلوم البرمجيات، وذلك عن مجموعة أدوات CADP. [ 19 ]

انظر أيضاً

مراجع

  1. ↑ غارافيل هـ، لانغ ف، ماتيسكو ر، سيروي و: CADP 2011: مجموعة أدوات لبناء وتحليل العمليات الموزعة، المجلة الدولية لأدوات البرمجيات لنقل التكنولوجيا (STTT)، 15(2):89-107، أبريل 2013
  2. ↑ معيار ISO 8807، مواصفات لغة الترتيب الزمني
  3. ↑ نموذج طلب CADP عبر الإنترنت . Cadp.inria.fr (30-08-2011). تم الاطلاع عليه بتاريخ 16-06-2014.
  4. ↑ H. Garavel. تجميع أنواع البيانات المجردة LOTOS ، في وقائع المؤتمر الدولي الثاني حول تقنيات الوصف الرسمي FORTE'89 (فانكوفر، كولومبيا البريطانية، كندا)، ST Vuong (محرر)، نورث هولاند، ديسمبر 1989، ص 147-162.
  5. ↑ H. Garavel, J. Sifakis. Compilation and Verification of LOTOS Specifications , in Proceedings of the 10th International Symdioment on Protocol Specification, Testing and Verification (Ottawa, Canada), L. Logrippo, RL Probert, H. Ural (editors), North-Holland, IFIP, June 1990, p. 379–394.
  6. ↑ H. Garavel. OPEN/CÆSAR: بنية برمجية مفتوحة للتحقق والمحاكاة والاختبار ، في وقائع المؤتمر الدولي الأول حول الأدوات والخوارزميات لبناء وتحليل الأنظمة TACAS'98 (لشبونة، البرتغال)، برلين، B. Steffen (محرر)، سلسلة محاضرات في علوم الحاسوب، النسخة الكاملة متاحة كتقرير بحثي من Inria RR-3352 ، Springer Verlag، مارس 1998، المجلد 1384، ص 68-84.
  7. ↑ م. هينيسي، ر. ميلنر. القوانين الجبرية لعدم الحتمية والتزامن ، في: مجلة ACM ، 1985، المجلد 32، ص 137-161.
  8. ↑ إي إم كلارك، إي إيه إيمرسون، إيه بي سيستلا. التحقق التلقائي من الأنظمة المتزامنة ذات الحالة المحدودة باستخدام مواصفات المنطق الزمني ، في: معاملات ACM في لغات البرمجة والأنظمة ، أبريل 1986، المجلد 8، العدد 2، ص 244-263.
  9. ↑ R. De Nicola, FW Vaandrager. Action vs State Based Logics for Transition Systems , Lecture Notes in Computer Science , Springer Verlag, 1990, vol. 469, p. 407–419.
  10. ↑ H. Garavel, F. Lang. SVL: لغة برمجة نصية للتحقق التركيبي ، في: وقائع المؤتمر الدولي الحادي والعشرين لمجموعة العمل 6.1 التابعة للاتحاد الدولي لمعالجة المعلومات حول التقنيات الرسمية للأنظمة الشبكية والموزعة FORTE'2001 (جزيرة جيجو، كوريا)، M. Kim، B. Chin، S. Kang، D. Lee (محررون)، النسخة الكاملة متاحة كتقرير بحثي من Inria RR-4223 ، Kluwer Academic Publishers، IFIP، أغسطس 2001، ص 377-392.
  11. ^ "Radu Mateescu يفوز بجائزة تكنولوجيا المعلومات الممنوحة من Fondation Rhône-Alpes Futur" .
  12. ↑ إيزابيل بيلين (16 أبريل 2011). "هوبرت غارافيل يحصل على جائزة غاي-لوساك هومبولت للبحوث" . مؤرشف من الأصل بتاريخ 10 يوليو 2016.
  13. ↑ "نتائج تحدي RERS لعام 2019" .
  14. ↑ "نشرة CADP رقم 12 - 10 أبريل 2019" .
  15. ↑ "نتائج تحدي RERS لعام 2020" .
  16. ↑ "فريق CNR-Inria يفوز بالميداليات الذهبية في تحدي RERS 2020 Parallel CTL" .
  17. ↑ "نشرة CADP رقم 13 - 22 فبراير 2021" .
  18. ↑ "يعزز فريق Convecs أمن الأنظمة المتوازية" .
  19. ↑ "جائزة ETAPS لأداة اختبار الزمن" .