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

From Vigyanwiki
Revision as of 23:09, 7 March 2023 by alpha>Ashirvad Verma

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

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

निम्न तालिका में मॉडल चेकर्स शामिल हैं जिनके पास है

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

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

  • समानताएं:
    • एसबी: मजबूत बिसिमुलेशन
    • पश्चिम बंगाल: कमजोर बिसिमुलेशन
    • बीबी: ब्रांचिंग बिसिमुलेशन
    • STE: मजबूत ट्रेस तुल्यता
    • डब्ल्यूटीई: कमजोर ट्रेस समानता
    • मैं: मई तुल्यता
    • ME: समानता होनी चाहिए
    • OE: ऑब्जर्वेशनल इक्विलेंस
    • एसई: सुरक्षा तुल्यता
    • t*E: tau*.a तुल्यता
  • सॉफ़्टवेयर लाइसेंस:
    • एफयूएससी: विशिष्ट शर्त के तहत नि: शुल्क (उदाहरण के लिए, शिक्षाविदों के लिए मुफ्त)
Name Model Checking Equivalence checking GUI Availability
Plain, Probabilistic, Stochastic, ... Modelling language Properties language Supported equivalences Counter example generation   GUI   Graphical Specification Counter example visualization Software license Programming language used Platform, OS
BLAST Code analysis C Monitor automata Yes No No No Free OCaml Windows, Unix related
CADP Plain and probabilistic LOTOS, FC2, FSP, LNT AFMC, MCL, XTL SB, WB, BB, OE, STE, WTE, SE, tau*E Yes Yes No Yes FUSC C, Bourne shell, Tcl/Tk, LOTOS, LNT macOS, Linux, Solaris, Windows
CPAchecker Code analysis C Monitor automata Yes Yes No Yes Free Java Any
DREAM Real-time C++, Timed automata Monitor automata Yes No No No Free C++ Windows, Unix related
Java Pathfinder Plain and timed Java unknown No Yes No No Open Source Agreement Java macOS, Windows, Linux
Murφ (Murphi) Plain Murφ Invariants, assertions Yes No No No Free C++ Linux
NuSMV Plain SMV input language CTL, LTL, PSL Yes No No No Free C Unix, Windows, macOS
PAT Plain, real-time, probabilistic CSP#, timed CSP, probabilistic CSP LTL, assertions Yes Yes Yes Yes Free C# Windows, others with Mono
PRISM Probabilistic PEPA, PRISM language, Plain MC CSL, PLTL, PCTL No Yes No No Free C++, Java Windows, Linux, macOS
SPIN Plain Promela LTL Yes Yes No Yes FUSC C, C++ Windows, Unix related
TAPAAL Real-time Timed-Arc Petri Nets, age invariants, inhibitor arcs, transport arcs TCTL subset No Yes Yes Yes Free C++, Java macOS, Windows, Linux
TAPAs Plain CCSP CTL, μ-calculus SB, WB, BB, STE, WTE, me, ME, OE Yes Yes Yes Yes Free Java Windows, macOS, Unix related
UPPAAL Real-time Timed automata, C subset TCTL subset Yes Yes Yes Yes FUSC C++, Java macOS, Windows, Linux
ROMEO Real-time Time Petri Nets, stopwatch parametric Petri nets TCTL subset Yes Yes Yes No Free C++, Tcl/Tk macOS, Windows, Linux
TLA+ Model Checker (TLC) Plain TLA+, PlusCal TLA Yes Yes Yes No Free Java macOS, Windows, Linux


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

  • CCSP: कम्यूनिकेटिंग अनुक्रमिक प्रक्रियाओं के कुछ ऑपरेटरों को शामिल करके संचार प्रणालियों के कैलकुलस से प्राप्त प्रक्रिया कलन। इसे Olderog द्वारा परिभाषित किया गया है[1] और वैन ग्लैबीक/वैंडरजर द्वारा।[2]
  • अनुक्रमिक प्रक्रियाओं का संचार करना: अनुक्रमिक प्रक्रियाओं का संचार करना; समवर्ती प्रणालियों में बातचीत के पैटर्न का वर्णन करने के लिए औपचारिक भाषा। FDR2 CSP के लिए परिशोधन जाँच उपकरण है, जो संगतता के लिए दो मॉडलों की तुलना करता है।
  • DVE इनपुट भाषा: प्रणाली को विस्तारित परिमित राज्य मशीनों के नेटवर्क के रूप में वर्णित किया गया है जो साझा चर और असंबद्ध चैनलों के माध्यम से संचार करती है। बफ़र किए गए चैनलों के लिए और उचित प्राप्त किए बिना प्राप्त होने वाले संदेश के प्रकार की जाँच के लिए समर्थन शामिल नहीं है।
  • FC2: (सामान्य प्रारूप V2) ऑटोमेटा के सिंक्रनाइज़ (श्रेणीबद्ध) नेटवर्क के लिए मशीन-स्तर ASCII प्रतिनिधित्व। एस्प्रिट बेसिक रिसर्च एक्शन कॉनसुर, 1992 द्वारा परिभाषित। मुख्य रूप से प्रक्रिया बीजगणित के क्षेत्र में कई सत्यापन उपकरणों द्वारा इनपुट और विनिमय प्रारूप के रूप में उपयोग किया जाता है।
  • FSP: इंपीरियल कॉलेज में परिभाषित परिमित राज्य प्रक्रिया भाषा।
  • जावा (प्रोग्रामिंग भाषा): वस्तु-उन्मुख प्रोग्रामिंग भाषा।
  • एलएनटी: लोटोस न्यू टेक्नोलॉजी; प्रक्रिया गणना, कार्यात्मक प्रोग्रामिंग भाषाओं और अनिवार्य प्रोग्रामिंग भाषाओं से प्रेरित विशिष्ट भाषा; LNT को टेम्पोरल ऑर्डरिंग स्पेसिफिकेशन की भाषा और E-LOTOS के आधुनिक प्रतिस्थापन के रूप में डिज़ाइन किया गया था।
  • टेम्पोरल ऑर्डरिंग विशिष्टता की भाषा: टेम्पोरल ऑर्डरिंग विशिष्टता की भाषा (आईएसओ मानक 8807); आईएसओ ओएसआई मानकों में प्रोटोकॉल विनिर्देश के लिए प्रयुक्त अस्थायी आदेश के आधार पर औपचारिक विनिर्देश भाषा।
  • Murφ: वैश्विक चरों के माध्यम से किए गए सभी सिंक्रनाइज़ेशन और संचार के साथ संरक्षित आदेश और अतुल्यकालिक, संगामिति का इंटरलीविंग मॉडल।
  • कागज़ : प्रदर्शन मूल्यांकन प्रक्रिया बीजगणित; यह स्टोकेस्टिक प्रक्रिया बीजगणित है जिसे मॉडलिंग कंप्यूटर और संचार प्रणालियों के लिए डिज़ाइन किया गया है।
  • प्लेन MC: MRMC और PRISM में उपयोग किए जाने वाले सरल टेक्स्ट-फ़ाइल स्वरूप।
  • प्रोमेला: प्रक्रिया या प्रोटोकॉल मेटा भाषा; यह सत्यापन मॉडलिंग भाषा है। भाषा मॉडल के लिए समवर्ती प्रक्रियाओं के गतिशील निर्माण की अनुमति देती है, उदाहरण के लिए, वितरित सिस्टम।
  • टीएलए+: सामान्य-उद्देश्य विनिर्देशन भाषा, क्रियाओं के टेम्पोरल लॉजिक पर आधारित, मूल रूप से वितरित और समवर्ती प्रणालियों के लिए उपयोग की जाती है। विनिर्देशों और उनके गुणों के लिए भाषा समान है।

गुण भाषा

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

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

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

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

  • 1999 में, जूडी रोमिजन ने उपभोक्ता इलेक्ट्रॉनिक्स के लिए HAVi इंटरऑपरेबिलिटी ऑडियो-वीडियो प्रोटोकॉल पर दो मॉडल चेकर्स (वितरित प्रक्रियाओं का निर्माण और विश्लेषण और SPIN मॉडल चेकर) की तुलना की।[3]
  • 2003 में, Yifei Dong, Xiaoqun Du, Gerard J. Holzmann, और Scott A. Smolka ने संचार प्रोटोकॉल, GNU i- पर चार मॉडल चेकर्स (अर्थात्: Cospan, Murphi, SPIN मॉडल चेकर, और XMC) की तुलना प्रकाशित की। शिष्टाचार।[4]
  • 2005 में, ऐलेना एम. बोर्टनिक, निकोला ट्रक्का, एंटन विज, बास लुटिक, जे.एम. वैन डी मोर्टेल-फ्रॉन्ज़ाक, जोस सी.एम. बैटेन, वान फोकिंक, और जे.ई. रूडा ने चार मॉडल चेकर्स की तुलना प्रकाशित की (अर्थात्: वितरित का निर्माण और विश्लेषण) प्रक्रियाओं, एमयूसीआरएल, स्पिन मॉडल चेकर, और उप्पल मॉडल चेकर) औद्योगिक निर्माण प्रणाली, घूर्णन ड्रिलिंग मशीन पर।[5]
  • 2018 में, F. Mazzanti और ​​A. Ferrari ने दस मॉडल चेकर्स की तुलना प्रकाशित की (अर्थात्: वितरित प्रक्रियाओं का निर्माण और विश्लेषण, CPN Tools, FDR4, NuSMV/nuXmv, mCRL2, ProB, SPIN मॉडल चेकर, TLA+, UMC, और उप्पल मॉडल चेकर) ट्रेन पर्यवेक्षण समस्या पर, भाषाओं की उपयोगकर्ता-मित्रता और उपकरणों के प्रदर्शन दोनों को ध्यान में रखते हुए।[6]

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

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

यह भी देखें

संदर्भ

  1. ↑ E.R. Olderog: Operational Petri net semantics for CCSP
  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.


बाहरी संबंध

Common benchmarks
  • MCC (models of the Model Checking Contest): a collection of hundreds of Petri nets originating from many academic and industrial case studies.
  • VLTS (Very Large Transition Systems): a collection of Labelled Transition Systems of increasing sizes, used in many scientific publications.
Retrieved from ‘https://www.vigyanwiki.in/index.php?title=मॉडल_जाँच_उपकरणों_की_सूची&oldid=106757’