مستكشف جافا

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

جافا باثفايندر (JPF) هو نظام للتحقق من برامج بايت كود جافا القابلة للتنفيذ . طُوّر JPF في مركز أبحاث ناسا أميس ، وأُتيح كمصدر مفتوح عام ٢٠٠٥. يُرجى عدم الخلط بين اختصار JPF ومشروع إطار عمل جافا الإضافي (Java Plugin Framework) غير ذي الصلة .

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

  • التحقق من نموذج التطبيقات الموزعة
  • التحقق من نماذج واجهات المستخدم
  • توليد حالات الاختبار عن طريق التنفيذ الرمزي
  • تفتيش البرنامج على مستوى منخفض
  • أدوات البرنامج ومراقبة وقت التشغيل

لا يمتلك JPF مفهومًا ثابتًا لفروع فضاء الحالة ويمكنه التعامل مع كل من البيانات وخيارات الجدولة.

قابلية التوسعة

JPF هو نظام مفتوح المصدر يمكن توسيعه بطرق متنوعة. أهم بنى التوسيع هي

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

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

القيود

انظر أيضاً

  • MoonWalker - مشابه لـ Java PathFinder، ولكنه مخصص لبرامج .NET بدلاً من برامج Java

مراجع

  • ويليم فيسر، كورينا س. باساريانو ، سرفراز خورشيد. توليد مدخلات الاختبار باستخدام جافا باث فايندر. في: جورج س. أفرونين، جريج روثرميل (محرران): وقائع ندوة ACM/SIGSOFT الدولية لاختبار البرمجيات وتحليلها 2004. مطبعة ACM، 2004. ISBN 1-58113-820-2.
  • Willem Visser, Klaus Havelund, Guillaume Brat, Seungjoon Park, Flavio Lerda, Model Checking Programs, Automated Software Engineering 10(2), 2003.
  • كلاوس هافيلوند، ويليم فيسر، التحقق من نموذج البرنامج كاتجاه جديد، STTT 4(1)، 2002.
  • كلاوس هافيلوند، توماس بريسبورغر، التحقق من نماذج برامج جافا باستخدام جافا باثفايندر، STTT 2(4)، 2000.