مبادئ التحقق من النماذج

كتاب "مبادئ التحقق من النماذج" هو كتاب دراسي حول التحقق من النماذج ، وهو مجال من علوم الحاسوب يُعنى بأتمتة عملية تحديد ما إذا كانت الآلة تفي بمتطلبات المواصفات. وقد ألّفه كريستيل باير وجوست بيتر كاتوين ، ونُشر عام 2008 من قِبل مطبعة معهد ماساتشوستس للتكنولوجيا .

يُقدّم الفصل الأول والمقدمة لمحة عامة عن مجال التحقق من النماذج : حيث يُمكن تحليل نموذج آلة أو عملية للتأكد من استيفائه للخصائص المطلوبة. على سبيل المثال، قد تُحقق آلة البيع خاصية "لا يُمكن أن يقل الرصيد عن 0.00 يورو". وقد تُطبّق لعبة فيديو قاعدة "إذا لم يتبقَّ للاعب أي أرواح، تنتهي اللعبة بخسارة". يُمكن نمذجة كلٍّ من آلة البيع ولعبة الفيديو كنظام انتقالي . التحقق من النماذج هو عملية وصف هذه المتطلبات بلغة رياضية، وأتمتة إثباتات استيفاء النموذج لهذه المتطلبات، أو اكتشاف الأمثلة المضادة في حال وجود خلل في النموذج.

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

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

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

يستكشف الفصلان الخامس والسادس منطق الزمن الخطي (LTL) ومنطق شجرة الحساب (CTL)، وهما فئتان من الصيغ التي تعبر عن الخصائص. يشفر منطق الزمن الخطي متطلبات المسارات عبر النظام، مثل "يمر كل لاعب في لعبة مونوبولي بخانة 'انطلاق' عددًا لا نهائيًا من المرات"؛ بينما يشفر منطق شجرة الحساب متطلبات الحالات في النظام، مثل "من أي موقع، يمكن لجميع اللاعبين في النهاية الوصول إلى خانة 'انطلاق'". كما تُعرَّف صيغ CTL* ، التي تجمع بين هذين النوعين من القواعد النحوية. وتُقدَّم خوارزميات للتحقق من صحة الصيغ في هذين المنطقين.

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

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

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

في عام 2014، كان الكتاب واحداً من أكثر خمسة نصوص أكاديمية استشهاداً بها وفقاً لمؤشر الاستشهاد بالكتب (BKCI). ^{[ 3 ]}

• لانج، مارتن (2010)، ماث ساينت ، MR 2493187 {{citation}}: CS1 maint: untitled periodical ( link )

• الموقع الرسمي