ما هي تجربتك مع التحقق من نموذج البرنامج؟[مغلق]

Question

• ما هي أنواع التطبيقات التي استخدمتها فحص النموذج ل؟
• ما هي أداة التحقق من النموذج التي استخدمتها؟
• كيف تلخص تجربتك مع هذه التقنية، وتحديداً في تقييم فعاليتها في تقديم برامج ذات جودة أعلى؟

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

Answer 1

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

على الرغم من أن هذه الأدوات كانت ممتعة في الاستخدام، إلا أنني أعتقد أنها تتألق حقًا عندما تجمعها مع شيء يفرض قيودًا على برنامجك ديناميكيًا (بحيث يكون من الأسهل قليلًا التحقق من الأشياء "المفيدة" في برنامجك).انتهى بنا الأمر بأخذ إطار عمل Spring WebFlow, ، والذي يستخدم XML لكتابة ملف يشبه جهاز الحالة الذي يحدد صفحات الويب التي يمكنها الانتقال إلى الصفحات الأخرى، واستخدام SMV لتتمكن من إجراء التحقق على التطبيقات المذكورة (المكونات وقح هنا).

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

Answer 2

لقد استخدمنا العديد من أدوات التحقق النموذجية في التدريس، وتصميم الأنظمة، وتطوير الأنظمة.تتضمن مجموعة الأدوات الخاصة بنا SPIN، وUPPAL، وJava Pathfinder، وPVS، وBogor.لكل منها نقاط قوتها وضعفها.كلهم يجدون مشاكل في النماذج التي من المستحيل على البشر اكتشافها.وتختلف قابليتها للاستخدام، على الرغم من أن معظمها يعمل تلقائيًا بضغطة زر.

متى تستخدم مدقق النموذج؟أود أن أقول في أي وقت تصف فيه نموذجًا يجب أن يحتوي (أو لا يمتلك) خصائص معينة وهو أكبر من مجرد مجموعة من المفاهيم.أي شخص يعتقد أنه قادر على وصف وفهم أي شيء أكبر أو أكثر تعقيدًا فهو يخدع نفسه.

Answer 3

ما أنواع التطبيقات التي استخدمتها للتحقق من النماذج؟

استخدمنا مدقق نموذج Java Path Finder للتحقق من بعض الأمان (حالة الجمود، وحالة السباق) والخصائص الزمنية (باستخدام المنطق الزمني الخطي لتحديدها).وهو يدعم التأكيدات الكلاسيكية (مثل NotNull) على Java (الرمز الثانوي) - وهو مخصص للتحقق من طراز البرنامج.

ما هي أداة التحقق من النموذج التي استخدمتها؟

كنا جافا مسار مكتشف (للأغراض الأكاديمية).إنه برنامج مفتوح المصدر طورته وكالة ناسا في البداية.

كيف تلخص تجربتك مع هذه التقنية، وتحديداً في تقييم فعاليتها في تقديم برامج ذات جودة أعلى؟

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

Answer 4

لقد استخدمت SPIN للعثور على مشكلة التزامن في برنامج PLC.لقد وجدت حالة سباق غير متوقعة كان من الصعب جدًا العثور عليها عن طريق الفحص أو الاختبار.

بالمناسبة، هل يوجد كتاب "SPIN for Dummies"؟كان علي أن أتعلم ذلك من كتاب "The SPIN Model Checker" والعديد من البرامج التعليمية عبر الإنترنت.

Answer 5

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

استخدمنا جهازًا افتراضيًا للسير في كل مسار/حالة محتملة للبرنامج، باستخدام A* وبعض الأساليب الإرشادية، اعتمادًا على نوع الخطأ (حالة توقف تام، أخطاء الإدخال/الإخراج، ...)

كان مستوحى من جافا باثفايندر وعملت مع كود C++.(كل ما يمكن لدول مجلس التعاون الخليجي تجميعه)

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