2025-11-24T00:55:25.034139

PolyVer: A Compositional Approach for Polyglot System Modeling and Verification

Chen, Lin, Godbole et al.
Several software systems are polyglot; that is, they comprise programs implemented in a combination of programming languages. Verifiers that directly run on mainstream programming languages are currently customized for single languages. Thus, to verify polyglot systems, one usually translates them into a common verification language or formalism on which the verifier runs. In this paper, we present an alternative approach, PolyVer, which employs abstraction, compositional reasoning, and synthesis to directly perform polyglot verification. PolyVer constructs a formal model of the original polyglot system as a transition system where the update functions associated with transitions are implemented in target languages such as C or Rust. To perform verification, PolyVer then connects a model checker for transition systems with language-specific verifiers (e.g., for C or Rust) using pre/post-condition contracts for the update functions. These contracts are automatically generated by synthesis oracles based on syntax-guided synthesis or large language models (LLMs), and checked by the language-specific verifiers. The contracts form abstractions of the update functions using which the model checker verifies the overall system-level property on the polyglot system model. PolyVer iterates between counterexample-guided abstraction-refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS) until the property is verified or a true system-level counterexample is found. We demonstrate the utility of PolyVer for verifying programs in the Lingua Franca polyglot language using the UCLID5 model checker connected with the CBMC and Kani verifiers for C and Rust respectively.
academic

PolyVer: منهج تركيبي لنمذجة والتحقق من أنظمة متعددة اللغات البرمجية

المعلومات الأساسية

  • معرّف الورقة: 2503.03207
  • العنوان: PolyVer: منهج تركيبي لنمذجة والتحقق من أنظمة متعددة اللغات البرمجية
  • المؤلفون: Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, Sanjit A. Seshia
  • التصنيف: cs.PL (لغات البرمجة)
  • تاريخ النشر/المؤتمر: Formal Methods in Computer-Aided Design 2025
  • رابط الورقة: https://arxiv.org/abs/2503.03207

الملخص

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

خلفية البحث والدافع

تعريف المشكلة

تعتمد الأنظمة البرمجية الحديثة بشكل متزايد على معماريات متعددة اللغات، حيث تسمح أطر عمل مثل ROS2 و Lingua Franca للمطورين باختيار أنسب لغة برمجية لكل مكون. ومع ذلك، تجلب هذه المرونة تحديات التحقق:

  1. اختلافات دلالات اللغة: تتمتع لغات البرمجة المختلفة بنحو ودلالات مختلفة، مثل دالة saturating_add في Rust التي تشبع إلى القيمة القصوى عند الفيضان، بينما قد يحدث التفاف في عملية الجمع في C.
  2. قيود المدققات الحالية: معظم مدققات البرامج (مثل CBMC للغة C و Kani للغة Rust) مصممة خصيصاً للغة واحدة ولا يمكنها التعامل مباشرة مع الأنظمة متعددة اللغات.
  3. تعقيد الترجمة: ترجمة نظام متعدد اللغات بالكامل إلى لغة تحقق واحدة تتطلب دعم النحو والدلالات الكاملة لجميع اللغات، وهو أمر محظور للغات الحديثة.

أهمية البحث

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

قيود الطرق الموجودة

  • طرق الترجمة الموحدة: تتطلب تطوير بنية مترجم كاملة لكل لغة
  • صعوبة الحفاظ على الدلالات: من الصعب التقاط جميع الإنشاءات الخاصة باللغة المصدر بأمانة في لغة التحقق الهدف
  • مشاكل قابلية التوسع: قد تصبح مشاكل التحقق المُنتجة كبيرة جداً

المساهمات الأساسية

  1. تشكيل رسمي لمشكلة التحقق متعدد اللغات: تشكيل منهجي لأول مرة لمشكلة التحقق متعدد اللغات واقتراح حل تركيبي يدمج عدة مدققات خاصة باللغة.
  2. توليف العقود المؤتمت: اقتراح طريقة توليف وتحسين عقود الشروط المسبقة واللاحقة المؤتمتة باستخدام لغة وسيطة و حلقة CEGIS-CEGAR، مع دعم التوليف الموجه بالنحو ونماذج اللغة الكبيرة كمتنبئات توليف.
  3. تطبيق الأداة: تطبيق أداة PolyVer بناءً على UCLID5، مع دعم C و Rust، من خلال مدققات CBMC و Kani، مما يثبت أن متنبئات التوليف المستندة إلى نماذج اللغة الكبيرة تتفوق على طرق التوليف الرمزي البحت.
  4. دراسات الحالة والتقييم: تطوير مدقق للغة التنسيق Lingua Franca، والتحقق من الأنظمة متعددة اللغات التي تحتوي على عمليات C و Rust، وأجزاء من لغة C التي لم تدعمها الأعمال السابقة.

شرح الطريقة

تعريف المهمة

الإدخال: نموذج متعدد اللغات M = (Q,V,I₀,T,F) وخاصية النظام φ الإخراج: نتيجة التحقق (نجح/فشل) وربما مسار مضاد الهدف: تحديد ما إذا كان M ⊨ φ صحيحاً

حيث:

  • Q: مجموعة الأنماط
  • V: مجموعة المتغيرات المكتوبة
  • I₀: مجموعة الحالات الأولية
  • T: مجموعة انتقالات الأنماط
  • F: مجموعة العمليات

معمارية النموذج

1. آلة الحالة الموسعة (ESM)

يقوم PolyVer بنمذجة الأنظمة متعددة اللغات كآلات حالة موسعة، حيث:

  • تتكون الحالات من أنماط وتعيينات متغيرات
  • ترتبط الانتقالات بشروط حماية وعلاقات تحديث
  • تتخصص علاقات التحديث في سلاسل استدعاءات العمليات

2. لغة العقد الوسيطة L*

الابتكار الرئيسي هو إدخال لغة وسيطة L* كـ "لاصق" بين اللغات المختلفة:

  • تُكتب العقود باستخدام L*
  • يتم تحويلها إلى لغات ملموسة من خلال ترجمة حفظ الدلالات compL
  • تتجنب تعقيد ترجمة اللغة الكاملة

3. طريقة CEGIS-CEGAR الهجينة

يتمثل جوهر الخوارزمية في حلقتي تكرار متداخلتين:

حلقة CEGAR الخارجية:

  1. بناء نموذج مجرد M' باستخدام العقود الحالية
  2. فاحص النموذج يتحقق من M' ⊨ φ
  3. إذا فشل، تحقق مما إذا كان المضاد وهمياً
  4. إذا كان وهمياً، قم بتحسين العقد؛ وإلا أبلغ عن مضاد حقيقي

حلقة CEGIS الداخلية:

  1. متنبئ التوليف ينتج عقود مرشحة
  2. فاحص التحقق يتحقق من صحة العقد
  3. إذا كان غير صحيح، أضف أمثلة موجبة وأعد التوليف

نقاط الابتكار التقني

1. استراتيجية التحقق التركيبية

بخلاف الترجمة الموحدة، يعتمد PolyVer على استراتيجية "فرّق تسد":

  • استخدام تجريد العقود للعمليات الفردية
  • مدققات خاصة باللغة تتحقق من صحة العقود
  • فاحص النموذج يتحقق من خصائص المستوى النظامي

2. توليف العقود المؤتمت

يدعم متنبئات توليف متعددة:

  • مولد قائم على نماذج اللغة الكبيرة: استخدام تلميحات سلسلة الفكر و DSL بايثون
  • مولد SyGuS/SyMO: ترميز المشكلة كمشكلة برمجة بالأمثلة

3. فحص الوهمية

من خلال التحقق من {V = d} C {V' ≠ d'} للتحقق من قابلية الوصول إلى مسار المضاد، التمييز بين المضادات الحقيقية والوهمية.

إعداد التجارب

مجموعة البيانات

  1. معايير LFVerifier: 22 برنامج Lingua Franca، يتضمن نحو C مقيد
  2. أمثلة LF الكاملة: متحكم LED، روبوت متسلق، متحكم موقف القمر الصناعي وأنظمة مدمجة أخرى
  3. أنظمة متعددة اللغات: برامج LF مختلطة C/Rust، تطبيقات ROS2، برامج استدعاء FFI

مقاييس التقييم

  • عدد تكرارات التوليف (IS: تكرارات CEGIS، AR: تكرارات CEGAR)
  • وقت التشغيل (SOT: وقت متنبئ التوليف، VOT: وقت فاحص التحقق، UT: وقت UCLID5)
  • معدل نجاح التحقق

الطرق المقارنة

المقارنة مع LFVerifier15، وهي الأداة الوحيدة المعروفة للتحقق الآلي الشامل من برامج LF.

تفاصيل التطبيق

  • استخدام OpenAI o1-mini كمولد قائم على نماذج اللغة الكبيرة، مع 3 استعلامات متوازية لكل عملية
  • CBMC-6.3.1 و Kani-0.56.0 و z3-4.8.7 كنهايات خلفية للتحقق
  • جهاز Intel Core i9 بسرعة 3.7GHz، ذاكرة RAM بسعة 62GB

نتائج التجارب

النتائج الرئيسية

RQ1: المقارنة مع أعمال التحقق من LF الموجودة

في 22 معيار:

  • PolyVer ينجح في التحقق من جميع المعايير، بينما LFVerifier لا يستطيع التحقق من مثال TrafficLight
  • 18 معيار يتم توليف العقود بشكل صحيح في تكرار CEGIS واحد، بمتوسط 37 ثانية
  • على الرغم من أن إجمالي وقت التشغيل أبطأ (يهيمن عليه وقت توليف العقود)، إلا أنه يوفر تحسينات نوعية كبيرة

RQ2: التعامل مع أمثلة LF الكاملة

نجح في التحقق من الأنظمة المدمجة التي تحتوي على كود C كامل:

  • متحكم LED: عملية واحدة، 123 سطر كود C، 31.0 ثانية وقت توليف
  • روبوت متسلق: 12 عملية، 75 سطر كود C/Rust، 685.4 ثانية وقت توليف
  • متحكم القمر الصناعي: 6 عمليات، 424 سطر كود C، 729.0 ثانية وقت توليف

RQ3: التحقق من الأنظمة متعددة اللغات

التحقق من الأنظمة متعددة اللغات الحقيقية:

  • برامج LF مختلطة C/Rust
  • تطبيقات خدمات ROS2
  • برامج استدعاء FFI عبر اللغات

النتائج المهمة

  1. تفوق نماذج اللغة الكبيرة على الطرق الرمزية: حلالات SyGuS/SyMO تتطلب عدد كبير من تكرارات CEGAR وغالباً ما تفشل في الإنهاء
  2. تحديات توليف العقود: العمليات ذات تدفق التحكم المعقد والاعتماديات البيانات تتطلب تكرارات أكثر
  3. التحقق من الجدوى العملية: القدرة على التعامل مع كود التطبيق الفعلي وليس أمثلة لعبة

الأعمال ذات الصلة

التحقق من الأنظمة متعددة اللغات

  • طرق الترجمة اليدوية: ترجمة Cook وآخرون لكود التجميع إلى C للتحقق من مراقب الآلة الافتراضية Xen
  • ترجمة الأجزاء التلقائية: ترجمة LFVerifier التلقائية لأجزاء C إلى لغة التحقق
  • طرق الصندوق الأسود: استنتاج الملخصات من سلوك الإدخال والإخراج

التحقق التركيبي

  • يتم تطبيق التحقق التركيبي المستند إلى منطق Hoare على نطاق واسع في برامج أحادية اللغة الكبيرة
  • استخدام التفسير المجرد و CEGAR لأتمتة تعلم الشروط المسبقة واللاحقة

استنتاج العقود

  • طرق استنتاج العقود الموجهة بالخصائص
  • حلالات فقرات Horn المقيدة
  • التطبيقات الحديثة لنماذج اللغة الكبيرة في تعلم المواصفات

الخلاصة والنقاش

الاستنتاجات الرئيسية

  1. ينجح PolyVer في حل التحديات الرئيسية للتحقق من الأنظمة متعددة اللغات
  2. يتجنب المنهج التركيبي تعقيد ترجمة اللغة الكاملة
  3. يجعل توليف العقود المؤتمت الطريقة عملية
  4. يتفوق مولد قائم على نماذج اللغة الكبيرة على الطرق الرمزية التقليدية

القيود

  1. الإنهاء: الخوارزمية لا تضمن الإنهاء، وتعتمد على جودة متنبئ التوليف
  2. دعم اللغات: يدعم حالياً فقط C و Rust، ويتطلب تطوير متنبئات تحقق للغات أخرى
  3. تعبيرية العقود: تحد قدرة التعبير عن اللغة الوسيطة L* من تعقيد الخصائص القابلة للتحقق
  4. قابلية التوسع: قد يصبح وقت توليف العقود للأنظمة الكبيرة عنق الزجاجة

الاتجاهات المستقبلية

  1. التوسع إلى أنظمة برمجية موزعة متعددة اللغات أخرى وأنظمة برمجيات الروبوتات
  2. التطبيق على التحقق الرسمي من ترجمة الكود (مثل ترجمة C إلى Rust)
  3. تحسين كفاءة ودقة توليف العقود
  4. دعم خصائص منطق زمني أكثر تعقيداً

التقييم المتعمق

المميزات

  1. أهمية المشكلة: التحقق من الأنظمة متعددة اللغات مشكلة عملية وهامة
  2. ابتكار الطريقة: الجمع بين التحقق التركيبي وتوليف العقود المؤتمت جديد
  3. الأساس النظري: التعريف الرسمي واضح والضمانات الصحيحة محددة
  4. القيمة العملية: القدرة على التعامل مع أنظمة حقيقية وليس أمثلة لعبة
  5. تطبيق الأداة: توفير تطبيق أداة قابل للاستخدام

أوجه القصور

  1. الحمل الأداء: وقت توليف العقود طويل نسبياً، قد يحد من التطبيق العملي
  2. تغطية اللغات: يدعم حالياً فقط C و Rust، لا تزال قابلية التوسع بحاجة إلى التحقق
  3. المعايير محدودة: على الرغم من تضمن أمثلة حقيقية، الحجم نسبياً صغير
  4. الاعتماد على نماذج اللغة الكبيرة: الاعتماد على خدمات نماذج اللغة الكبيرة التجارية قد يؤثر على قابلية إعادة الإنتاج

التأثير

  1. المساهمة الأكاديمية: فتح اتجاه بحثي جديد للتحقق من الأنظمة متعددة اللغات
  2. القيمة العملية: توفير أداة تحقق للأنظمة متعددة اللغات الحساسة من حيث السلامة
  3. الإلهام التقني: فكرة العقود كواجهة بين اللغات لها قيمة عامة

السيناريوهات المعمول بها

  1. الأنظمة المدمجة: أنظمة الوقت الفعلي المختلطة C/Rust
  2. الأنظمة الموزعة: أطر عمل ROS2 و gRPC وغيرها متعددة اللغات
  3. التطبيقات الحساسة من حيث السلامة: الأنظمة التي تتطلب ضمانات التحقق الرسمي
  4. تكامل الأنظمة الموروثة: أنظمة مختلطة من الكود القديم والجديد

المراجع

تستشهد الورقة بـ 50 مرجعاً ذا صلة، تغطي أنظمة متعددة اللغات والتحقق الرسمي واستنتاج العقود والتوليف الموجه بالنحو وغيرها من المجالات المهمة، مما يوفر أساساً نظرياً متيناً للبحث.

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