Murφ
मर्फि (/m. fi/, मर्फि भी लिखा जाता है) स्टैनफोर्ड विश्वविद्यालय में विकसित एक स्पष्ट-राज्य मॉडल जाँचक है, और व्यापक रूप से कैश-सुसंगतता प्रोटोकॉल के औपचारिक सत्यापन के लिए उपयोग किया जाता है। डेविड डिल द्वारा एक पेपर में इतिहास मुर्फी के प्रारंभिक इतिहास का वर्णन किया गया है। मुर्फी का पहला संस्करण 1990 और 1991 में स्टैनफोर्ड विश्वविद्यालय में प्रो. डेविड डिल और उनके स्नातक छात्रों एंड्रियास ड्रेक्सलर, एलन हू और हान यांग द्वारा डिजाइन किया गया था, और मुख्य रूप से एंड्रियास ड्रेक्सलर द्वारा लागू किया गया था। डेविड डिल, एलन हू, सी. नॉरिस आईपी, राल्फ मेल्टन, सेउंगजून पार्क और हान यांग द्वारा विनिर्देशन भाषा को व्यापक रूप से संशोधित और विस्तारित किया गया था। राल्फ मेल्टन ने 1992 की गर्मियों और शरद ऋतु के दौरान नए संस्करण को लागू किया। सेउंगजून पार्क ने जीवंतता जाँच और निष्पक्षता बाधाओं को जोड़ा, लेकिन क्योंकि जीवंतता सत्यापन के लिए एल्गोरिथ्म महत्वपूर्ण अनुकूलन, विशेष रूप से समरूपता में कमी के साथ संघर्ष करता है, इसलिए बाद के संस्करणों में जीवंतता सत्यापन को छोड़ दिया गया। सी. नॉरिस आईपी ने प्रतिवर्ती नियमों और पुनरावृत्ति निर्माताओं (जो रिलीज 3.1 में शामिल नहीं हैं) को लागू किया, और समरूपता और बहु-समुच्चय कटौती (जो हैं) को जोड़ा। उलरिच स्टर्न ने हैश संपीड़न को लागू किया, डिस्क के उपयोग में सुधार किया और समानांतर मुरफ़ को लागू किया। स्टैनफोर्ड से अंतिम रिलीज 1993 के नवंबर में 3.1 जारी की गई थी। मर्फि के कई व्युत्पन्न संस्करण तब से अन्य समूहों द्वारा बनाए गए हैं। विशेषताएँ मर्फ संकलक मर्फ विनिर्देशन भाषा में लिखे गए एक मॉडल को स्वीकार करता है और सी + + कोड आउटपुट करता है जो उस मॉडल के लिए एक सत्यापनकर्ता का गठन करता है। (अर्थात, सी + + कोड, जब निष्पादित किया जाता है, तो विनिर्देशन द्वारा वर्णित डिजाइन पर स्पष्ट-स्थिति मॉडल की जाँच करता है।) मुर्फी विनिर्देशन भाषा वैश्विक चरों के माध्यम से किए गए सभी समन्वय और संचार के साथ संरक्षित आदेशों और समवर्ती के एक अतुल्यकालिक, इंटरलीविंग मॉडल का उपयोग करती है। सत्यापनकर्ता मॉडल में निर्दिष्ट अपरिवर्तनीय और आंतरिक अभिकथनों के रूप में सुरक्षा गुणों की जांच करता है, और गतिरोध की जांच करता है। यह जीवंतता गुणों की जांच नहीं करता है, हालांकि मुर्फी रिलीज 2.7 एल ने सामान्य एल. टी. एल. जीवंतता गुणों के एक समूह के सत्यापन का समर्थन किया। भाषा और सत्यापनकर्ता कुछ प्रकार की समरूपता में कमी का समर्थन करते हैं। Murφ को मूल रूप से कैश-सुसंगतता प्रोटोकॉल को सत्यापित करने के लिए लागू किया गया था, लेकिन सुरक्षा प्रोटोकॉल के सत्यापन सहित अन्य समस्याओं पर भी लागू किया गया है। मरफी लाइसेंस एम. आई. टी. लाइसेंस के समान है। मुर्फी का उपयोग किसी भी उद्देश्य के लिए किया जा सकता है, प्रतिलिपि बनाई जा सकती है, संशोधित किया जा सकता है, बेचा जा सकता है और पुनर्वितरित किया जा सकता है, बशर्ते कॉपीराइट सूचना और लाइसेंस शामिल हों, स्टैनफोर्ड विश्वविद्यालय का नाम बिना अनुमति के विज्ञापन या प्रचार के लिए उपयोग नहीं किया जाता है, और संशोधित संस्करणों को बिना अनुमति के मुर्फी नहीं कहा जाता है। व्युत्पन्न स्टैनफोर्ड और अन्य जगहों पर मर्फि के कई व्युत्पन्न संस्करण बनाए गए हैं, जिनमें शामिल हैंः समानांतर मर्फि एडी-समानांतर और वितरित मर्फि। पी. आर. ई. एच. (समानांतर पहुँच)-एर्लांग में लागू समानांतर मॉडल जाँच। वितरित मर्फि पैरलल रैंडम-वॉक मर्फि पी. ए. एम.-प्रेडिकेट एब्स्ट्रैक्शन मर्फि पोएम-आंशिक-आदेश सक्षम मर्फि सी. मर्फि-कैचिंग मर्फि। एफ. एच. पी.-मर्फी-फाइनाइट होराइजन प्रोबेबिलिस्टिक मर्फी। एड्डी मर्फी-समानान्तर और वितरित, CMurphy पर आधारित, संदेश पारित करने के लिए MPI का उपयोग करते हुए। यूनिवर्सल प्लानर मर्फि-प्रक्रियाओं और घटनाओं के साथ रैखिक और अरैखिक निरंतर पी. डी. डी. एल. + मॉडल के लिए योजना और सार्वभौमिक योजना; प्रारंभिक शाब्दिक और समयबद्ध प्रारंभिक धाराप्रवाह भी। अफवाह मॉडल जाँच उपकरण की सूची भी देखें संदर्भ बाहरी लिंक मर्फि एनोटेटेड संदर्भ नियमावली, स्टैनफोर्ड सुरक्षा प्रयोगशाला, सुरक्षा प्रोटोकॉल के लिए मॉडल जाँच विधि यूटा विश्वविद्यालय, कम्प्यूटिंग स्कूल-मर्फ के संस्करणों का एक संग्रह। मॉडल जाँच सी + + में प्रोग्राम किए गए मुक्त सॉफ्टवेयर