تحسين التجريد الموجه بالأمثلة المضادة

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

يُعدّ تحسين التجريد الموجه بالأمثلة المضادة ( CEGAR ) أسلوبًا للتحقق من النماذج الرمزية . [ 1 ] [ 2 ] كما يُطبّق أيضًا في خوارزميات حسابات الجداول المنطقية لتحسين كفاءتها. [ 3 ]

في التحقق والتحليل بمساعدة الحاسوب للبرامج، غالبًا ما تتكون نماذج الحوسبة من حالات . ومع ذلك، قد تحتوي نماذج حتى البرامج الصغيرة على عدد هائل من الحالات. تُعرف هذه المشكلة بمشكلة انفجار الحالات. [ 4 ] يعالج مركز CEGAR هذه المشكلة على مرحلتين: التجريد ، الذي يبسط النموذج بتجميع الحالات، والتحسين ، الذي يزيد من دقة التجريد لتقريب النموذج الأصلي بشكل أفضل.

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

التحقق من البرنامج

التجريد

للتحقق من صحة البرنامج، لا سيما البرامج التي تتضمن مفهوم الزمن للتزامن ، تُستخدم نماذج انتقال الحالة. على وجه الخصوص، يمكن استخدام نماذج الحالات المحدودة مع المنطق الزمني في التحقق التلقائي. [ 6 ] وبالتالي، يقوم مفهوم التجريد على أساس الربط بين بنيتين من بنى كريپكي . وبالتحديد، يمكن وصف البرامج باستخدام أتمتة تدفق التحكم (CFA). [ 7 ]

عرّف بنية كريپكيم{\displaystyle M}مثل⟨S،s0،R،L⟩{\displaystyle \langle S,s_{0},R,L\rangle }، أين

  • S{\displaystyle S}هي مجموعة محدودة من الحالات،
  • s0{\displaystyle s_{0}}هي حالة ابتدائية فيS{\displaystyle S}،
  • R{\displaystyle R}هي علاقة انتقالية شاملة، و
  • L{\displaystyle L}هي دالة تقوم بتصنيف كل حالة بمجموعة من الأسماء المنطقية التي تنطبق عليها.

تجريد لـم{\displaystyle M}يتم تعريفها بواسطة⟨Sα،s0α،Rα،Lα⟩{\displaystyle \langle S_{\alpha },s_{0}^{\alpha },R_{\alpha },L_{\alpha }\rangle }أينα{\displaystyle \alpha }هي عملية تجريد تقوم برسم خريطة لكل حالة فيS{\displaystyle S}إلى ولاية فيSα{\displaystyle S_{\alpha }}[ 5 ]​

للحفاظ على الخصائص الأساسية للنموذج، يقوم رسم الخرائط التجريدية برسم الحالة الأولية في النموذج الأصليs0{\displaystyle s_{0}}إلى نظيرهs0α{\displaystyle s_{0}^{\alpha }}في النموذج المجرد. كما يضمن تعيين التجريد الحفاظ على علاقات الانتقال بين حالتين.

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

في كل تكرار، يتم إجراء فحص النموذج للنموذج المجرد. على سبيل المثال، يقوم فحص النموذج المحدود بإنشاء صيغة منطقية يتم فحصها بعد ذلك للتأكد من قابليتها للإرضاء المنطقي بواسطة محلل SAT . [ 5 ]

التحسين

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

تضمن عملية التحسين عدم انتماء الحالات المسدودة والحالات السيئة إلى نفس الحالة المجردة. الحالة المسدودة هي حالة يمكن الوصول إليها دون وجود انتقال خارجي، بينما الحالة السيئة هي حالة تتضمن انتقالات تؤدي إلى ظهور المثال المضاد. [ 2 ]

حسابات الجدول

بما أن المنطق الموجه غالباً ما يتم تفسيره بدلالات كريپكي ، حيث يشبه إطار كريپكي بنية أنظمة انتقال الحالة المعنية في التحقق من البرامج، فإن تقنية CEGAR يتم تطبيقها أيضاً لإثبات النظريات الآلي . [ 3 ]

مراجع

  1. ↑ كلارك، إدموند ؛ غرومبيرغ، أورنا ؛ جها، سوميش؛ لو، يوان؛ فيث، هيلموت (1 سبتمبر 2003). "تحسين التجريد الموجه بالأمثلة المضادة للتحقق من النموذج الرمزي" . مجلة ACM . 50 (5): 752-794 . doi : 10.1145/876638.876643 .
  2. 1 2 كلارك، إدموند ؛ غرومبيرغ، أورنا ؛ جها، سوميش؛ لو، يوان؛ فيث، هيلموت (2000). تحسين التجريد الموجه بالأمثلة المضادة . المؤتمر الدولي للتحقق بمساعدة الحاسوب CAV 2000: التحقق بمساعدة الحاسوب. سلسلة محاضرات في علوم الحاسوب. المجلد 1855. برلين، هايدلبرغ: سبرينغر. الصفحات 154-169 . doi : 10.1007/10722167_15 . ISBN   978-3-540-45047-4.
  3. 1 2 غوريه، راجيف؛ كيكرت، كورماك (6 سبتمبر 2021). CEGAR-Tableaux: تحسين قابلية الإرضاء المشروط عبر تعلم العبارات المشروطة وSAT . الاستدلال الآلي باستخدام الجداول التحليلية والأساليب ذات الصلة: المؤتمر الدولي الثلاثون، TABLEAUX 2021، برمنغهام، المملكة المتحدة. سلسلة محاضرات في علوم الحاسوب. المجلد 12842. تشام: سبرينغر. الصفحات 74-91 . doi : 10.1007/978-3-030-86059-2_5 . ISBN   978-3-030-86059-2.
  4. ↑ فالماري، أنتي (1998). مشكلة انفجار الحالات . دورة متقدمة في شبكات بيتري، ACPN 1996. سلسلة محاضرات في علوم الحاسوب. المجلد 1491. برلين، هايدلبرغ: سبرينغر. الصفحات 429-528 . doi : 10.1007/978-3-642-35746-6_1 . ISBN   978-3-540-49442-3تم الاطلاع عليه بتاريخ 27 ديسمبر 2023 .
  5. 1 2 3 كلارك، إدموند ؛ كليبر، ويليام؛ نوفاتشيك، ميلوش؛ زولياني، باولو (2011). التحقق من النموذج ومشكلة انفجار الحالة . مدرسة LASER الصيفية لهندسة البرمجيات: LASER 2011. سلسلة محاضرات في علوم الحاسوب. المجلد 7682. الصفحات 1-30. doi : 10.1007 / 978-3-642-35746-6_1 . ISBN   978-3-642-35746-6تم الاطلاع عليه بتاريخ 27 ديسمبر 2023 .
  6. ↑ كلارك، إدموند ؛ براون، مايكل سي؛ إيمرسون، إي. ألين ؛ سيستلا، أ.ب. "استخدام المنطق الزمني للتحقق التلقائي من أنظمة الحالة المحدودة". منطق ونماذج الأنظمة المتزامنة . ناتو ASI. المجلد 13. برلين، هايدلبرغ: سبرينغر. doi : 10.1007/978-3-642-82453-1_1 . ISBN  978-3-642-82453-1.
  7. ↑ هاجدو، آكوس؛ ميكيسكي، زولتان (11 نوفمبر 2019). "استراتيجيات فعالة لفحص النماذج المستندة إلى CEGAR" . مجلة الاستدلال الآلي . 64 (4). سبرينغر نيتشر: 1051–1091 . دوى : 10.1007/s10817-019-09535-x .