मॉडल जाँच उपकरणों की सूची

सीसीयह आलेख मॉडल जांच उपकरणों को सूचीबद्ध करता है और प्रत्येक की कार्यक्षमता का अवलोकन देता है।

कुछ मॉडल जांच उपकरणों का अवलोकन

निम्न सूची में मॉडल चेकर्स सम्मिलित होते हैं जिनके पास निम्नलिखित बिन्दु होते हैं

वेब साइट जिसके द्वारा इसे डाउनलोड किया जा सकता है,
घोषित लाइसेंस,
संग्रहीत साहित्य में प्रकाशित विवरण, और
विकिपीडिया लेख इसका वर्णन करता है।

नीचे दी गई सूची में, निम्नलिखित संक्षेपों का उपयोग किया गया है:

समानताएं:
- एसबी: शक्तिशाली बिसिमुलेशन
- पीबी: कमजोर बिसिमुलेशन
- बीबी: ब्रांचिंग बिसिमुलेशन
- एसटीई: मजबूत ट्रेस तुल्यता
- डब्ल्यूटीई: कमजोर ट्रेस समानता
- आई: मई तुल्यता
- एमई: समानता होनी चाहिए
- ओई: ऑब्जर्वेशनल इक्विलेंस
- एसई: सुरक्षा तुल्यता
- टी*ई: टाऊ*.ए तुल्यता
सॉफ़्टवेयर लाइसेंस:
- एफयूएससी: विशिष्ट प्रावधानों के अनुसार नि: शुल्क (उदाहरण के लिए, शिक्षाविदों के लिए मुफ्त)

नाम	प्रारूप की जाँच			बराबरी की जाँच		जीयूआई			उपलब्धता
	प्लेन, प्रोबैबिलिस्टिक, स्टोकैस्टिक, ...	माॅडलिंग भाषा	प्रापर्टीज भाषा	बराबरी का सहयोग	काउंटर जनरेशन का उदाहरण	जीयूआई	ग्राफिकल स्पेसिफिकेशन	काउंटर प्रदर्शन का उदाहरण	साॅफ्टवेयर लाइसेंस	उपयोगी प्रोग्रामिंग भाषा	प्लैटफाॅर्म, ओएस
ब्लास्ट	कोड एनालिसिस	सी	माॅनीटर आटोमेटा		Yes	No	No	No	Free	ओ कैमल	विंडोज, यूनिक्स रिलेटेड
सीए़डीपी	प्लेन और प्रोबैबिलिस्टिक	लोटोस, एफसी2, एफएसपी, एलएनटी	एएफएमसी, एमसीएल, एक्सटीएल	एसबी, डब्ल्यूबी, बीबी, OE, एसटीई, डब्ल्यूटीई, SE, tau*E	Yes	Yes	No	Yes	FUSC	सी, बाॅउर्न शेल, टीसीएल/टीके, लोटोस, एलएनटी	मैक ओएस, लाइनेक्स, सोलैरिस, विंडोज
सीपीए जाँच	कोड एनालिसिस	सी	माॅनीटर आटोमेटा		Yes	Yes	No	Yes	Free	जावा	अन्य
ड्रीम	रियल टाईम	सी++, टाइम्ड आटोमेटा	माॅनीटर आटोमेटा		Yes	No	No	No	Free	सी++	विंडोज, यूनिक्स रिलेटेड
जावा पाथफाइंडर	प्लेन और टाइम्ड	जावा	अज्ञात		No	Yes	No	No	Open Source Agreement	जावा	मैक ओएस, विंडोज, लाइनेक्स
Murφ (मर्फी)	प्लेन	Murφ	इनवैरियेंट, एसर्सन्स		Yes	No	No	No	Free	सी++	लाइनेक्स
एनयू एसएमवी	प्लेन	एसएमवी इनपुट भाषा	सीटीएल, एलटीएल, पीएसएल		Yes	No	No	No	Free	सी	यूनिक्स, विंडोज, मैक ओएस
पीएटी	प्लेन, रियल टाईम, प्रोबैबिलिस्टिक	सीएसपी#, टाइम्ड सीएसपी, प्रोबैबिलिस्टिक सीएसपी	एलटीएल, एसर्सन्स		Yes	Yes	Yes	Yes	Free	सी #	विंडोज, others with Mono
प्रिज्म	प्रोबैबिलिस्टिक	पीईपीए, प्रिज्म भाषा, प्लेन एमसी	सीएसएल, पीएलटीएल, पीसीटीएल		No	Yes	No	No	Free	सी++, जावा	विंडोज, लाइनेक्स, मैक ओएस
स्पिन	प्लेन	प्रोमेला	एलटीएल		Yes	Yes	No	Yes	FUSC	सी, सी++	विंडोज, यूनिक्स रिलेटेड
टापाल	रियल टाईम	टाइम्ड-आर्क पेटरी नेट्स, आयु इनवैरियेंट, इनिहिबिटर आर्क्स, ट्रांसपोर्ट आर्क्स	टीसीटीएल सबसेट		No	Yes	Yes	Yes	Free	सी++, जावा	मैक ओएस, विंडोज, लाइनेक्स
टीएपीए	प्लेन	सीसीएसपी	सीटीएल, μ-कैल्कुलस	एसबी, डब्ल्यूबी, बीबी, एसटीई, डब्ल्यूटीई, एमई, एमई, ओई	Yes	Yes	Yes	Yes	Free	जावा	विंडोज, मैक ओएस, यूनिक्स रिलेटेड
यूप्पाल	रियल टाईम	टाइम्ड आटोमेटा, सी सबसेट	टीसीटीएल सबसेट		Yes	Yes	Yes	Yes	FUSC	सी++, जावा	मैक ओएस, विंडोज, लाइनेक्स
रोमियो	रियल टाईम	टाइम पेट्री नेट्स, स्टाॅपवाच पैरामेट्रिक पेट्री नेट्स	टीसीटीएल सबसेट		Yes	Yes	Yes	No	Free	सी++, टीसीएल/टीके	मैक ओएस, विंडोज, लाइनेक्स
टीएलए+ माॅडल जांच (टीएलसी)	प्लेन	टीएलए+, प्लस कैल्कुलेशन	टीएलए		Yes	Yes	Yes	No	Free	जावा	मैक ओएस, विंडोज, लाइनेक्स

मॉडलिंग भाषाएँ

सीसीएसपी: कम्यूनिकेटिंग अनुक्रमिक प्रक्रियाओं के कुछ ऑपरेटरों को सम्मिलित करके संचार प्रणालियों के कैलकुलस से प्राप्त प्रक्रिया को फंक्शन के द्वारा प्रदर्शित करता हैं। इसे ओल्डराॅग और वैन ग्लैबीक/वैंडरजर द्वारा परिभाषित किया गया है।^[1]^[2]
अनुक्रमिक प्रक्रियाओं का संचार करना: अनुक्रमिक प्रक्रियाओं का संचार करना; समवर्ती प्रणालियों में संचरण के पैटर्न का वर्णन करने के लिए औपचारिक भाषा के रूप में उपयोग किया जाता हैं। एफडीआर2 सीएसपी के लिए परिशोधन जाँच उपकरण है, जो संगतता के लिए दो मॉडलों की तुलना करता है।
डीवीई इनपुट भाषा: प्रणाली को विस्तारित परिमित स्थिति मशीनों के नेटवर्क के रूप में वर्णित किया गया है जो साझा वैरियेबल और असंबद्ध चैनलों के माध्यम से संचार करती है। इस प्रकार बफ़र किए गए चैनलों के लिए और उचित प्राप्त किए बिना प्राप्त होने वाले संदेश के प्रकार की जाँच के लिए समर्थन सम्मिलित नहीं है।
एफसी2: (सामान्य प्रारूप वी2) ऑटोमेटा के सिंक्रनाइज़ (श्रेणीबद्ध) नेटवर्क के लिए मशीन-स्तर ASCII प्रतिनिधित्व करता हैं। एस्प्रिट बेसिक रिसर्च एक्शन कॉनसुर, 1992 द्वारा परिभाषित किया गया हैं। जिसे मुख्य रूप से प्रक्रिया बीजगणित के क्षेत्र में कई सत्यापन उपकरणों द्वारा इनपुट और विनिमय प्रारूप के रूप में उपयोग किया जाता है।
एफएसपी: इंपीरियल कॉलेज में परिभाषित परिमित स्थिति प्रक्रिया भाषा का उदाहरण हैं।
जावा (प्रोग्रामिंग भाषा): वस्तु-उन्मुख प्रोग्रामिंग भाषा का उदाहरण हैं।
एलएनटी: लोटोस न्यू टेक्नोलॉजी; प्रक्रिया गणना, कार्यात्मक प्रोग्रामिंग भाषाओं और अनिवार्य प्रोग्रामिंग भाषाओं से प्रेरित विशिष्ट भाषा; एलएनटी को टेम्पोरल ऑर्डरिंग स्पेसिफिकेशन की भाषा और ई-लोटोस के आधुनिक प्रतिस्थापन के रूप में डिज़ाइन किया गया था।
टेम्पोरल ऑर्डरिंग विशिष्टता की भाषा: टेम्पोरल ऑर्डरिंग विशिष्टता की भाषा (आईएसओ मानक 8807); आईएसओ ओएसआई मानकों में प्रोटोकॉल विनिर्देश के लिए प्रयुक्त अस्थायी आदेश के आधार पर औपचारिक विनिर्देश भाषा के रूप में उपयोग किया जाता हैं।
Murφ: वैश्विक चरों के माध्यम से किए गए सभी सिंक्रनाइज़ेशन और संचार के साथ संरक्षित आदेश और अतुल्यकालिक, संगामिति का इंटरलीविंग मॉडल का उदाहरण हैं।
कागज़ : प्रदर्शन मूल्यांकन प्रक्रिया बीजगणित; यह स्टोकेस्टिक प्रक्रिया बीजगणित है जिसे मॉडलिंग कंप्यूटर और संचार प्रणालियों के लिए डिज़ाइन किया गया है।
प्लेन एमसी: MRएमसी और प्रिज्म में उपयोग किए जाने वाले सरल टेक्स्ट-फ़ाइल स्वरूप हैं।
प्रोमेला: प्रक्रिया या प्रोटोकॉल मेटा भाषा; यह सत्यापन मॉडलिंग भाषा है। भाषा मॉडल के लिए समवर्ती प्रक्रियाओं के गतिशील निर्माण की अनुमति देती है, उदाहरण के लिए, वितरित सिस्टम इत्यादि।
टीएलए+: सामान्य-उद्देश्य विनिर्देशन भाषा, क्रियाओं के टेम्पोरल लॉजिक पर आधारित, मूल रूप से वितरित और समवर्ती प्रणालियों के लिए उपयोग की जाती है। विनिर्देशों और उनके गुणों के लिए भाषा समान है।

प्रापर्टीज भाषा

एएफएमसी: अल्टरनेशन-फ्री मोडल μ-कैलकुलस का उदाहरण हैं।
अभिकथन (कंप्यूटिंग): अनिवार्य अभिकथन कथन का उदाहरण हैं।
सीएसएल: कंटीन्यूअस स्टोकेस्टिक लॉजिक, निरंतर-टाइम मार्कोव प्रोसेस के बिसिमुलेशन की विशेषता बताता है।
सीएसआरएल: कंटीन्यूअस स्टोकेस्टिक रिवॉर्ड लॉजिक; इनाम संरचना (तथाकथित मार्कोव इनाम मॉडल) के साथ विस्तारित CTएमसीs पर उपायों को निर्दिष्ट करने के लिए तर्क।
संगणना वृक्ष तर्क : कम्प्यूटेशन ट्री लॉजिक; ब्रांचिंग-टाइम लॉजिक, जिसका अर्थ है कि इसका समय का मॉडल पेड़ जैसी संरचना है जिसमें भविष्य निर्धारित नहीं होता है; भविष्य में अलग-अलग मार्ग हैं, जिनमें से कोई वास्तविक मार्ग हो सकता है जिसे साकार किया जा सकता है।
इनवेरिएंट (गणित)#कंप्यूटर विज्ञान में इनवेरिएंट: सिस्टम स्थिति पर भविष्यवाणी करता है।
रैखिक लौकिक तर्क: रैखिक लौकिक तर्क; समय की चर्चा करते हुए तौर-तरीकों के साथ मोडल टेम्पोरल लॉजिक।
एमसीएल: मॉडल चेकिंग लैंग्वेज; अल्टरनेशन-फ्री मोडल μ-कैलकुलस को उपयोगकर्ता के अनुकूल रेगुलर एक्सप्रेशन और वैल्यू-पासिंग कंस्ट्रक्शन के साथ विस्तारित किया गया; कम्प्यूटेशन ट्री लॉजिक और लीनियर टेम्पोरल लॉजिक को समाहित करता है।
एमसीआरएल2 म्यू-कैलकुलस: कोज़ेन का प्रस्तावात्मक मोडल μ-कैलकुलस (परमाणु प्रस्तावों को छोड़कर), इसके साथ विस्तारित: डेटा-निर्भर प्रक्रियाएं, डेटा प्रकारों पर मात्रा का ठहराव, बहु-क्रियाएं, समय और नियमित सूत्र का उदाहरण हैं।
संभाव्य सीटीएल: संभाव्य संगणना ट्री लॉजिक; सीटीएल का विस्तार जो वर्णित गुणों की संभाव्य मात्रा का ठहराव के लिए अनुमति देता है।
पीएलटीएल: संभाव्य रैखिक लौकिक तर्क का उदाहरण हैं।
पीआरसीटीएल: प्रोबेबिलिस्टिक रिवॉर्ड कंप्यूटेशन ट्री लॉजिक; यह रिवॉर्ड-बाउंड प्रॉपर्टी के साथ प्रोबेबिलिस्टिक सीटीएल का विस्तार करता है।
संपत्ति विशिष्टता भाषा: संपत्ति विशिष्टता भाषा का उदाहरण हैं।
SVA: SyएसटीईmVerilog मानक अभिकथन भाषा उपसमुच्चय, IEEE 1800 के रूप में मानकीकृत किया जाता हैं।
एक्सटीएल: एक्सटेंडेड टेम्पोरल लैंग्वेज; क्रिया-आधारित, स्पष्ट-स्थिति, मूल्य-पास करने वाले मॉडल चेकर्स को त्वरित रूप से लागू करने के लिए डोमेन-विशिष्ट भाषा का उदाहरण हैं।

मॉडल जाँच उपकरणों की तुलना

वैज्ञानिक प्रकाशन

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

1999 में, जूडी रोमिजन ने उपभोक्ता इलेक्ट्रॉनिक्स के लिए एचएवीआई इंटरऑपरेबिलिटी ऑडियो-वीडियो प्रोटोकॉल पर दो मॉडल चेकर्स (वितरित प्रक्रियाओं का निर्माण और विश्लेषण और स्पिन मॉडल चेकर) की तुलना की जाती हैं।^[3]
2003 में, यीफी डाॅंग. इयाक्युन डू, गिरार्ड जे. हाॅल्जमैन्न, और स्काॅट ए. स्मोल्का ने संचार प्रोटोकॉल, जीएनयू i- पर चार मॉडल चेकर्स (अर्थात्: काॅस्पैन, मर्फी, स्पिन मॉडल चेकर, और Xएमसी) की तुलना प्रकाशित का व्यावहारिक रूप हैं।^[4]
2005 में, ऐलेना एम. बोर्टनिक, निकोला ट्रक्का, एंटन विज, बास लुटिक, जे.एम. वैन डी मोर्टेल-फ्रॉन्ज़ाक, जोस सी.एम. बैटेन, वान फोकिंक, और जे.ई. रूडा ने चार मॉडल चेकर्स की तुलना प्रकाशित की (अर्थात्: वितरित का निर्माण और विश्लेषण) प्रक्रियाओं, एमयूसीआरएल, स्पिन मॉडल चेकर, और उप्पल मॉडल चेकर) औद्योगिक निर्माण प्रणाली, घूर्णन ड्रिलिंग मशीन पर किया जाता हैं।^[5]
2018 में, एफ. मैज्जैन्टी और ए. फरारी ने दस मॉडल चेकर्स की तुलना प्रकाशित की (अर्थात्: वितरित प्रक्रियाओं का निर्माण और विश्लेषण, सीपीएन टूल्स, एफडीआर4, न्यू एसएमवी/न्यूएक्सएमवी, एमसीआरएल2, प्रौब, स्पिन मॉडल चेकर, टीएलए+, यूएमसी, और उप्पल मॉडल चेकर) ट्रेन पर्यवेक्षण समस्या पर, भाषाओं की उपयोगकर्ता-मित्रता और उपकरणों के प्रदर्शन दोनों को ध्यान में रखते हुए करता हैं।^[6]

अंतर्राष्ट्रीय सॉफ्टवेयर प्रतियोगिताएं

2007 से, हार्डवेयर मॉडल जाँच प्रतियोगिता (एचडब्ल्यूएमसीसी) हार्डवेयर डिज़ाइन की ओर उन्मुख मॉडल जाँच उपकरणों के प्रदर्शन की तुलना करती है।
2011 से, मॉडल जाँच प्रतियोगिता (एमसीसी) अत्यधिक समवर्ती प्रणालियों का विश्लेषण करने के लिए डिज़ाइन किए गए मॉडल जाँच उपकरणों के प्रदर्शन की तुलना करती है।

यह भी देखें

एल्टारिका

संदर्भ

↑ E.R. Olderog: Operational Petri net semantics for CCSP
↑ Rob van Glabbeek, Frits Vaandrager: Bundle Event Structures and CCSP
↑ Romijn, Judi (June 1999). एक HAVi नेता चुनाव प्रोटोकॉल की जाँच करने वाला मॉडल (Technical report). Amsterdam: CWI. SEN-R9915. Archived from the original on 2019-09-11. Retrieved 2018-06-14.
↑ Dong, Yifei; Du, Xiaoqun; Holzmann, Gerard; Smolka, Scott (2003). "Fighting Livelock in the GNU i-Protocol: A Case Study in Explicit-State Model Checking". Software Tool for Technology Transfer. 4 (4): 505–528.
↑ Bortnik, Elena M.; Trcka, Nikola; Wijs, Anton; Luttik, Bas; van de Mortel-Fronczak, J. M.; Baeten, Jos C. M.; Fokkink, Wan; Rooda, J. E. (2005). "स्पिन, सीएडीपी और उप्पल का उपयोग करके टर्नटेबल सिस्टम के ची मॉडल का विश्लेषण" (PDF). Journal of Logical and Algebraic Methods in Programming. 65 (2): 51–104. doi:10.1016/j.jlap.2005.05.001. Archived (PDF) from the original on 2021-01-27. Retrieved 2018-05-25.
↑ Mazzanti, Franco; Ferrari, Alessio (2018). "Ten Diverse Formal Models for a CBTC Automatic Train Supervision System". Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation (MARS/VPT’18), Thessaloniki, Greece. Electronic Proceedings in Theoretical Computer Science. Vol. 268. pp. 104–149. arXiv:1803.10324v1. doi:10.4204/EPTCS.268.4.

बाहरी संबंध

Common benchmarks

एमसीC (models of the Model Checking Contest): a collection of hundreds of Petri nets originating from mअन्य academic and industrial case studies.
VLTS (Very Large Transition Syएसटीईms): a collection of Labelled Transition Syएसटीईms of increasing sizes, used in mअन्य scientific publications.

[CCSP1-1] E.R. Olderog: Operational Petri net semantics for CCSP

[CCSP2-2] Rob van Glabbeek, Frits Vaandrager: Bundle Event Structures and CCSP

[3] Romijn, Judi (June 1999). एक HAVi नेता चुनाव प्रोटोकॉल की जाँच करने वाला मॉडल (Technical report). Amsterdam: CWI. SEN-R9915. Archived from the original on 2019-09-11. Retrieved 2018-06-14.

[4] Dong, Yifei; Du, Xiaoqun; Holzmann, Gerard; Smolka, Scott (2003). "Fighting Livelock in the GNU i-Protocol: A Case Study in Explicit-State Model Checking". Software Tool for Technology Transfer. 4 (4): 505–528.

[5] Bortnik, Elena M.; Trcka, Nikola; Wijs, Anton; Luttik, Bas; van de Mortel-Fronczak, J. M.; Baeten, Jos C. M.; Fokkink, Wan; Rooda, J. E. (2005). "स्पिन, सीएडीपी और उप्पल का उपयोग करके टर्नटेबल सिस्टम के ची मॉडल का विश्लेषण" (PDF). Journal of Logical and Algebraic Methods in Programming. 65 (2): 51–104. doi:10.1016/j.jlap.2005.05.001. Archived (PDF) from the original on 2021-01-27. Retrieved 2018-05-25.

[6] Mazzanti, Franco; Ferrari, Alessio (2018). "Ten Diverse Formal Models for a CBTC Automatic Train Supervision System". Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation (MARS/VPT’18), Thessaloniki, Greece. Electronic Proceedings in Theoretical Computer Science. Vol. 268. pp. 104–149. arXiv:1803.10324v1. doi:10.4204/EPTCS.268.4.

[1]

[2]

[3]

[4]

[5]

[6]