5

क्या कोई ऐसा उपकरण है जो मॉडल को बड़ी, असली दुनिया, ज्यादातर-सी ++, वितरित सिस्टम, जैसे केडीई की जांच कर सकता है?मॉडल के लिए उपकरण बड़े, वितरित सी ++ परियोजनाओं जैसे कि केडीई की जांच?

(केडीई इस अर्थ में एक वितरित प्रणाली है कि यह आईपीसी का उपयोग करता है, हालांकि आम तौर पर सभी प्रक्रियाएं एक ही मशीन पर होती हैं। हाँ, वैसे, यह "वितरित प्रणाली" का वैध उपयोग है - विकिपीडिया की जांच करें।)

उपकरण को इंट्राप्रोसेस घटनाओं और अंतर-प्रक्रिया संदेशों से निपटने में सक्षम होने की आवश्यकता होगी।

(मान लेते उपकरण सी ++ का समर्थन करता है, लेकिन अन्य सामग्री पर केडीई इस तरह के MOC के रूप में उपयोग करता है का समर्थन नहीं करता है, तो यह है कि, हम उस वैकल्पिक हल के लिए एक साथ कुछ हैक कर सकते हैं।)

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

+0

वहाँ बड़े * गैर * रियल-दुनिया के ज्यादातर सी ++ वितरण प्रणाली रहे हैं? :-) – Ken

+5

क्या आप मॉडल जांच द्वारा अपना मतलब समझ सकते हैं? –

+1

मुझे यकीन है कि उसका मतलब संपत्तियों के लिए राज्य-स्थान की जांच (http://en.wikipedia.org/wiki/Model_checking का कुछ विशिष्ट उदाहरण) है, और उसने हमें यह बताकर संकेत दिया है कि उसके पास संदेश का उपयोग करके एक वितरित प्रणाली है primitives, तो प्रक्रिया इंटरैक्शन द्वारा गठित राज्यों का एक अंतर्निहित सेट है। लेकिन विवरण मायने रखता है। –

उत्तर

5

आप स्पष्ट रूप से एक स्थिर विश्लेषण उपकरण है जो

  • पार्स सी ++ पैमाने
  • पर ब्याज
  • के कोड के टुकड़े का पता लगाने कर सकते हैं एक मॉडल चेकर करने के लिए एक मॉडल
  • पास उस मॉडल को निकालने के लिए देख रहे हैं
  • रिपोर्ट जो आपको

एक महत्वपूर्ण समस्या यह है कि सभी के पास एक अलग विचार है कि वे किस मॉडल को देखना चाहते हैं। वह अकेला संभवतः आप जो चाहते हैं उसे ढूंढने का मौका मारता है, क्योंकि प्रत्येक मॉडल निष्कर्षण उपकरण ने आम तौर पर एक मॉडल के रूप में कैप्चर करना चाहते हैं, और यह संभावना है कि यह से मेल खाता है जो आप चाहते हैं कि IMHO बंद हो शून्य करने के लिए।

आप विशेष रूप से क्या आप मॉडल बनाना चाहते हैं पर स्पष्ट नहीं हैं, लेकिन मुझे लगता है आप गतिरोध की तरह कुछ के लिए जाँच करने के लिए संचार पुरातन खोजने के लिए और प्रक्रिया बातचीत मॉडल बनाना चाहते हैं?

वाणिज्यिक स्थैतिक विश्लेषण उपकरण विक्रेता देखने के लिए एक तार्किक जगह की तरह लगते हैं, लेकिन मुझे नहीं लगता कि वे वहां हैं, फिर भी। Coverity सर्वश्रेष्ठ शर्त की तरह प्रतीत होता है, लेकिन ऐसा लगता है कि जावा थ्रेडिंग समस्याओं के लिए उनके पास केवल कुछ प्रकार का गतिशील विश्लेषण है।

यह पेपर ऐसा करने का दावा करता है, लेकिन मैंने किसी भी विवरण में नहीं देखा है: Compositional analysis of C/C++ programs with VeriSoft। संबंधित [PDF] Computer-Assisted Assume/Guarantee Reasoning with VeriSoft है। ऐसा लगता है कि आपको ब्याज के मॉडलिंग तत्वों को इंगित करने के लिए स्रोत कोड को हाथ-एनोटेट करना होगा। Verifysoft उपकरण खुद बेल लैब्स के मालिकाना प्रतीत होता है और संभवतः प्राप्त करना मुश्किल है।

इसी प्रकार यह एक: Distributed Verification of Multi-threaded C++ Programs

यह पेपर भी दिलचस्प दावों को बनाता है, लेकिन शीर्षक के बावजूद सी ++ को संसाधित नहीं करता है: Runtime Model Checking of Multithreaded C/C++ Programs

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

हमारे DMS Software Reengineering Toolkit अनुकूल उद्देश्य पैटर्न मिलान और तथ्य निष्कर्षण के साथ सामान्य उद्देश्य पार्सिंग प्रदान करता है, और इसमें मजबूत C++ Front End है जो सी ++ की कई बोलीभाषाओं को संभालता है। यह आपके द्वारा देखी जाने वाली मॉडल के अनुरूप तथ्यों को खोजने और निकालने के लिए कॉन्फ़िगर किया जा सकता है। लेकिन यह शेल्फ से यह नहीं करता है।

डीएमएस अपने सी फ्रंट एंड का उपयोग अत्यधिक बड़े अनुप्रयोगों (1 9, 000 संकलन इकाइयों!) को संसाधित करने के लिए किया गया है। सी ++ फ्रंट एंड का उपयोग बड़े पैमाने पर सी ++ परियोजनाओं पर क्रोध में किया जाता है लेकिन आम तौर पर उस पैमाने पर नहीं। डीएमएस की सामान्य क्षमता को देखते हुए, मुझे लगता है कि यह कोड के काफी बड़े हिस्से को संभालने में सक्षम है। YMMV।

1

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

आप रन टाइम पर "Daikon" उस पर कब्जा कथित अपरिवर्तनशीलताओं की तरह स्वत: अपरिवर्तनीय खोज उपकरणों का उपयोग करने की कोशिश कर सकते हैं। यदि आप खोजे गए आविष्कार (चर के समानता "ए == बी + 1" उदाहरण के लिए) समझाते हैं तो आप बाद में मान्य कर सकते हैं और फिर अपने कोड में स्थायी आवेषण डालें। इस तरह जब आपके परिवर्तन के परिणामस्वरूप आविष्कार का उल्लंघन किया जाता है तो आपको एक चेतावनी मिलेगी कि शायद आपने अपने बदलाव से कुछ तोड़ा। यह विधि परीक्षण और मैक्स जोड़ने के लिए पुनर्गठन या अपने कोड को बदलने से बचने में मदद करती है।

0

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

+0

यह उत्तर की तुलना में प्रश्न पर एक टिप्पणी के रूप में बेहतर होगा। मुझे खुशी है कि यह एक दृष्टिकोण है, लेकिन यह वास्तव में एक तरह से एक महंगी दृष्टिकोण है, और वैसे भी यह ठोस सवाल का जवाब नहीं है: जो उपकरण वास्तविक दुनिया उपयोग के इस प्रकार के लिए उचित होगा? –