اهتمام بحثي

التحقق الشكلي

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

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