Libdmc

الموسوعة الحرة

Libdmc [ 1 ] [ 2 ] هي مكتبة مصممة في مختبر LIP6 [ 3 ] . هدفها تسهيل توزيع أدوات التحقق من النماذج الحالية . كما صُممت لتوفير واجهات عامة للغاية، دون المساس بالأداء، بفضل لغة C++ .

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

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

مراجع

  1. ↑ هامز، ألكسندر؛ كوردون، فابريس؛ تيري-ميغ، يان (2007). "IibDMC: مكتبة لتشغيل التحقق الفعال من النماذج الموزعة". ندوة IEEE الدولية للمعالجة المتوازية والموزعة لعام 2007. الصفحات 1-8 . doi : 10.1109/IPDPS.2007.370647 . ISBN  978-1-4244-0909-9. S2CID 12586847 . 
  2. ↑ هامز، ألكسندر؛ كوردون، فابريس؛ تييري-ميغ، يان؛ ليجون-أوبري، فابريس (2007). "DMCG: مدقق نماذج رمزية موزعة قائم على GreatSPN". شبكات بيتري ونماذج أخرى للتزامن - ICATPN 2007. سلسلة محاضرات في علوم الحاسوب. المجلد 4546. الصفحات 495-504 . doi : 10.1007/978-3-540-73094-1_29 . ISBN   978-3-540-73093-4.
  3. ↑ الصفحة الرئيسية LIP6