सॉफ़्टवेयर मॉडल की जांच के साथ आपका अनुभव क्या है?

Question

• आपने किस प्रकार के अनुप्रयोगों का उपयोग model checking के लिए किया है?
• आप किस मॉडल जांच उपकरण का उपयोग करते थे?
• आप अपने अनुभव w/तकनीक को संक्षेप में कैसे सारांशित करेंगे, विशेष रूप से उच्च गुणवत्ता वाले सॉफ़्टवेयर देने में इसकी प्रभावशीलता का मूल्यांकन करने में?

अपनी पढ़ाई के दौरान, मैं Spin उपयोग करने के लिए एक मौका था, और यह कितना वास्तविक मॉडल की जाँच चल रहा है करने के लिए और कितना मूल्य संगठनों को इससे बाहर हो रही है के रूप में मेरी जिज्ञासा जगाया। मेरे काम के अनुभव में, मैंने व्यावसायिक अनुप्रयोगों पर काम किया है, जहां तर्क (औपचारिक रूप से) तर्क के औपचारिक सत्यापन को लागू करने पर कोई विचार नहीं है। मैं वास्तव में विषय पर एसओ लोगों मॉडल जांच अनुभव और विचारों के बारे में जानना चाहता हूं। मॉडल जांच कभी भी व्यापक रूप से उपयोग किए जाने वाले विकासशील अभ्यास बन जाएगी जो हमारे टूलकिट में होनी चाहिए?

Answer 1

मैंने मॉडल जांच पर एक कक्षा समाप्त की और हमारे द्वारा उपयोग किए जाने वाले बड़े उपकरण Spin और SMV थे। हमने सामान्य सिंक्रनाइज़ेशन समस्याओं पर गुणों की जांच करने के लिए उनका उपयोग समाप्त कर दिया, और मैंने एसएमवी को उपयोग करने के लिए थोड़ा सा आसान पाया।

हालांकि ये उपकरण उपयोग करने के लिए मजेदार थे, मुझे लगता है कि जब आप उन्हें अपने प्रोग्राम पर बाधाओं को गतिशील रूप से लागू करते हैं तो वे वास्तव में चमकते हैं (ताकि आपके प्रोग्राम के बारे में 'उपयोगी' चीजों को सत्यापित करना थोड़ा आसान हो)। हमने Spring WebFlow framework ले लिया, जो कि एक राज्य-मशीन जैसे फ़ाइल लिखने के लिए एक्सएमएल का उपयोग करता है जो निर्दिष्ट करता है कि कौन से वेब पेज अन्य लोगों में संक्रमण कर सकते हैं, और एसएमवी का उपयोग करके कहा गया अनुप्रयोगों पर सत्यापन करने में सक्षम होने के लिए (shameless plug here)।

अपने अंतिम प्रश्न का उत्तर देने के लिए, मुझे लगता है कि मॉडल जांच निश्चित रूप से उपयोगी है, लेकिन मैं एक तकनीक के रूप में यूनिट परीक्षण का उपयोग करने की दिशा में अधिक दुबला हूं जो मुझे अपना अंतिम उत्पाद देने के बारे में सहज महसूस करता है।

Answer 2

मैंने पीएलसी सॉफ़्टवेयर में एक समवर्ती समस्या खोजने के लिए स्पिन का उपयोग किया। इसे एक अप्रत्याशित दौड़ की स्थिति मिली जो निरीक्षण या परीक्षण द्वारा खोजना बहुत कठिन होता।

वैसे, क्या "डमीज़ के लिए स्पिन" पुस्तक है? मुझे इसे "स्पिन मॉडल चेकर" पुस्तक और विभिन्न ऑन-लाइन ट्यूटोरियल्स से सीखना पड़ा।

Answer 3

मैंने विश्वविद्यालय में अपने समय के दौरान उस विषय पर कुछ शोध किया है, State Exploring Assembly Model Checker का विस्तार किया है।

हम एक आभासी मशीन का इस्तेमाल किया और हर संभव पथ/प्रोग्राम की स्थिति चलने के लिए, एक * और कुछ अनुमानी का उपयोग कर, त्रुटि के प्रकार पर निर्भर (गतिरोध, आई/ओ त्रुटियों, ...)

यह Java Pathfinder से प्रेरित था और यह सी ++ कोड के साथ काम करता था। (सब कुछ जीसीसी संकलित कर सकता है)

लेकिन हमारे अनुभवों में जीयूआई से संबंधित समस्याओं के कारण, इस तरह की तकनीक जल्द ही व्यावसायिक अनुप्रयोगों में उपयोग नहीं की जाएगी, प्रारंभिक परीक्षण वातावरण और भारी हार्डवेयर आवश्यकताओं के निर्माण के लिए आवश्यक कार्य। (आपको विशाल राज्य स्थान की वजह से बहुत सी रैम और डिस्क स्पेस चाहिए)

Answer 4

हमने शिक्षण, सिस्टम डिज़ाइन और सिस्टम विकास में कई मॉडल चेकर्स का उपयोग किया है। हमारे टूलबॉक्स में स्पिन, यूपीपीएएल, जावा पाथफाइंडर, पीवीएस, और बोगोर शामिल हैं। प्रत्येक में इसकी ताकत और कमजोरियां होती हैं। सभी मॉडलों के साथ समस्याएं पाती हैं जो मनुष्यों के लिए खोजना असंभव है। उनकी उपयोगिता भिन्न होती है, हालांकि अधिकांश पुशबटन स्वचालित होते हैं।

मॉडल चेकर का उपयोग कब करें? मैं कहूंगा कि आप किसी भी समय ऐसे मॉडल का वर्णन कर रहे हैं जिसमें विशेष गुण होना चाहिए (या नहीं) और यह कुछ हद तक अवधारणाओं से बड़ा है। कोई भी जो सोचता है कि वे किसी भी बड़े या अधिक जटिल का वर्णन और समझ सकते हैं, वह खुद को मूर्ख बना रहा है।

Answer 5

आपने किस प्रकार के अनुप्रयोगों के लिए मॉडल जांच की है?

हम कुछ सुरक्षा (गतिरोध, रेस स्थिति) और लौकिक गुण (रैखिक लौकिक तर्क का उपयोग कर उन्हें निर्दिष्ट करने के लिए) को सत्यापित करने के जावा पथ खोजक मॉडल चेकर का इस्तेमाल किया। यह जावा (बाइटकोड) पर शास्त्रीय दावे (जैसे नोटनुल) का समर्थन करता है - यह प्रोग्राम मॉडल जांच के लिए है।

आप किस मॉडल जांच उपकरण का उपयोग करते थे?

हमने Java Path Finder (अकादमिक उद्देश्यों के लिए) का उपयोग किया। यह प्रारंभ में नासा द्वारा विकसित ओपन सोर्स सॉफ्टवेयर है।

आप अपने अनुभव w/तकनीक को संक्षेप में कैसे सारांशित करेंगे, विशेष रूप से उच्च गुणवत्ता वाले सॉफ्टवेयर देने में इसकी प्रभावशीलता का मूल्यांकन करने में?

प्रोग्राम मॉडल जांच में राज्य अंतरिक्ष विस्फोट (स्मृति & डिस्क उपयोग) के साथ एक बड़ी समस्या है। लेकिन समस्याओं को कम करने के लिए तकनीकों की एक विस्तृत विविधता है, आंशिक क्रम में कमी, अमूर्तता, समरूपता में कमी, इत्यादि