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

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

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

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

طُوِّرت فئةٌ مهمةٌ من أساليب التحقق من النماذج لفحص نماذج تصميمات الأجهزة والبرامج ، حيث تُعطى المواصفات بصيغة منطقية زمنية . وقد قام أمير بنويلي بعملٍ رائدٍ في مجال مواصفات المنطق الزمني ، وحصل على جائزة تورينج عام 1996 عن "عمله الرائد في إدخال المنطق الزمني إلى علوم الحاسوب". ^{[ 3 ]} بدأ التحقق من النماذج مع العمل الرائد لكلٍّ من إي إم كلارك ، وإي إيه إيمرسون ، ^{[ 4 ] [ 5 ] [ 6 ]} وجي بي كويل، وجيه سيفاكيس . ^{[ 7 ]} تقاسم كلارك وإيمرسون وسيفاكيس جائزة تورينج عام 2007 لعملهم الرائد في تأسيس وتطوير مجال التحقق من النماذج. ^{[ 8 ] [ 9 ]}

يُستخدم التحقق من النماذج غالبًا في تصميمات الأجهزة. أما بالنسبة للبرمجيات، فبسبب عدم قابلية الحسم (انظر نظرية الحوسبة )، لا يمكن أن يكون هذا النهج خوارزميًا بالكامل، أو أن ينطبق على جميع الأنظمة، أو أن يُعطي إجابة دائمًا؛ ففي الحالة العامة، قد يفشل في إثبات أو دحض خاصية معينة. في أجهزة الأنظمة المدمجة ، من الممكن التحقق من صحة المواصفات المُقدمة، على سبيل المثال، باستخدام مخططات نشاط UML ^{[ 10 ]} أو شبكات بتري المُفسَّرة للتحكم ^{[ 11 ]} .

عادةً ما يُقدَّم هيكل البرنامج كوصفٍ لشفرة المصدر بلغة وصف الأجهزة الصناعية أو لغة برمجة متخصصة. يُقابل هذا البرنامج آلة الحالة المحدودة (FSM)، أي رسمًا بيانيًا موجهًا يتكون من عُقد (أو رؤوس ) وحواف . ترتبط بكل عُقدة مجموعة من القضايا الذرية، تُحدد عادةً عناصر الذاكرة التي قيمتها واحد. تُمثل العُقد حالات النظام، بينما تُمثل الحواف الانتقالات المُحتملة التي قد تُغير الحالة، في حين تُمثل القضايا الذرية الخصائص الأساسية التي تسري عند نقطة التنفيذ. ^{[ 12 ]}

بصورة رسمية، يمكن صياغة المشكلة على النحو التالي: بالنظر إلى خاصية مرغوبة، معبر عنها بصيغة منطقية زمنية${\displaystyle p}$وهيكل${\displaystyle M}$مع الحالة الأولية${\displaystyle s}$قرر ما إذا${\displaystyle M,s\models p}$. لو${\displaystyle M}$بما أن البيانات محدودة، كما هو الحال في الأجهزة، فإن التحقق من النموذج يختزل إلى بحث في الرسم البياني .

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

تاريخيًا، استخدمت الطرق الرمزية الأولى مخططات القرار الثنائية (BDDs ). بعد نجاح إمكانية إرضاء القضايا في حل مشكلة التخطيط في الذكاء الاصطناعي (انظر satplan ) عام 1996، عُمِّمَ النهج نفسه للتحقق من صحة النماذج في المنطق الزمني الخطي (LTL): إذ تُقابل مشكلة التخطيط التحقق من صحة النماذج لخصائص السلامة. تُعرف هذه الطريقة بالتحقق المحدود من صحة النماذج. ^{[ 13 ]} وقد أدى نجاح حلول إمكانية إرضاء القضايا المنطقية في التحقق المحدود من صحة النماذج إلى انتشار استخدام حلول إمكانية الإرضاء في التحقق الرمزي من صحة النماذج. ^{[ 14 ]}

تواجه أدوات التحقق من النماذج مشكلة تضخم فضاء الحالة، والمعروفة باسم مشكلة انفجار الحالة ، والتي يجب معالجتها لحل معظم مشاكل العالم الحقيقي. وهناك عدة طرق لمواجهة هذه المشكلة.

1. تتجنب الخوارزميات الرمزية إنشاء الرسم البياني لآلة الحالة المحدودة (FSM) بشكل صريح؛ بل تمثله ضمنيًا باستخدام صيغة في منطق القضايا الكمي. وقد شاع استخدام مخططات القرار الثنائية (BDDs) بفضل أعمال كين ماكميلان ^{[ 16 ]} ، وكذلك أعمال أوليفييه كودير وجان كريستوف مادري ^{[ 17 ]} ، وتطوير مكتبات مفتوحة المصدر لمعالجة مخططات القرار الثنائية مثل CUDD ^{[ 18 ] وBuDDy [ 19 ]} .
2. تقوم خوارزميات التحقق من النموذج المحدود بفكّ آلة الحالة المحدودة لعدد ثابت من الخطوات،${\displaystyle k}$وتحقق مما إذا كان من الممكن حدوث انتهاك للملكية في${\displaystyle k}$أو خطوات أقل. يتضمن هذا عادةً ترميز النموذج المقيد كمثال على SAT . يمكن تكرار العملية بقيم أكبر فأكبر لـ${\displaystyle k}$إلى أن يتم استبعاد جميع الانتهاكات المحتملة (انظر البحث التكراري العميق أولاً ).
3. يسعى التجريد إلى إثبات خصائص نظام ما من خلال تبسيطه أولًا. عادةً لا يُحقق النظام المُبسط نفس خصائص النظام الأصلي تمامًا، مما قد يستدعي عملية تحسين. عمومًا، يُشترط أن يكون التجريد سليمًا (أي أن الخصائص المُثبتة فيه تنطبق على النظام الأصلي)؛ مع ذلك، قد لا يكون التجريد كاملًا في بعض الأحيان (أي أن بعض خصائص النظام الأصلي لا تنطبق على التجريد). من أمثلة التجريد تجاهل قيم المتغيرات غير المنطقية والاكتفاء بالمتغيرات المنطقية وتدفق التحكم في البرنامج؛ قد يكون هذا التجريد، رغم بساطته الظاهرية، كافيًا لإثبات خصائص مثل الاستبعاد المتبادل .
4. تبدأ عملية تحسين التجريد الموجه بالأمثلة المضادة (CEGAR) بالتحقق من خلال تجريد تقريبي (أي غير دقيق) ثم تُحسّنه بشكل متكرر. عند اكتشاف انتهاك (أي مثال مضاد )، تُحلل الأداة مدى جدواه (أي، هل الانتهاك حقيقي أم ناتج عن تجريد غير مكتمل؟). إذا كان الانتهاك ممكنًا، يتم إبلاغ المستخدم به. أما إذا لم يكن كذلك، فيُستخدم دليل عدم الجدوى لتحسين التجريد، ثم يبدأ التحقق من جديد. ^{[ 20 ]}

تم تطوير أدوات التحقق من النماذج في البداية للتفكير في الصحة المنطقية لأنظمة الحالة المنفصلة ، ​​ولكن تم توسيعها منذ ذلك الحين للتعامل مع الوقت الحقيقي والأشكال المحدودة من الأنظمة الهجينة .

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

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

تندرج هذه المسألة ضمن فئة الدوائر AC ^0. ويمكن حلها عند فرض بعض القيود على بنية الإدخال، كاشتراط أن يكون عرض الشجرة محدودًا بثابت (وهو ما يعني عمومًا سهولة التحقق من النموذج لمنطق الرتبة الثانية الأحادي )، وتحديد درجة كل عنصر من عناصر المجال، وشروط أكثر عمومية كالتوسع المحدود ، والتوسع المحدود محليًا، والبنى غير الكثيفة في أي مكان. ^{[ 21 ]} وقد وُسِّعت هذه النتائج لتشمل مهمة حصر جميع حلول صيغة من الرتبة الأولى ذات متغيرات حرة.

فيما يلي قائمة بأدوات التحقق من النماذج المهمة:

• أفرا: أداة للتحقق من النماذج للغة ريبيكا، وهي لغة قائمة على الممثلين لنمذجة الأنظمة المتزامنة والتفاعلية
• سبيكة (محلل السبائك)
• BLAST (أداة التحقق من البرمجيات بتقنية التجريد الكسول من بيركلي)
• CADP (بناء وتحليل العمليات الموزعة) هي مجموعة أدوات لتصميم بروتوكولات الاتصال والأنظمة الموزعة
• CPAchecker : أداة مفتوحة المصدر للتحقق من نماذج البرامج المكتوبة بلغة C، تعتمد على إطار عمل CPA
• إكلير : منصة للتحليل والتحقق والاختبار والتحويل التلقائي لبرامج C و C++
• FDR2 : أداة للتحقق من صحة نماذج الأنظمة في الوقت الحقيقي التي تم تصميمها وتحديدها كعمليات CSP
• FizzBee : بديل أسهل استخدامًا لـ TLA+، يستخدم لغة مواصفات شبيهة بلغة بايثون، ويحتوي على نمذجة سلوكية مثل TLA+ ونمذجة احتمالية مثل PRISM
• أداة التحقق من مستوى كود ISP لبرامج MPI
• جافا باثفايندر : أداة مفتوحة المصدر للتحقق من نماذج برامج جافا
• Libdmc : إطار عمل للتحقق من النماذج الموزعة
• مجموعة أدوات mCRL2 ، رخصة برنامج Boost ، مبنية على ACP
• NuSMV : مدقق نماذج رمزية جديد
• PAT : محاكي مُحسَّن، ومدقق نماذج، ومدقق تحسينات للأنظمة المتزامنة والأنظمة التي تعمل في الوقت الحقيقي
• بريزم : مدقق نماذج رمزية احتمالية
• روميو : بيئة أدوات متكاملة لنمذجة ومحاكاة والتحقق من أنظمة الوقت الحقيقي المصممة كشبكات بتري بارامترية وزمنية وشبكات بتري ساعة الإيقاف
• SPIN : أداة عامة للتحقق من صحة نماذج البرمجيات الموزعة بطريقة دقيقة وآلية في الغالب
• ستورم : ^{[ 22 ]} مدقق نماذج للأنظمة الاحتمالية.
• TAPAs : أداة لتحليل جبر العمليات
• TAPAAL : بيئة أدوات متكاملة لنمذجة شبكات بتري ذات الأقواس الموقوتة والتحقق من صحتها والتحقق منها
• مدقق نموذج TLA+ من تصميم ليزلي لامبورت
• UPPAAL : بيئة أدوات متكاملة لنمذجة أنظمة الوقت الحقيقي والتحقق من صحتها والتحقق منها، والتي يتم نمذجتها كشبكات من الأتمتة الموقوتة
• Zing ^{[ 23 ]} – أداة تجريبية من مايكروسوفت للتحقق من صحة نماذج حالة البرمجيات على مستويات مختلفة: أوصاف البروتوكولات عالية المستوى، ومواصفات سير العمل، وخدمات الويب، وبرامج تشغيل الأجهزة، والبروتوكولات في صميم نظام التشغيل. يُستخدم Zing حاليًا لتطوير برامج تشغيل لنظام ويندوز.