मॉडल की जाँच: Difference between revisions

Latest revision as of 09:54, 29 August 2023

लिफ्ट नियंत्रण सॉफ्टवेयर को दोनों सुरक्षा गुणों को सत्यापित करने के लिए मॉडल-जांच किया जा सकता है, जैसे "केबिन अपने दरवाजे खुले के साथ कभी नहीं चलता",^[1] और जीवंतता गुण, जैसे "जब भी nवें फ्लोर का कॉल बटन दबाया जाता है, केबिन अंततः nवें फ्लोर पर रुक जाएगा और दरवाजा खोल देगा"।

कंप्यूटर विज्ञान में, मॉडल की जाँचया गुण की जाँच यह जाँचने की एक विधि है कि क्या सिस्टम का परिमित-अवस्था मॉडल किसी दिए गए विनिर्देश (जिसे शुद्धता के रूप में भी जाना जाता है) को पूरा करता है। यह प्रायः हार्डवेयर या सॉफ्टवेयर सिस्टम से जुड़ा होता है, जहां विनिर्देश में जीवंतता आवश्यकताएं (जैसे लाइवलॉक से बचाव) के साथ-साथ सुरक्षा आवश्यकताएं (जैसे कि सिस्टम दुर्घटना का प्रतिनिधित्व करने वाली अवस्थाओं से बचाव) सम्मिलित होती हैं।

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

अवलोकन

गुण की जाँच का उपयोग सत्यापन के लिए किया जाता है जब दो विवरण समान नहीं होते हैं। शोधन के दौरान, विनिर्देश को उन विवरणों से पूरित किया जाता है जो उच्च-स्तरीय विनिर्देशन में अनावश्यक हैं। मूल विनिर्देशन के विरुद्ध नए प्रारम्भ किए गए गुणों को सत्यापित करने की कोई आवश्यकता नहीं है क्योंकि यह संभव नहीं है। इसलिए, विशुद्ध द्वि-दिशात्मक तुल्यता जांच को एक तरफ़ा गुण जांच में आराम दिया जाता है। कार्यान्वयन या डिजाइन को सिस्टम के मॉडल के रूप में माना जाता है, जबकि विनिर्देश ऐसे गुण हैं जो मॉडल को संतुष्ट करने चाहिए।^[2]

हार्डवेयर और सॉफ़्टवेयर डिज़ाइन के मॉडल की जाँच के लिए मॉडल-जाँच विधियों का महत्वपूर्ण वर्ग विकसित किया गया है जहाँ विनिर्देश एक अस्थायी तर्क सूत्र द्वारा दिया गया है। अस्थायी तर्क विनिर्देश में अग्रणी काम आमिर पनुएली द्वारा किया गया था, जिन्हें 1996 में "कम्प्यूटिंग विज्ञान में अस्थायी तर्क परिचय करने वाले मौलिक कार्य" के लिए ट्यूरिंग पुरस्कार मिला था।^[3] मॉडल चेकिंग का प्रारम्भ ई.एम. क्लार्क, ई.ए. इमर्सन,^[4]^[5]^[6] जे.पी. क्विले और जे. सिफाकिस^[7] के अग्रणी कार्य से हुआ था। क्लार्क, एमर्सन, और सिफाकिस ने मॉडल चेकिंग के क्षेत्र को स्थापित करने और विकसित करने के अपने मौलिक कार्य के लिए 2007 ट्यूरिंग पुरस्कार साझा किया था।^[8]^[9]

मॉडल जाँच को प्रायः हार्डवेयर डिज़ाइनों पर लागू किया जाता है। सॉफ्टवेयर के लिए, अनिर्वचनीयता के कारण (कंप्यूटेबिलिटी सिद्धांत देखें) दृष्टिकोण पूरी तरह से एल्गोरिथम नहीं हो सकता है, सभी सिस्टम पर लागू होता है, और हमेशा सामान्य स्थिति में उत्तर देता है, यह किसी दिए गए गुण को सिद्ध या अस्वीकृत करने में विफल हो सकता है। अंतर्निहित-सिस्टम हार्डवेयर में, दिए गए विनिर्देशों को सत्यापित करना संभव है, उदाहरण के लिए, यूएमएल (UML) गतिविधि आरेखों^[10] या नियंत्रण-व्याख्या पेट्री जाल के माध्यम से।^[11]

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

औपचारिक रूप से, समस्या को निम्नानुसार कहा जा सकता है- वांछित गुण दिए गए है, जिसे अस्थायी तर्क सूत्र $p$ के रूप में व्यक्त किया गया है, और प्रारंभिक अवस्था $s$ , के साथ संरचना $M$ , यह तय करें कि $M,s\models p$ । यदि $M$ परिमित है, जैसा कि हार्डवेयर में है, तो मॉडल की जाँच ग्राफ़ खोज में कम हो जाती है।

प्रतीकात्मक मॉडल की जाँच

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

ऐतिहासिक रूप से, पहले प्रतीकात्मक विधियों में बीडीडी (BDDs) का उपयोग किया गया था। 1996 में आर्टिफिशियल इंटेलिजेंस (सतप्लान देखें) में योजना की समस्या को हल करने में प्रस्तावनात्मक संतुष्टि की सफलता के बाद, रैखिक अस्थायी तर्क (एलटीएल) के लिए मॉडल जाँच के लिए समान दृष्टिकोण को सामान्यीकृत किया गया था- नियोजन समस्या सुरक्षा गुणों के लिए मॉडल जाँच के अनुरूप होती है। इस विधि को सीमित मॉडल जाँच के रूप में जाना जाता है।^[12] सीमित मॉडल जाँच में बूलियन संतोषजनकता समाधानकर्ता की सफलता ने प्रतीकात्मक मॉडल जाँच में संतोषजनकता समाधानकर्ता के व्यापक उपयोग को प्रेरित किया था।^[13]

उदाहरण

इस तरह की प्रणाली की आवश्यकता का एक उदाहरण- उस समय के बीच जब किसी मंजिल पर लिफ्ट को बुलाया जाता है और जिस समय यह उस मंजिल पर अपने दरवाजे खोलती है, तो लिफ्ट उस मंजिल पर अधिकतम दो बार पहुंच सकती है। "परिमित-अवस्था सत्यापन के लिए गुण विनिर्देशन में पैटर्न" के लेखक इस आवश्यकता को निम्नलिखित एलटीएल (LTL) सूत्र में अनुवादित करते हैं-^[14]

{\begin{aligned}\Box {\Big (}({\texttt {call}}\lor \Diamond {\texttt {open}})\to &{\big (}(\lnot {\texttt {atfloor}}\lor \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (({\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor ((\lnot {\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (({\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (\lnot {\texttt {atfloor}}~{\mathcal {U}}~{\texttt {open}})))))))){\big )}{\Big )}\end{aligned}}

यहाँ, $\Box$ को "हमेशा", $\Diamond$ को "अंततः" के रूप में, ${\mathcal {U}}$ को "जब तक" के रूप में पढ़ा जाना चाहिए और अन्य प्रतीक मानक तार्किक प्रतीक $\lor$ "या" के लिए, $\land$ "और" के लिए, $\lnot$ और "नहीं" के लिए हैं।

तकनीक

मॉडल-जांच उपकरण अवस्था-स्थान के संयोजन विस्फोट का सामना करते हैं, जिसे प्रायः अवस्था विस्फोट समस्या के रूप में जाना जाता है, जिसे वास्तविक दुनिया की अधिकांश समस्याओं को हल करने के लिए संबोधित किया जाना चाहिए। इस समस्या से निपटने के कई तरीके हैं।

प्रतीकात्मक एल्गोरिदम परिमित अवस्था मशीनों (एफएसएम) के लिए स्पष्ट रूप से ग्राफ का निर्माण करने से बचते हैं इसके स्थान पर, वे मात्रात्मक प्रस्तावपरक तर्क में सूत्र का उपयोग करते हुए अंतर्निहित रूप से ग्राफ का प्रतिनिधित्व करते हैं। केन मैकमिलन^[15] के काम और सीयूडीडी (CUDD)^[16] और बीयूडीडीवाई (BuDDy) जैसे मुक्त-स्रोत बीडीडी (BDD) प्रकलन लाइब्रेरी के विकास से बाइनरी निर्णय आरेख (BDDs) के उपयोग को लोकप्रिय बनाया गया था।^[17]
सीमित मॉडल-जाँच एल्गोरिदम निश्चित चरणों की संख्या, $k$ के लिए एफएसएम (FSM) को खोलते हैं, और जाँचते हैं कि $k$ या उससे कम चरणों में गुण का उल्लंघन हो सकता है या नहीं। इसमें प्रायः प्रतिबंधित मॉडल को एसएटी (SAT) के उदाहरण के रूप में एन्कोड करना सम्मिलित होता है। इस प्रक्रिया को $k$ के बड़े और बड़े मानों के साथ तब तक दोहराया जा सकता है जब तक कि सभी संभावित उल्लंघनों से इंकार नहीं किया जाता है (सीएफ. पुनरावृत्त गहनन गहराई-प्रथम खोज)।
पृथक्करण किसी सिस्टम के गुणों को पहले सरलीकृत करके सिद्ध करने का प्रयास करता है। सरलीकृत प्रणाली प्रायः मूल के समान गुणों को संतुष्ट नहीं करती है ताकि शोधन की प्रक्रिया आवश्यक हो सके। प्रायः, किसी के पृथक्करण होने की आवश्यकता होती है (पृथक्करण पर सिद्ध गुण मूल प्रणाली के सत्य हैं) हालाँकि, कभी-कभी पृथक्करण पूर्ण नहीं होता है (मूल प्रणाली के सभी वास्तविक गुण पृथक्करण के सत्य नहीं होते हैं)। पृथक्करण का एक उदाहरण गैर-बूलियन चर के मानों की उपेक्षा करना और केवल बूलियन चर और प्रोग्राम के नियंत्रण प्रवाह पर विचार करना है इस तरह का पृथक्करण, हालांकि यह मोटे दिखाई दे सकते है, वास्तव में, सिद्ध करने के लिए पर्याप्त हो सकता है, उदाहरण के लिए- पारस्परिक बहिष्करण के गुण।
विपरीत उदाहरण- निर्देशित पृथक्करण शोधन (सीईजीएआर) मोटे (अर्थात सटीक) पृथक्करण के साथ जांच प्रारम्भ करता है और इसे पुनरावृत्त रूप से परिष्कृत करता है। जब कोई उल्लंघन (अर्थात विपरीत उदाहरण) पाया जाता है, तो उपकरण व्यवहार्यता के लिए इसका विश्लेषण करता है (अर्थात, उल्लंघन वास्तविक है या अपूर्ण पृथक्करण का परिणाम है?) यदि उल्लंघन संभव है, तो इसकी सूचना उपयोगकर्ता को दी जाती है। यदि ऐसा नहीं है, तो पृथक्करण को परिष्कृत करने के लिए अव्यवहार्यता के प्रमाण का उपयोग किया जाता है और जाँच फिर से प्रारम्भ होती है।^[18]

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

प्रथम क्रम तर्क

कम्प्यूटेशनल जटिलता सिद्धांत के क्षेत्र में मॉडल जाँच का भी अध्ययन किया जाता है। विशेष रूप से, प्रथम-क्रम तार्किक सूत्र मुक्त चर के बिना तय किया जाता है और निम्नलिखित निर्णय समस्या पर विचार किया जाता है-

परिमित व्याख्या को देखते हुए, उदाहरण के लिए, संबंधपरक डेटाबेस के रूप में वर्णित, यह तय करें कि क्या व्याख्या सूत्र का एक मॉडल है।

यह समस्या परिपथ वर्ग AC⁰ में है। इनपुट संरचना पर कुछ प्रतिबंध लगाते समय यह सुविधाजनक होता है- उदाहरण के लिए, यह आवश्यक है कि इसकी ट्रीविड्थ स्थिरांक से बंधी हो (जो प्रायः मोनाडिक द्वितीय क्रम तर्क के लिए मॉडल जाँच की शिक्षणीयता को दर्शाता है), प्रत्येक क्षेत्र तत्व की सीमा को सीमित करना, और अधिक सामान्य स्थितियाँ जैसे कि परिबद्ध विस्तार, स्थानीय रूप से परिबद्ध विस्तार, और कहीं नहीं-सघन संरचनाएँ है। इन परिणामों को मुक्त चरों के साथ प्रथम-क्रम सूत्र के सभी समाधानों की गणना करने के कार्य के लिए विस्तारित किया गया है।

उपकरण

यहाँ महत्वपूर्ण मॉडल-जाँच उपकरणों की सूची दी गई है-

मिश्र धातु (मिश्र धातु विश्लेषक)
बीएलएएसटी (BLAST) (बर्कले लेजी पृथक्करण सॉफ्टवेयर सत्यापन उपकरण)
सीएडीपी (CADP) (वितरित प्रक्रियाओं का निर्माण और विश्लेषण) संचार प्रोटोकॉल और वितरित प्रणालियों के डिजाइन के लिए उपकरण बॉक्स
सीपीएजाँचकर्ता (CPAchecker)- सी (C) प्रोग्राम के लिए मुक्त स्रोत सॉफ्टवेयर मॉडल जाँचकर्ता, जो सीपीए (CPA) रूपरेखा पर आधारित है।
ईसीएलएआईआर (ECLAIR)- स्वचालित विश्लेषण, सत्यापन, परीक्षण और सी (C) और सी ++ (C++) प्रोग्रामों के परिवर्तन के लिए एक मंच
एफडीआर2 (FDR2)- सीएसपी(CSP) प्रक्रियाओं के रूप में मॉडलिंग और निर्दिष्ट वास्तविक समय सिस्टम को सत्यापित करने के लिए एक मॉडल जाँचकर्ता
एमपीआई (MPI) प्रोग्राम के लिए आईएसपी (ISP) कोड स्तर सत्यापनकर्ता
जावा पाथफाइंडर- जावा प्रोग्रामों के लिए एक मुक्त स्रोत मॉडल जाँचकर्ता
लिबडएमसी (Libdmc)- वितरित मॉडल जाँच के लिए रूपरेखा
एमसीआरएल2 (mCRL2) टूलसेट, बूस्ट सॉफ़्टवेयर लाइसेंसबूस्ट सॉफ्टवेयर लाइसेंस, एसीपी (ACP) पर आधारित है।
एनयूएसएमवी (NuSMV)- नया प्रतीकात्मक मॉडल जाँचकर्ता
पीएटी (PAT)- समवर्ती और वास्तविक समय प्रणालियों के लिए उन्नत अनुरूपक, मॉडल जाँचकर्ता और शोधन जाँचकर्ता
प्रिज्म- संभाव्य प्रतीकात्मक मॉडल जाँचकर्ता
रोमियो- पैरामीट्रिक, टाइम और स्टॉपवॉच पेट्री नेट के रूप में मॉडलिंग, अनुरूपक और वास्तविक-समय सिस्टम के सत्यापन के लिए एकीकृत उपकरण परिवेश
स्पिन- कठोर और अधिकतर स्वचालित फैशन में वितरित सॉफ़्टवेयर मॉडल की शुद्धता को सत्यापित करने के लिए सामान्य उपकरण
स्टॉर्म-^[19] संभावनावादी सिस्टम के लिए मॉडल जाँचकर्ता।
टीएपीए (TAPAs)- प्रक्रिया बीजगणित के विश्लेषण के लिए उपकरण
टीएपीएएएल (TAPAAL)- टाइम्ड-आर्क पेट्री नेट्स के मॉडलिंग, सत्यापन और सत्यापन के लिए एकीकृत उपकरण परिवेश
लेस्ली लामपोर्ट द्वारा टीएलए+ (TLA+) मॉडल जाँचकर्ता
यूपीपीएएएल (UPPAAL)- समयबद्ध ऑटोमेटा के नेटवर्क के रूप में मॉडलिंग, सत्यापन और वास्तविक समय प्रणालियों के सत्यापन के लिए एकीकृत उपकरण परिवेश
ज़िंग^[20]- विभिन्न स्तरों पर सॉफ़्टवेयर के अवस्था मॉडल को मान्य करने के लिए माइक्रोसॉफ्ट का प्रायोगिक उपकरण- उच्च-स्तरीय प्रोटोकॉल विवरण, कार्य-प्रवाह विनिर्देश, वेब सेवाएँ, डिवाइस ड्राइवर और ऑपरेटिंग सिस्टम के मूल में प्रोटोकॉल है। ज़िंग का उपयोग वर्तमान में विंडोज के लिए ड्राइवर विकसित करने के लिए किया जा रहा है।

यह भी देखें

संदर्भ

↑ For convenience, the example properties are paraphrased in natural language here. Model-checkers require them to be expressed in some formal logic, like LTL.
↑ Lam K., William (2005). "Chapter 1.1: What Is Design Verification?". Hardware Design Verification: Simulation and Formal Method-Based Approaches. Retrieved December 12, 2012.
↑ "Amir Pnueli - A.M. Turing Award Laureate".
↑ Allen Emerson, E.; Clarke, Edmund M. (1980), "Characterizing correctness properties of parallel programs using fixpoints", Automata, Languages and Programming, Lecture Notes in Computer Science, 85: 169–181, doi:10.1007/3-540-10003-2_69, ISBN 978-3-540-10003-4
↑ Edmund M. Clarke, E. Allen Emerson: "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic". Logic of Programs 1981: 52-71.
↑ Clarke, E. M.; Emerson, E. A.; Sistla, A. P. (1986), "Automatic verification of finite-state concurrent systems using temporal logic specifications", ACM Transactions on Programming Languages and Systems, 8 (2): 244, doi:10.1145/5397.5399, S2CID 52853200
↑ Queille, J. P.; Sifakis, J. (1982), "Specification and verification of concurrent systems in CESAR", International Symposium on Programming, Lecture Notes in Computer Science, 137: 337–351, doi:10.1007/3-540-11494-7_22, ISBN 978-3-540-11494-9
↑ "Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology". Archived from the original on 2008-12-28. Retrieved 2009-01-06.
↑ USACM: 2007 Turing Award Winners Announced
↑ Grobelna, Iwona; Grobelny, Michał; Adamski, Marian (2014). "Model Checking of UML Activity Diagrams in Logic Controllers Design". Proceedings of the Ninth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX. June 30 – July 4, 2014, Brunów, Poland. Advances in Intelligent Systems and Computing. Vol. 286. pp. 233–242. doi:10.1007/978-3-319-07013-1_22. ISBN 978-3-319-07012-4.
↑ I. Grobelna, "Formal verification of embedded logic controller specification with computer deduction in temporal logic", Przeglad Elektrotechniczny, Vol.87, Issue 12a, pp.47–50, 2011
↑ Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. (2001). "संतुष्टि समाधान का उपयोग करके परिबद्ध मॉडल की जाँच". Formal Methods in System Design. 19: 7–34. doi:10.1023/A:1011276507260. S2CID 2484208.
↑ Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "बूलियन संतुष्टि सॉल्वर और मॉडल जाँच में उनके अनुप्रयोग". Proceedings of the IEEE. 103 (11): 2021–2035. doi:10.1109/JPROC.2015.2455034. S2CID 10190144.
↑ Dwyer, M.; Avrunin, G.; Corbett, J. (May 1999). "Patterns in property specifications for finite-state verification". Patterns in Property Specification for Finite-State Verification. Proceedings of the 21st international conference on Software engineering. pp. 411–420. doi:10.1145/302405.302672. ISBN 1581130740.
↑ *Symbolic Model Checking, Kenneth L. McMillan, Kluwer, ISBN 0-7923-9380-5, also online Archived 2007-06-02 at the Wayback Machine.
↑ "CUDD: CU Decision Diagram Package".
↑ "BuDDy – A Binary Decision Diagram Package".
↑ Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut (2000), "Counterexample-Guided Abstraction Refinement" (PDF), Computer Aided Verification, Lecture Notes in Computer Science, 1855: 154–169, doi:10.1007/10722167_15, ISBN 978-3-540-67770-3
↑ Storm model checker
↑ Zing

अग्रिम पठन

Peled, Doron A.; Pelliccione, Patrizio; Spoletini, Paola (2009). "Model Checking". Wiley Encyclopedia of Computer Science and Engineering. doi:10.1002/9780470050118.ecse247. ISBN 978-0-470-05011-8.
Clarke, Edmund M.; Grumberg, Orna; Peled, Doron A. (1999). Model Checking. MIT Press. ISBN 0-262-03270-8.
Berard, B.; Bidoit, M.; Finkel, A.; Laroussinie, F.; Petit, A.; Petrucci, L.; Schnoebelen, P. Systems and Software Verification: Model-Checking Techniques and Tools. ISBN 3-540-41523-8.
Huth, Michael; Ryan, Mark (2004). Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press.
Holzmann, Gerard J. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley. ISBN 0-321-22862-6.
Bradfield, Julian; Stirling, Colin (2001). "4. Modal Logics and mu-Calculi: An introduction". Handbook of Process Algebra. Elsevier. pp. 293–330. doi:10.1016/B978-044482830-9/50022-9. ISBN 978-0-444-82830-9.. JA Bergstra, A. Ponse and SA Smolka, editors." ().
"Specification Patterns". SAnToS Laboratory, Kansas State University. Archived from the original on 2011-07-19.
"Property Pattern Mappings for RAFMC". CADP:Construction and Analysis of Distributed Processes. 2019.
Mateescu, Radu; Sighireanu, Mihaela (2003). "Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus" (PDF). Science of Computer Programming. 46 (3): 255–281. doi:10.1016/S0167-6423(02)00094-1.
Müller-Olm, M.; Schmidt, D.A.; Steffen, B. (1999). "Model checking: a tutorial introduction". Static Analysis: 6th International Symposium, SAS'99, Venice, Italy, September 22-24, 1999, Proceedings. Vol. 1694. LNCS: Springer. pp. 330–354. CiteSeerX 10.1.1.96.3011. doi:10.1007/3-540-48294-6_22. ISBN 978-3-540-48294-9.
Baier, C.; Katoen, J. (2008). Principles of Model Checking. MIT Press. ISBN 978-0-262-30403-0.
Clarke, E.M. (2008). "The birth of model checking". 25 Years 2008. Lecture Notes in Computer Science. Vol. 5000. pp. 1–26. doi:10.1007/978-3-540-69850-0_1. ISBN 978-3-540-69849-4.
Emerson, E. Allen (2008). "The Beginning of Model Checking: A Personal Perspective". In Grumberg, Orna; Veith, Helmut (eds.). 25 Years of Model Checking — History, Achievements, Perspectives. LNCS. Vol. 5000. Springer. pp. 27–45. doi:10.1007/978-3-540-69850-0_2. ISBN 978-3-540-69849-4. (this is also a very good introduction and overview of model checking)

[1] For convenience, the example properties are paraphrased in natural language here. Model-checkers require them to be expressed in some formal logic, like LTL.

[2] Lam K., William (2005). "Chapter 1.1: What Is Design Verification?". Hardware Design Verification: Simulation and Formal Method-Based Approaches. Retrieved December 12, 2012.

[3] "Amir Pnueli - A.M. Turing Award Laureate".

[Allen1980-4] Allen Emerson, E.; Clarke, Edmund M. (1980), "Characterizing correctness properties of parallel programs using fixpoints", Automata, Languages and Programming, Lecture Notes in Computer Science, 85: 169–181, doi:10.1007/3-540-10003-2_69, ISBN 978-3-540-10003-4

[LoP81-5] Edmund M. Clarke, E. Allen Emerson: "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic". Logic of Programs 1981: 52-71.

[Clarke1986-6] Clarke, E. M.; Emerson, E. A.; Sistla, A. P. (1986), "Automatic verification of finite-state concurrent systems using temporal logic specifications", ACM Transactions on Programming Languages and Systems, 8 (2): 244, doi:10.1145/5397.5399, S2CID 52853200

[Queille1982-7] Queille, J. P.; Sifakis, J. (1982), "Specification and verification of concurrent systems in CESAR", International Symposium on Programming, Lecture Notes in Computer Science, 137: 337–351, doi:10.1007/3-540-11494-7_22, ISBN 978-3-540-11494-9

[8] "Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology". Archived from the original on 2008-12-28. Retrieved 2009-01-06.

[9] USACM: 2007 Turing Award Winners Announced

[10] Grobelna, Iwona; Grobelny, Michał; Adamski, Marian (2014). "Model Checking of UML Activity Diagrams in Logic Controllers Design". Proceedings of the Ninth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX. June 30 – July 4, 2014, Brunów, Poland. Advances in Intelligent Systems and Computing. Vol. 286. pp. 233–242. doi:10.1007/978-3-319-07013-1_22. ISBN 978-3-319-07012-4.

[11] I. Grobelna, "Formal verification of embedded logic controller specification with computer deduction in temporal logic", Przeglad Elektrotechniczny, Vol.87, Issue 12a, pp.47–50, 2011

[12] Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. (2001). "संतुष्टि समाधान का उपयोग करके परिबद्ध मॉडल की जाँच". Formal Methods in System Design. 19: 7–34. doi:10.1023/A:1011276507260. S2CID 2484208.

[13] Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "बूलियन संतुष्टि सॉल्वर और मॉडल जाँच में उनके अनुप्रयोग". Proceedings of the IEEE. 103 (11): 2021–2035. doi:10.1109/JPROC.2015.2455034. S2CID 10190144.

[Dwyer,_Avrunin,_Corbett-14] Dwyer, M.; Avrunin, G.; Corbett, J. (May 1999). "Patterns in property specifications for finite-state verification". Patterns in Property Specification for Finite-State Verification. Proceedings of the 21st international conference on Software engineering. pp. 411–420. doi:10.1145/302405.302672. ISBN 1581130740.

[15] *Symbolic Model Checking, Kenneth L. McMillan, Kluwer, ISBN 0-7923-9380-5, also online Archived 2007-06-02 at the Wayback Machine.

[16] "CUDD: CU Decision Diagram Package".

[17] "BuDDy – A Binary Decision Diagram Package".

[Clarke2000-18] Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut (2000), "Counterexample-Guided Abstraction Refinement" (PDF), Computer Aided Verification, Lecture Notes in Computer Science, 1855: 154–169, doi:10.1007/10722167_15, ISBN 978-3-540-67770-3

[19] Storm model checker

[20] Zing

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

@@ Line 1: / Line 1: @@
 {{short description|Computer science field}}
-{{about|checking of models in computer science|the checking of models in statistics|statistical model validation}}
+{{about|यह लेख कंप्यूटर विज्ञान में मॉडलों की जाँच के बारे में है।|आँकड़ों में मॉडलों की जाँच के लिए |सांख्यिकीय मॉडल सत्यापन देखें।}}
-[[File:Two One G (cropped).jpg|thumb|लिफ्ट नियंत्रण सॉफ्टवेयर को दोनों सुरक्षा गुणों को सत्यापित करने के लिए मॉडल-जांच किया जा सकता है, जैसे कि केबिन कभी भी अपने दरवाजे के साथ नहीं चलता है,<ref>For convenience, the example properties are paraphrased in natural language here. Model-checkers require them to be expressed in some formal logic, like [[Linear temporal logic|LTL]].</ref> और जीवंतता गुण, जैसे जब भी n<sup>वें तल का कॉल बटन दबाया जाता है, केबिन अंततः n पर रुकेगा<sup>वें तल पर और दरवाजा खोलो।]][[कंप्यूटर विज्ञान]] में, मॉडल की जाँच या संपत्ति की जाँच यह जाँचने का एक तरीका है कि क्या एक परिमित-अवस्था मशीन | एक प्रणाली का परिमित-अवस्था मॉडल एक दिए गए [[औपचारिक विनिर्देश]] (जिसे [[शुद्धता (कंप्यूटर विज्ञान)]] के रूप में भी जाना जाता है) को पूरा करता है)। यह आमतौर पर [[कंप्यूटर हार्डवेयर]] या [[सॉफ्टवेयर सिस्टम]] से जुड़ा होता है, जहां विनिर्देश में जीवंतता आवश्यकताएं (जैसे [[ livelock ]] से बचाव) के साथ-साथ सुरक्षा आवश्यकताएं (जैसे [[क्रैश (कंप्यूटिंग)]] का प्रतिनिधित्व करने वाले राज्यों से बचाव) शामिल हैं।
+[[File:Two One G (cropped).jpg|thumb|लिफ्ट नियंत्रण सॉफ्टवेयर को दोनों सुरक्षा गुणों को सत्यापित करने के लिए मॉडल-जांच किया जा सकता है, जैसे "केबिन अपने दरवाजे खुले के साथ कभी नहीं चलता",<ref>For convenience, the example properties are paraphrased in natural language here. Model-checkers require them to be expressed in some formal logic, like [[Linear temporal logic|LTL]].</ref> और जीवंतता गुण, जैसे "जब भी nवें फ्लोर का कॉल बटन दबाया जाता है, केबिन अंततः nवें फ्लोर पर रुक जाएगा और दरवाजा खोल देगा"।]][[कंप्यूटर विज्ञान]] में, '''मॉडल की जाँच'''या गुण की जाँच यह जाँचने की एक विधि है कि क्या सिस्टम का परिमित-अवस्था मॉडल किसी दिए गए [[औपचारिक विनिर्देश|विनिर्देश]] (जिसे [[शुद्धता (कंप्यूटर विज्ञान)|शुद्धता]] के रूप में भी जाना जाता है) को पूरा करता है। यह प्रायः [[कंप्यूटर हार्डवेयर|हार्डवेयर]] या [[सॉफ्टवेयर सिस्टम|सॉफ्टवेयर]] सिस्टम से जुड़ा होता है, जहां विनिर्देश में जीवंतता आवश्यकताएं (जैसे [[ livelock |लाइवलॉक]] से बचाव) के साथ-साथ सुरक्षा आवश्यकताएं (जैसे कि [[क्रैश (कंप्यूटिंग)|सिस्टम दुर्घटना]] का प्रतिनिधित्व करने वाली अवस्थाओं से बचाव) सम्मिलित होती हैं।
-इस तरह की समस्या को एल्गोरिदमिक रूप से हल करने के लिए, सिस्टम के मॉडल और उसके विनिर्देशन दोनों को कुछ सटीक गणितीय भाषा में तैयार किया जाता है। इसके लिए, समस्या को [[तर्क]] में एक कार्य के रूप में तैयार किया जाता है, अर्थात् यह जाँचने के लिए कि क्या कोई [[संरचना (गणितीय तर्क)]] किसी दिए गए तार्किक सूत्र को संतुष्ट करती है। यह सामान्य अवधारणा कई प्रकार के तर्क और कई प्रकार की संरचनाओं पर लागू होती है। एक साधारण मॉडल-चेकिंग समस्या में यह सत्यापित करना शामिल है कि क्या प्रस्तावित कलन में एक सूत्र किसी दिए गए ढांचे से संतुष्ट है।
+इस तरह की समस्या को एल्गोरिथम से हल करने के लिए, सिस्टम के मॉडल और उसके विनिर्देश दोनों को कुछ सटीक गणितीय भाषा में तैयार किया जाता है। इसके लिए, समस्या को [[तर्क]] में एक कार्य के रूप में तैयार किया जाता है, अर्थात् यह जाँचने के लिए कि क्या कोई [[संरचना (गणितीय तर्क)|संरचना]] दिए गए तार्किक सूत्र को संतुष्ट करती है। यह सामान्य अवधारणा कई प्रकार के तर्क और कई प्रकार की संरचनाओं पर लागू होती है। साधारण मॉडल-जाँच समस्या में यह सत्यापित करना सम्मिलित है कि क्या प्रस्तावपरक तर्क में कोई सूत्र किसी दी गई संरचना से संतुष्ट होता है।
-== सिंहावलोकन ==
+== अवलोकन ==
-सॉफ़्टवेयर सत्यापन के लिए संपत्ति जाँच का उपयोग तब किया जाता है जब दो विवरण समतुल्य नहीं होते हैं। परि[[शोधन (कंप्यूटिंग)]] के दौरान, विनिर्देश को उन विवरणों से पूरित किया जाता है जो उच्च-स्तरीय विनिर्देश में डोन्ट-केयर शब्द हैं। मूल विनिर्देशन के खिलाफ नई शुरू की गई संपत्तियों को सत्यापित करने की कोई आवश्यकता नहीं है क्योंकि यह संभव नहीं है। इसलिए, सख्त द्वि-दिशात्मक तुल्यता जांच एक तरफ़ा संपत्ति जाँच में ढील दी जाती है। कार्यान्वयन या डिजाइन को सिस्टम के एक मॉडल के रूप में माना जाता है, जबकि विनिर्देश गुण हैं जो मॉडल को संतुष्ट करना चाहिए।<ref>{{cite book |last= Lam K.|first=William |year=2005 |title=Hardware Design Verification: Simulation and Formal Method-Based Approaches |chapter-url=http://my.safaribooksonline.com/book/electrical-engineering/semiconductor-technology/0131433474/an-invitation-to-design-verification/ch01lev1sec1#X2ludGVybmFsX0h0bWxWaWV3P3htbGlkPTAxMzE0MzM0NzQlMkZjaDAxbGV2MXNlYzEmcXVlcnk9 |access-date=December 12, 2012|chapter=Chapter 1.1: What Is Design Verification?}}</ref>
+गुण की जाँच का उपयोग सत्यापन के लिए किया जाता है जब दो विवरण समान नहीं होते हैं। [[शोधन (कंप्यूटिंग)|शोधन]] के दौरान, विनिर्देश को उन विवरणों से पूरित किया जाता है जो उच्च-स्तरीय विनिर्देशन में अनावश्यक हैं। मूल विनिर्देशन के विरुद्ध नए प्रारम्भ किए गए गुणों को सत्यापित करने की कोई आवश्यकता नहीं है क्योंकि यह संभव नहीं है। इसलिए, विशुद्ध द्वि-दिशात्मक तुल्यता जांच को एक तरफ़ा गुण जांच में आराम दिया जाता है। कार्यान्वयन या डिजाइन को सिस्टम के मॉडल के रूप में माना जाता है, जबकि विनिर्देश ऐसे गुण हैं जो मॉडल को संतुष्ट करने चाहिए।<ref>{{cite book |last= Lam K.|first=William |year=2005 |title=Hardware Design Verification: Simulation and Formal Method-Based Approaches |chapter-url=http://my.safaribooksonline.com/book/electrical-engineering/semiconductor-technology/0131433474/an-invitation-to-design-verification/ch01lev1sec1#X2ludGVybmFsX0h0bWxWaWV3P3htbGlkPTAxMzE0MzM0NzQlMkZjaDAxbGV2MXNlYzEmcXVlcnk9 |access-date=December 12, 2012|chapter=Chapter 1.1: What Is Design Verification?}}</ref>
-कंप्यूटर हार्डवेयर और [[सॉफ़्टवेयर]] डिज़ाइन के मॉडल की जाँच के लिए मॉडल-जाँच विधियों का एक महत्वपूर्ण वर्ग विकसित किया गया है जहाँ विनिर्देश एक अस्थायी तर्क सूत्र द्वारा दिया गया है। [[ लौकिक तर्क ]] स्पेसिफिकेशंस में अग्रणी काम [[आमिर पनुएली]] द्वारा किया गया था, जिन्होंने कंप्यूटिंग साइंस में टेम्पोरल लॉजिक को पेश करने वाले सेमिनल वर्क के लिए 1996 का ट्यूरिंग अवार्ड प्राप्त किया था।<ref>{{Cite web | url=http://amturing.acm.org/award_winners/pnueli_4725172.cfm/ | title=Amir Pnueli - A.M. Turing Award Laureate}}</ref> मॉडल जाँच की शुरुआत ई. एम. क्लार्क, ई. ए. इमर्सन, के अग्रणी कार्य से हुई।<ref name=Allen1980>{{citation
+हार्डवेयर और [[सॉफ़्टवेयर]] डिज़ाइन के मॉडल की जाँच के लिए मॉडल-जाँच विधियों का महत्वपूर्ण वर्ग विकसित किया गया है जहाँ विनिर्देश एक अस्थायी तर्क सूत्र द्वारा दिया गया है। [[ लौकिक तर्क |अस्थायी तर्क]] विनिर्देश में अग्रणी काम [[आमिर पनुएली]] द्वारा किया गया था, जिन्हें 1996 में "कम्प्यूटिंग विज्ञान में अस्थायी तर्क परिचय करने वाले मौलिक कार्य" के लिए ट्यूरिंग पुरस्कार मिला था।<ref>{{Cite web | url=http://amturing.acm.org/award_winners/pnueli_4725172.cfm/ | title=Amir Pnueli - A.M. Turing Award Laureate}}</ref> मॉडल चेकिंग का प्रारम्भ ई.एम. क्लार्क, ई.ए. इमर्सन,<ref name="Allen1980">{{citation
   | last1 = Allen Emerson | first1 = E.
   | last2 = Clarke | first2 = Edmund M.
@@ Line 18: / Line 19: @@
 | series = Lecture Notes in Computer Science
   | isbn = 978-3-540-10003-4
-  }}</ref><ref name="LoP81">Edmund M. Clarke, E. Allen Emerson: [http://portal.acm.org/citation.cfm?id=747438&dl= "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic"]. Logic of Programs 1981: 52-71.</ref><ref name=Clarke1986>{{citation
+  }}</ref><ref name="LoP81">Edmund M. Clarke, E. Allen Emerson: [http://portal.acm.org/citation.cfm?id=747438&dl= "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic"]. Logic of Programs 1981: 52-71.</ref><ref name="Clarke1986">{{citation
   | last1 = Clarke | first1 =  E. M.
   | last2 = Emerson | first2 =  E. A.
@@ Line 30: / Line 31: @@
   | issue = 2
 | s2cid = 52853200
-  }}</ref> जे.पी. क्विले और जे. सिफाकिस द्वारा।<ref name=Queille1982>{{citation
+  }}</ref> जे.पी. क्विले और जे. सिफाकिस<ref name="Queille1982">{{citation
   | last1 = Queille | first1 = J. P.
   | last2 = Sifakis | first2 = J.
@@ Line 41: / Line 42: @@
 | series = Lecture Notes in Computer Science
   | isbn = 978-3-540-11494-9
-  }}</ref> क्लार्क, एमर्सन, और सिफाकिस ने मॉडल चेकिंग के क्षेत्र की स्थापना और विकास के लिए अपने मौलिक कार्य के लिए 2007 [[ट्यूरिंग अवार्ड]] साझा किया।<ref>{{Cite web |url=http://www.acm.org/press-room/news-releases/turing-award-07/ |title=Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology |access-date=2009-01-06 |archive-url=https://web.archive.org/web/20081228210748/http://www.acm.org/press-room/news-releases/turing-award-07/ |archive-date=2008-12-28 |url-status=dead }}</ref><ref>[http://usacm.acm.org/usacm/weblog/index.php?p=572 ''USACM'': 2007 Turing Award Winners Announced]</ref>
+  }}</ref> के अग्रणी कार्य से हुआ था। क्लार्क, एमर्सन, और सिफाकिस ने मॉडल चेकिंग के क्षेत्र को स्थापित करने और विकसित करने के अपने मौलिक कार्य के लिए 2007 [[ट्यूरिंग अवार्ड|ट्यूरिंग पुरस्कार]] साझा किया था।<ref>{{Cite web |url=http://www.acm.org/press-room/news-releases/turing-award-07/ |title=Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology |access-date=2009-01-06 |archive-url=https://web.archive.org/web/20081228210748/http://www.acm.org/press-room/news-releases/turing-award-07/ |archive-date=2008-12-28 |url-status=dead }}</ref><ref>[http://usacm.acm.org/usacm/weblog/index.php?p=572 ''USACM'': 2007 Turing Award Winners Announced]</ref>
-मॉडल की जाँच अक्सर हार्डवेयर डिज़ाइनों पर लागू होती है। सॉफ्टवेयर के लिए, अनिर्णयता के कारण (कंप्यूटेबिलिटी सिद्धांत (कंप्यूटर विज्ञान) देखें) दृष्टिकोण पूरी तरह से एल्गोरिथम नहीं हो सकता है, सभी प्रणालियों पर लागू होता है, और हमेशा एक उत्तर देता है; सामान्य स्थिति में, यह किसी दिए गए गुण को सिद्ध या असिद्ध करने में विफल हो सकता है। [[ अंतः स्थापित प्रणाली ]]|एम्बेडेड-सिस्टम्स हार्डवेयर में, डिलीवर किए गए विनिर्देश को सत्यापित करना संभव है, उदाहरण के लिए, [[यूएमएल गतिविधि आरेख]] के माध्यम से<ref>{{Cite book | doi=10.1007/978-3-319-07013-1_22| chapter=Model Checking of UML Activity Diagrams in Logic Controllers Design| title=Proceedings of the Ninth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX. June 30 – July 4, 2014, Brunów, Poland| series=Advances in Intelligent Systems and Computing| year=2014| last1=Grobelna| first1=Iwona| last2=Grobelny| first2=Michał| last3=Adamski| first3=Marian| volume=286| pages=233–242| isbn=978-3-319-07012-4}}</ref> या नियंत्रण-व्याख्या [[पेट्री नेट]]।<ref>I. Grobelna, "[https://www.researchgate.net/profile/Jan_Sikora3/publication/267037615_Advanced_Numerical_Modelling/links/5442adc40cf2e6f0c0f9366b/Advanced-Numerical-Modelling.pdf#page=63 Formal verification of embedded logic controller specification with computer deduction in temporal logic]", Przeglad Elektrotechniczny, Vol.87, Issue 12a, pp.47–50, 2011</ref>
-संरचना आमतौर पर एक औद्योगिक [[हार्डवेयर विवरण भाषा]] या एक विशेष प्रयोजन भाषा में स्रोत कोड विवरण के रूप में दी जाती है। ऐसा प्रोग्राम एक परिमित राज्य मशीन (एफएसएम) से मेल खाता है, यानी, एक [[निर्देशित ग्राफ]] जिसमें नोड्स (या वर्टेक्स (ग्राफ थ्योरी)) और एज (ग्राफ थ्योरी) शामिल हैं। प्रत्येक नोड के साथ परमाणु प्रस्तावों का एक सेट जुड़ा हुआ है, आमतौर पर यह बताता है कि कौन से स्मृति तत्व एक हैं। [[नोड (कंप्यूटर विज्ञान)]] एक प्रणाली की अवस्थाओं का प्रतिनिधित्व करता है, किनारे संभावित संक्रमणों का प्रतिनिधित्व करते हैं जो राज्य को बदल सकते हैं, जबकि परमाणु प्रस्ताव उन बुनियादी गुणों का प्रतिनिधित्व करते हैं जो निष्पादन के बिंदु पर होते हैं।
-औपचारिक रूप से, समस्या को निम्नानुसार कहा जा सकता है: एक वांछित संपत्ति दी गई है, जिसे अस्थायी तर्क सूत्र के रूप में व्यक्त किया गया है <math>p</math>, और एक संरचना <math>M</math> प्रारंभिक अवस्था के साथ <math>s</math>, अगर तय करें <math>M,s \models p</math>. अगर <math>M</math> परिमित है, क्योंकि यह हार्डवेयर में है, मॉडल की जाँच एक ग्राफ़ खोज को कम कर देती है।
+मॉडल जाँच को प्रायः हार्डवेयर डिज़ाइनों पर लागू किया जाता है। सॉफ्टवेयर के लिए, अनिर्वचनीयता के कारण (कंप्यूटेबिलिटी सिद्धांत देखें) दृष्टिकोण पूरी तरह से एल्गोरिथम नहीं हो सकता है, सभी सिस्टम पर लागू होता है, और हमेशा सामान्य स्थिति में उत्तर देता है, यह किसी दिए गए गुण को सिद्ध या अस्वीकृत करने में विफल हो सकता है। [[ अंतः स्थापित प्रणाली |अंतर्निहित-सिस्टम]] हार्डवेयर में, दिए गए विनिर्देशों को सत्यापित करना संभव है, उदाहरण के लिए, [[यूएमएल गतिविधि आरेख|यूएमएल (UML) गतिविधि आरेखों]]<ref>{{Cite book | doi=10.1007/978-3-319-07013-1_22| chapter=Model Checking of UML Activity Diagrams in Logic Controllers Design| title=Proceedings of the Ninth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX. June 30 – July 4, 2014, Brunów, Poland| series=Advances in Intelligent Systems and Computing| year=2014| last1=Grobelna| first1=Iwona| last2=Grobelny| first2=Michał| last3=Adamski| first3=Marian| volume=286| pages=233–242| isbn=978-3-319-07012-4}}</ref> या नियंत्रण-व्याख्या [[पेट्री नेट|पेट्री जाल]] के माध्यम से।<ref>I. Grobelna, "[https://www.researchgate.net/profile/Jan_Sikora3/publication/267037615_Advanced_Numerical_Modelling/links/5442adc40cf2e6f0c0f9366b/Advanced-Numerical-Modelling.pdf#page=63 Formal verification of embedded logic controller specification with computer deduction in temporal logic]", Przeglad Elektrotechniczny, Vol.87, Issue 12a, pp.47–50, 2011</ref>
-== प्रतीकात्मक मॉडल की जाँच ==
+संरचना को प्रायः औद्योगिक [[हार्डवेयर विवरण भाषा]] या विशेष प्रयोजन भाषा में स्रोत कोड विवरण के रूप में दिया जाता है। इस तरह का प्रोग्राम परिमित अवस्था मशीन (एफएसएम(FSM)) से मेल खाता है, अर्थात्, [[निर्देशित ग्राफ]] जिसमें नोड्स (या कोने) और किनारे सम्मिलित होते हैं। प्रत्येक नोड के साथ परमाणु प्रस्तावों का एक सेट जुड़ा हुआ होता है, प्रायः यह बताते हुए कि कौन से मेमोरी तत्व एक हैं। [[नोड (कंप्यूटर विज्ञान)|नोड्स]] सिस्टम की अवस्थाओं का प्रतिनिधित्व करते हैं, किनारे संभावित संक्रमणों का प्रतिनिधित्व करते हैं जो अवस्था को बदल सकते हैं, जबकि परमाणु प्रस्ताव मूल गुणों का प्रतिनिधित्व करते हैं जो निष्पादन के बिंदु पर होते हैं।
-एक समय में एक पहुंच योग्य राज्यों की गणना करने के बजाय, कभी-कभी एक ही चरण में बड़ी संख्या में राज्यों पर विचार करके राज्य स्थान को अधिक कुशलता से पार किया जा सकता है। जब इस तरह के राज्य-अंतरिक्ष ट्रैवर्सल राज्यों के एक सेट के प्रतिनिधित्व और तार्किक सूत्रों, [[[[द्विआधारी निर्णय आरेख]]]] (बीडीडी) या अन्य संबंधित डेटा संरचनाओं के रूप में संक्रमण संबंधों पर आधारित होते हैं, तो मॉडल-जांच विधि प्रतीकात्मक होती है।
+औपचारिक रूप से, समस्या को निम्नानुसार कहा जा सकता है- वांछित गुण दिए गए है, जिसे अस्थायी तर्क सूत्र <math>
+p</math> के रूप में व्यक्त किया गया है, और प्रारंभिक अवस्था <math>
+s</math>, के साथ संरचना <math>
+M</math>, यह तय करें कि<math>
+M,s \models p</math>। यदि <math>
+M</math> परिमित है, जैसा कि हार्डवेयर में है, तो मॉडल की जाँच ग्राफ़ खोज में कम हो जाती है।
-ऐतिहासिक रूप से, पहली प्रतीकात्मक विधियों में द्विआधारी निर्णय आरेख का उपयोग किया गया था। 1996 में [[ कृत्रिम होशियारी ]] ([[विमान बैठ गया]] देखें) में [[स्वचालित योजना और शेड्यूलिंग]] समस्या को हल करने में [[प्रस्तावित संतुष्टि]] की सफलता के बाद, समान दृष्टिकोण को [[रैखिक लौकिक तर्क]] (एलटीएल) के लिए मॉडल जाँच के लिए सामान्यीकृत किया गया था: नियोजन समस्या सुरक्षा गुणों के लिए मॉडल जाँच से मेल खाती है। . इस विधि को बाउंडेड मॉडल चेकिंग के रूप में जाना जाता है।<ref>{{Cite journal | last1 = Clarke | first1 = E. | last2 = Biere | first2 = A. | last3 = Raimi | first3 = R. | last4 = Zhu | first4 = Y. | journal = Formal Methods in System Design | volume = 19 | pages = 7–34 | year = 2001 | doi = 10.1023/A:1011276507260|title=संतुष्टि समाधान का उपयोग करके परिबद्ध मॉडल की जाँच| s2cid = 2484208 }}</ref> बाउंडेड मॉडल चेकिंग में [[बूलियन संतुष्टि समस्या]] की सफलता के कारण प्रतीकात्मक मॉडल चेकिंग में संतोषजनक सॉल्वर का व्यापक उपयोग हुआ।<ref>{{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | pages = 2021–2035 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=बूलियन संतुष्टि सॉल्वर और मॉडल जाँच में उनके अनुप्रयोग| s2cid = 10190144 }}</ref>
+== प्रतीकात्मक मॉडल की जाँच ==
+एक समय में पहुंच योग्य अवस्थाओं की गणना करने के स्थान पर, कभी-कभी बड़ी संख्या में अवस्थाओं को एक ही चरण में विचार करके अवस्था स्थान को अधिक कुशलता से पार किया जा सकता है। जब इस तरह के अवस्था-स्थान ट्रैवर्सल तार्किक सूत्रों, [[द्विआधारी निर्णय आरेख|बाइनरी निर्णय आरेख]] (बीडीडी) या अन्य संबंधित डेटा संरचनाओं के रूप में अवस्थाओं और संक्रमण संबंधों के एक सेट के प्रतिनिधित्व पर आधारित होते हैं, तो मॉडल-जांच विधि प्रतीकात्मक होती है।
+ऐतिहासिक रूप से, पहले प्रतीकात्मक विधियों में बीडीडी (BDDs) का उपयोग किया गया था। 1996 में [[ कृत्रिम होशियारी |आर्टिफिशियल इंटेलिजेंस]] ([[विमान बैठ गया|सतप्लान]] देखें) में [[स्वचालित योजना और शेड्यूलिंग|योजना]] की समस्या को हल करने में [[प्रस्तावित संतुष्टि|प्रस्तावनात्मक संतुष्टि]] की सफलता के बाद, [[रैखिक लौकिक तर्क|रैखिक अस्थायी तर्क]] (एलटीएल) के लिए मॉडल जाँच के लिए समान दृष्टिकोण को सामान्यीकृत किया गया था- नियोजन समस्या सुरक्षा गुणों के लिए मॉडल जाँच के अनुरूप होती है। इस विधि को सीमित मॉडल जाँच के रूप में जाना जाता है।<ref>{{Cite journal | last1 = Clarke | first1 = E. | last2 = Biere | first2 = A. | last3 = Raimi | first3 = R. | last4 = Zhu | first4 = Y. | journal = Formal Methods in System Design | volume = 19 | pages = 7–34 | year = 2001 | doi = 10.1023/A:1011276507260|title=संतुष्टि समाधान का उपयोग करके परिबद्ध मॉडल की जाँच| s2cid = 2484208 }}</ref> सीमित मॉडल जाँच में [[बूलियन संतुष्टि समस्या|बूलियन संतोषजनकता समाधानकर्ता]] की सफलता ने प्रतीकात्मक मॉडल जाँच में संतोषजनकता समाधानकर्ता के व्यापक उपयोग को प्रेरित किया था।<ref>{{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | pages = 2021–2035 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=बूलियन संतुष्टि सॉल्वर और मॉडल जाँच में उनके अनुप्रयोग| s2cid = 10190144 }}</ref>
 === उदाहरण ===
-ऐसी प्रणाली आवश्यकता का एक उदाहरण:
+इस तरह की प्रणाली की आवश्यकता का एक उदाहरण- उस समय के बीच जब किसी मंजिल पर लिफ्ट को बुलाया जाता है और जिस समय यह उस मंजिल पर अपने दरवाजे खोलती है, तो लिफ्ट उस मंजिल पर अधिकतम दो बार पहुंच सकती है। "परिमित-अवस्था सत्यापन के लिए गुण विनिर्देशन में पैटर्न" के लेखक इस आवश्यकता को निम्नलिखित एलटीएल (LTL) सूत्र में अनुवादित करते हैं-<ref name="Dwyer, Avrunin, Corbett" >{{Cite conference
-जिस समय लिफ्ट को किसी मंजिल पर बुलाया जाता है और जिस समय वह उस मंजिल पर अपने दरवाजे खोलती है, उस समय के बीच लिफ्ट उस मंजिल पर अधिकतम दो बार पहुंच सकती है। परिमित-राज्य सत्यापन के लिए संपत्ति विशिष्टता में पैटर्न के लेखक इस आवश्यकता को निम्नलिखित LTL सूत्र में अनुवादित करते हैं:<ref name="Dwyer, Avrunin, Corbett" >{{Cite conference
    |first1=M.  |last1=Dwyer
    |first2=G.  |last2=Avrunin
@@ Line 75: / Line 80: @@
 & (\texttt{open} \lor ((\texttt{atfloor} \land \lnot \texttt{open}) ~\mathcal{U} \\
 & (\texttt{open} \lor (\lnot \texttt{atfloor} ~\mathcal{U}~ \texttt{open}))))))))\big)\Big)\end{align}</math>
-यहाँ, <math>\Box</math> हमेशा की तरह पढ़ना चाहिए <math>\Diamond</math> आखिरकार, <math>\mathcal{U}</math> जब तक और अन्य प्रतीक मानक तार्किक प्रतीक हैं, <math>\lor</math> के लिए या, <math>\land</math> के लिए और और <math>\lnot</math> के लिए नहीं ।
+यहाँ, <math>\Box</math> को "हमेशा", <math>\Diamond</math> को "अंततः" के रूप में, <math>\mathcal{U}</math> को "जब तक" के रूप में पढ़ा जाना चाहिए और अन्य प्रतीक मानक तार्किक प्रतीक <math>\lor</math> "या" के लिए, <math>\land</math> "और" के लिए, <math>\lnot</math> और "नहीं" के लिए हैं।
 == तकनीक ==
-मॉडल-जांच उपकरण राज्य-अंतरिक्ष के एक मिश्रित विस्फोट का सामना करते हैं, जिसे आमतौर पर राज्य विस्फोट समस्या के रूप में जाना जाता है, जिसे अधिकांश वास्तविक दुनिया की समस्याओं को हल करने के लिए संबोधित किया जाना चाहिए। इस समस्या से निपटने के कई तरीके हैं।
+मॉडल-जांच उपकरण अवस्था-स्थान के संयोजन विस्फोट का सामना करते हैं, जिसे प्रायः अवस्था विस्फोट समस्या के रूप में जाना जाता है, जिसे वास्तविक दुनिया की अधिकांश समस्याओं को हल करने के लिए संबोधित किया जाना चाहिए। इस समस्या से निपटने के कई तरीके हैं।
-# प्रतीकात्मक एल्गोरिदम कभी भी स्पष्ट रूप से परिमित राज्य मशीनों (एफएसएम) के लिए ग्राफ का निर्माण करने से बचते हैं; इसके बजाय, वे मात्रात्मक प्रस्तावपरक तर्क में एक सूत्र का उपयोग करते हुए अंतर्निहित रूप से ग्राफ का प्रतिनिधित्व करते हैं। केन मैकमिलन के काम से बाइनरी डिसीजन डायग्राम (BDDs) के उपयोग को लोकप्रिय बनाया गया था<ref>* ''Symbolic Model Checking'', Kenneth L. McMillan, Kluwer, {{ISBN|0-7923-9380-5}}, [http://www.kenmcmil.com/thesis.html also online] {{Webarchive|url=https://web.archive.org/web/20070602185228/http://www.kenmcmil.com/thesis.html |date=2007-06-02 }}.</ref> और CUDD जैसे ओपन-सोर्स BDD हेरफेर लाइब्रेरी का विकास<ref>{{cite web |url=https://www.cs.rice.edu/~lm30/RSynth/CUDD/cudd/doc/ |title=CUDD: CU Decision Diagram Package }}</ref> और बडी।<ref>{{cite web |url=http://vlsicad.eecs.umich.edu/BK/Slots/cache/www.itu.dk/research/buddy/ |title=BuDDy – A Binary Decision Diagram Package}}</ref>
+# प्रतीकात्मक एल्गोरिदम परिमित अवस्था मशीनों (एफएसएम) के लिए स्पष्ट रूप से ग्राफ का निर्माण करने से बचते हैं इसके स्थान पर, वे मात्रात्मक प्रस्तावपरक तर्क में सूत्र का उपयोग करते हुए अंतर्निहित रूप से ग्राफ का प्रतिनिधित्व करते हैं। केन मैकमिलन<ref>*''Symbolic Model Checking'', Kenneth L. McMillan, Kluwer, {{ISBN|0-7923-9380-5}}, [http://www.kenmcmil.com/thesis.html also online] {{Webarchive|url=https://web.archive.org/web/20070602185228/http://www.kenmcmil.com/thesis.html |date=2007-06-02 }}.</ref> के काम और सीयूडीडी (CUDD)<ref>{{cite web |url=https://www.cs.rice.edu/~lm30/RSynth/CUDD/cudd/doc/ |title=CUDD: CU Decision Diagram Package }}</ref> और बीयूडीडीवाई (BuDDy) जैसे मुक्त-स्रोत बीडीडी (BDD) प्रकलन लाइब्रेरी के विकास से बाइनरी निर्णय आरेख (BDDs) के उपयोग को लोकप्रिय बनाया गया था।<ref>{{cite web |url=http://vlsicad.eecs.umich.edu/BK/Slots/cache/www.itu.dk/research/buddy/ |title=BuDDy – A Binary Decision Diagram Package}}</ref>
-# बंधे हुए मॉडल-चेकिंग एल्गोरिदम निश्चित संख्या में चरणों के लिए FSM को अनलॉक करते हैं, <math>k</math>, और जांचें कि संपत्ति का उल्लंघन हो सकता है या नहीं <math>k</math> या कम कदम। इसमें आम तौर पर प्रतिबंधित मॉडल को बूलियन संतुष्टि समस्या के उदाहरण के रूप में एन्कोड करना शामिल है। प्रक्रिया को बड़े और बड़े मूल्यों के साथ दोहराया जा सकता है <math>k</math> जब तक कि सभी संभावित उल्लंघनों से इंकार नहीं किया जाता है (cf. पुनरावृत्त गहन गहराई-प्रथम खोज)।
+# सीमित मॉडल-जाँच एल्गोरिदम निश्चित चरणों की संख्या,<math>k</math> के लिए एफएसएम (FSM) को खोलते हैं, और जाँचते हैं कि <math>k</math> या उससे कम चरणों में गुण का उल्लंघन हो सकता है या नहीं। इसमें प्रायः प्रतिबंधित मॉडल को एसएटी (SAT) के उदाहरण के रूप में एन्कोड करना सम्मिलित होता है। इस प्रक्रिया को <math>k</math> के बड़े और बड़े मानों के साथ तब तक दोहराया जा सकता है जब तक कि सभी संभावित उल्लंघनों से इंकार नहीं किया जाता है (सीएफ. पुनरावृत्त गहनन गहराई-प्रथम खोज)।
-# अमूर्त व्याख्या पहले इसे सरल बनाकर किसी प्रणाली के गुणों को सिद्ध करने का प्रयास करती है। सरलीकृत प्रणाली आमतौर पर मूल के समान गुणों को संतुष्ट नहीं करती है ताकि शोधन की प्रक्रिया आवश्यक हो सके। आम तौर पर, किसी को अमूर्त होने की आवश्यकता होती है (अमूर्तता पर सिद्ध गुण मूल प्रणाली के लिए सही हैं); हालाँकि, कभी-कभी अमूर्तता पूर्ण नहीं होती है (मूल प्रणाली के सभी वास्तविक गुण अमूर्तता के सत्य नहीं होते हैं)। अमूर्तता का एक उदाहरण गैर-बूलियन चर के मूल्यों की उपेक्षा करना और केवल बूलियन चर और कार्यक्रम के नियंत्रण प्रवाह पर विचार करना है; इस तरह का एक अमूर्त, हालांकि यह मोटा लग सकता है, वास्तव में, साबित करने के लिए पर्याप्त हो सकता है। पारस्परिक बहिष्करण के गुण।
+# पृथक्करण किसी सिस्टम के गुणों को पहले सरलीकृत करके सिद्ध करने का प्रयास करता है। सरलीकृत प्रणाली प्रायः मूल के समान गुणों को संतुष्ट नहीं करती है ताकि शोधन की प्रक्रिया आवश्यक हो सके। प्रायः, किसी के पृथक्करण होने की आवश्यकता होती है (पृथक्करण पर सिद्ध गुण मूल प्रणाली के सत्य हैं) हालाँकि, कभी-कभी पृथक्करण पूर्ण नहीं होता है (मूल प्रणाली के सभी वास्तविक गुण पृथक्करण के सत्य नहीं होते हैं)। पृथक्करण का एक उदाहरण गैर-बूलियन चर के मानों की उपेक्षा करना और केवल बूलियन चर और प्रोग्राम के नियंत्रण प्रवाह पर विचार करना है इस तरह का पृथक्करण, हालांकि यह मोटे दिखाई दे सकते है, वास्तव में, सिद्ध करने के लिए पर्याप्त हो सकता है, उदाहरण के लिए- पारस्परिक बहिष्करण के गुण।
-# काउंटर उदाहरण-निर्देशित अमूर्त शोधन (सीईजीएआर) मोटे (यानी सटीक) अमूर्तता के साथ जांच शुरू करता है और इसे पुनरावृत्त रूप से परिष्कृत करता है। जब कोई उल्लंघन (यानी [[प्रति उदाहरण]]) पाया जाता है, तो उपकरण व्यवहार्यता के लिए इसका विश्लेषण करता है (यानी, उल्लंघन वास्तविक है या अपूर्ण सार का परिणाम है?)। यदि उल्लंघन संभव है, तो इसकी सूचना उपयोगकर्ता को दी जाती है। यदि ऐसा नहीं है, तो अमूर्तता को परिष्कृत करने के लिए अक्षमता के प्रमाण का उपयोग किया जाता है और जाँच फिर से शुरू होती है।<ref name=Clarke2000>{{citation
+# विपरीत उदाहरण- निर्देशित पृथक्करण शोधन (सीईजीएआर) मोटे (अर्थात सटीक) पृथक्करण के साथ जांच प्रारम्भ करता है और इसे पुनरावृत्त रूप से परिष्कृत करता है। जब कोई उल्लंघन (अर्थात विपरीत उदाहरण) पाया जाता है, तो उपकरण व्यवहार्यता के लिए इसका विश्लेषण करता है (अर्थात, उल्लंघन वास्तविक है या अपूर्ण पृथक्करण का परिणाम है?) यदि उल्लंघन संभव है, तो इसकी सूचना उपयोगकर्ता को दी जाती है। यदि ऐसा नहीं है, तो पृथक्करण को परिष्कृत करने के लिए अव्यवहार्यता के प्रमाण का उपयोग किया जाता है और जाँच फिर से प्रारम्भ होती है।<ref name=Clarke2000>{{citation
   | last1 = Clarke | first1 = Edmund
   | last2 = Grumberg | first2 = Orna
@@ Line 100: / Line 105: @@
   | doi-access = free
   }}</ref>
-[[असतत प्रणाली]] प्रणालियों की तार्किक शुद्धता के कारण के लिए मॉडल-जांच उपकरण शुरू में विकसित किए गए थे, लेकिन तब से वास्तविक समय और संकर प्रणालियों के सीमित रूपों से निपटने के लिए विस्तारित किए गए हैं।
+[[असतत प्रणाली|असतत अवस्था]] प्रणालियों की तार्किक शुद्धता के कारण के लिए मॉडल-जांच उपकरण प्रारम्भ में विकसित किए गए थे, लेकिन बाद में संकर प्रणालियों के वास्तविक समय और सीमित रूपों से निपटने के लिए विस्तारित किए गए हैं।
 == प्रथम क्रम तर्क ==
-[[कम्प्यूटेशनल जटिलता सिद्धांत]] के क्षेत्र में मॉडल जाँच का भी अध्ययन किया जाता है। विशेष रूप से, एक प्रथम-क्रम तर्क | प्रथम-क्रम तार्किक सूत्र [[मुक्त चर]] के बिना तय किया जाता है और निम्नलिखित [[निर्णय समस्या]] पर विचार किया जाता है:
+[[कम्प्यूटेशनल जटिलता सिद्धांत]] के क्षेत्र में मॉडल जाँच का भी अध्ययन किया जाता है। विशेष रूप से, प्रथम-क्रम तार्किक सूत्र [[मुक्त चर]] के बिना तय किया जाता है और निम्नलिखित [[निर्णय समस्या]] पर विचार किया जाता है-
-एक परिमित [[व्याख्या (तर्क)]] को देखते हुए, उदाहरण के लिए, एक संबंधपरक डेटाबेस के रूप में वर्णित, यह तय करें कि व्याख्या सूत्र का एक मॉडल है या नहीं।
+परिमित [[व्याख्या (तर्क)|व्याख्या]] को देखते हुए, उदाहरण के लिए, संबंधपरक डेटाबेस के रूप में वर्णित, यह तय करें कि क्या व्याख्या सूत्र का एक मॉडल है।
-यह समस्या [[ सर्किट वर्ग ]] 'AC0 (जटिलता)|AC' में है<sup>0</उप>। इनपुट संरचना पर कुछ प्रतिबंध लगाते समय यह Computational_complexity_theory#tractable_problem है: उदाहरण के लिए, यह आवश्यक है कि इसकी [[ पेड़ की चौड़ाई ]] एक स्थिरांक से बंधी हो (जो आमतौर पर [[मोनाडिक दूसरे क्रम का तर्क]] के लिए मॉडल जाँच की ट्रैक्टेबिलिटी को दर्शाता है), डिग्री को बाउंड करना (ग्राफ़ सिद्धांत) ) हर डोमेन तत्व, और अधिक सामान्य स्थितियाँ जैसे कि [[परिबद्ध विस्तार]], स्थानीय रूप से परिबद्ध विस्तार, और कहीं-सघन संरचनाएँ।<ref>{{Cite journal|last1=Dawar|first1=A|last2=Kreutzer|first2=S|date=2009|title=प्रथम-क्रम तर्क की पैरामिट्रीकृत जटिलता|url=http://pdfs.semanticscholar.org/ac54/505a6c9b843259727dba98fad1a02af2a567.pdf|archive-url=https://web.archive.org/web/20190303105602/http://pdfs.semanticscholar.org/ac54/505a6c9b843259727dba98fad1a02af2a567.pdf|url-status=dead|archive-date=2019-03-03|journal=ECCC|s2cid=5856640}}</ref> इन परिणामों को गणना एल्गोरिथम के कार्य तक बढ़ा दिया गया है, मुक्त चर के साथ प्रथम-क्रम सूत्र के सभी समाधान।{{cn|date=May 2019}}
+यह समस्या [[ सर्किट वर्ग |परिपथ वर्ग]] '''AC<sup>0</sup>''' में है। इनपुट संरचना पर कुछ प्रतिबंध लगाते समय यह सुविधाजनक होता है- उदाहरण के लिए, यह आवश्यक है कि इसकी ट्रीविड्थ स्थिरांक से बंधी हो (जो प्रायः मोनाडिक द्वितीय क्रम तर्क के लिए मॉडल जाँच की शिक्षणीयता को दर्शाता है), प्रत्येक क्षेत्र तत्व की सीमा को सीमित करना, और अधिक सामान्य स्थितियाँ जैसे कि परिबद्ध विस्तार, स्थानीय रूप से परिबद्ध विस्तार, और कहीं नहीं-सघन संरचनाएँ है। इन परिणामों को मुक्त चरों के साथ प्रथम-क्रम सूत्र के सभी समाधानों की गणना करने के कार्य के लिए विस्तारित किया गया है।
 == उपकरण ==
-{{main|List of model checking tools}}
+{{main|मॉडल जाँच उपकरणों की सूची}}
-यहाँ महत्वपूर्ण मॉडल-जाँच उपकरणों की सूची दी गई है:
+यहाँ महत्वपूर्ण मॉडल-जाँच उपकरणों की सूची दी गई है-
-* मिश्र धातु (विनिर्देश भाषा) (मिश्र धातु विश्लेषक)
+* मिश्र धातु (मिश्र धातु विश्लेषक)
-* [[ब्लास्ट मॉडल चेकर]] (बर्कले आलसी अमूर्त सॉफ्टवेयर सत्यापन उपकरण)
+* [[ब्लास्ट मॉडल चेकर|बीएलएएसटी (BLAST)]] (बर्कले लेजी पृथक्करण सॉफ्टवेयर सत्यापन उपकरण)
-* [[सीएडीपी]] (वितरित प्रक्रियाओं का निर्माण और विश्लेषण) संचार प्रोटोकॉल और वितरित प्रणालियों के डिजाइन के लिए एक टूलबॉक्स
+* [[सीएडीपी|सीएडीपी (CADP)]] (वितरित प्रक्रियाओं का निर्माण और विश्लेषण) संचार प्रोटोकॉल और वितरित प्रणालियों के डिजाइन के लिए उपकरण बॉक्स
-* [[CPAchecker]]: C प्रोग्राम के लिए एक ओपन सोर्स सॉफ्टवेयर मॉडल चेकर, जो CPA फ्रेमवर्क पर आधारित है
+* [[CPAchecker|सीपीएजाँचकर्ता (CPAchecker)]]- सी (C) प्रोग्राम के लिए मुक्त स्रोत सॉफ्टवेयर मॉडल जाँचकर्ता, जो सीपीए (CPA) रूपरेखा पर आधारित है।
-* [[ECLAIR]]: स्वचालित विश्लेषण, सत्यापन, परीक्षण और सी और सी ++ कार्यक्रमों के परिवर्तन के लिए एक मंच
+* [[ECLAIR|ईसीएलएआईआर (ECLAIR)]]- स्वचालित विश्लेषण, सत्यापन, परीक्षण और सी (C) और सी ++ (C++) प्रोग्रामों के परिवर्तन के लिए एक मंच
-* [[FDR2]]: रीयल-टाइम सिस्टम को सत्यापित करने के लिए एक मॉडल चेकर और अनुक्रमिक प्रक्रियाओं के संचार के रूप में निर्दिष्ट किया गया है।
+* [[FDR2|एफडीआर2 (FDR2)]]- सीएसपी(CSP) प्रक्रियाओं के रूप में मॉडलिंग और निर्दिष्ट वास्तविक समय सिस्टम को सत्यापित करने के लिए एक मॉडल जाँचकर्ता
-* [[संदेश पासिंग इंटरफ़ेस]] प्रोग्राम के लिए [[ आईएसपी औपचारिक सत्यापन उपकरण ]] कोड लेवल वेरिफायर
+* [[संदेश पासिंग इंटरफ़ेस|एमपीआई (MPI)]] प्रोग्राम के लिए [[ आईएसपी औपचारिक सत्यापन उपकरण |आईएसपी (ISP)]] कोड स्तर सत्यापनकर्ता
-* [[जावा पाथफाइंडर]]: जावा प्रोग्राम के लिए एक ओपन-सोर्स मॉडल चेकर
+* [[जावा पाथफाइंडर]]- जावा प्रोग्रामों के लिए एक मुक्त स्रोत मॉडल जाँचकर्ता
-* [[Libdmc]]: वितरित मॉडल जाँच के लिए एक रूपरेखा
+* [[Libdmc|लिबडएमसी (Libdmc)]]- वितरित मॉडल जाँच के लिए रूपरेखा
-* [[mCRL2]] टूलसेट, [[बूस्ट सॉफ्टवेयर लाइसेंस]], संचार प्रक्रियाओं के बीजगणित पर आधारित
+* [[mCRL2|एमसीआरएल2 (mCRL2)]] टूलसेट, बूस्ट सॉफ़्टवेयर लाइसेंस[[बूस्ट सॉफ्टवेयर लाइसेंस]], एसीपी (ACP) पर आधारित है।
-* [[NuSMV]]: एक नया सांकेतिक मॉडल चेकर
+*[[NuSMV|एनयूएसएमवी (NuSMV)]]- नया प्रतीकात्मक मॉडल जाँचकर्ता
-* पीएटी (मॉडल चेकर): समवर्ती और रीयल-टाइम सिस्टम के लिए एक उन्नत सिम्युलेटर, मॉडल चेकर और रिफाइनमेंट चेकर
+*पीएटी (PAT)- समवर्ती और वास्तविक समय प्रणालियों के लिए उन्नत अनुरूपक, मॉडल जाँचकर्ता और शोधन जाँचकर्ता
-* PRISM (मॉडल चेकर): एक संभाव्य प्रतीकात्मक मॉडल चेकर
+*प्रिज्म- संभाव्य प्रतीकात्मक मॉडल जाँचकर्ता
-* रोमियो मॉडल चेकर | रोमियो: पैरामीट्रिक, टाइम और स्टॉपवॉच पेट्री नेट के रूप में मॉडलिंग, सिमुलेशन और रीयल-टाइम सिस्टम के सत्यापन के लिए एक एकीकृत उपकरण वातावरण
+*रोमियो- पैरामीट्रिक, टाइम और स्टॉपवॉच पेट्री नेट के रूप में मॉडलिंग, अनुरूपक और वास्तविक-समय सिस्टम के सत्यापन के लिए एकीकृत उपकरण परिवेश
-* [[स्पिन मॉडल चेकर]]: एक कठोर और अधिकतर स्वचालित फैशन में वितरित सॉफ़्टवेयर मॉडल की शुद्धता को सत्यापित करने के लिए एक सामान्य उपकरण
+*[[स्पिन मॉडल चेकर|स्पिन]]- कठोर और अधिकतर स्वचालित फैशन में वितरित सॉफ़्टवेयर मॉडल की शुद्धता को सत्यापित करने के लिए सामान्य उपकरण
-* [[तूफान (मॉडल चेकर)]]:<ref>[https://www.stormchecker.org/ Storm model checker]</ref> संभाव्य प्रणालियों के लिए एक मॉडल चेकर।
+*[[तूफान (मॉडल चेकर)|स्टॉर्म]]-<ref>[https://www.stormchecker.org/ Storm model checker]</ref> संभावनावादी सिस्टम के लिए मॉडल जाँचकर्ता।
-* TAPAs मॉडल चेकर: प्रक्रिया बीजगणित के विश्लेषण के लिए एक उपकरण
+*टीएपीए (TAPAs)- प्रक्रिया बीजगणित के विश्लेषण के लिए उपकरण
-* [[टीएपीए मॉडल चेकर]]: टाइम्ड-आर्क [[ पेट्री नेट्ज़ ]] के मॉडलिंग, सत्यापन और सत्यापन के लिए एक एकीकृत उपकरण वातावरण
+*[[टीएपीए मॉडल चेकर|टीएपीएएएल (TAPAAL)]]- टाइम्ड-आर्क [[ पेट्री नेट्ज़ |पेट्री नेट्स]] के मॉडलिंग, सत्यापन और सत्यापन के लिए एकीकृत उपकरण परिवेश
-* [[लेस्ली लामपोर्ट]] द्वारा [[टीएलए+]] मॉडल चेकर
+*[[लेस्ली लामपोर्ट]] द्वारा [[टीएलए+|टीएलए+ (TLA+)]] मॉडल जाँचकर्ता
-* [[उप्पल मॉडल चेकर]]: समयबद्ध ऑटोमेटा के नेटवर्क के रूप में मॉडलिंग, सत्यापन और रीयल-टाइम सिस्टम के सत्यापन के लिए एक एकीकृत उपकरण वातावरण
+* [[उप्पल मॉडल चेकर|यूपीपीएएएल (UPPAAL)]]- समयबद्ध ऑटोमेटा के नेटवर्क के रूप में मॉडलिंग, सत्यापन और वास्तविक समय प्रणालियों के सत्यापन के लिए एकीकृत उपकरण परिवेश
-* [[ज़िंग (मॉडल-चेकर)]]<ref>[https://www.microsoft.com/en-us/research/project/zing Zing]</ref> - विभिन्न स्तरों पर सॉफ़्टवेयर के राज्य मॉडल को मान्य करने के लिए [[Microsoft]] से प्रायोगिक उपकरण: ऑपरेटिंग सिस्टम के मूल में उच्च-स्तरीय प्रोटोकॉल विवरण, कार्य-प्रवाह विनिर्देश, वेब सेवाएँ, डिवाइस ड्राइवर और प्रोटोकॉल। Zing का उपयोग वर्तमान में Windows के लिए ड्राइवर विकसित करने के लिए किया जा रहा है।
+*[[ज़िंग (मॉडल-चेकर)|ज़िंग]]<ref>[https://www.microsoft.com/en-us/research/project/zing Zing]</ref>- विभिन्न स्तरों पर सॉफ़्टवेयर के अवस्था मॉडल को मान्य करने के लिए [[Microsoft|माइक्रोसॉफ्ट]] का प्रायोगिक उपकरण- उच्च-स्तरीय प्रोटोकॉल विवरण, कार्य-प्रवाह विनिर्देश, वेब सेवाएँ, डिवाइस ड्राइवर और ऑपरेटिंग सिस्टम के मूल में प्रोटोकॉल है। ज़िंग का उपयोग वर्तमान में विंडोज के लिए ड्राइवर विकसित करने के लिए किया जा रहा है।
 == यह भी देखें ==
 {{cmn|
-* [[Abstract interpretation]]
+* [[संक्षेप व्याख्या]]
-* [[Automated theorem proving]]
+* [[स्वचालित प्रमेय सिद्ध करना]]
-* [[Binary decision diagram]]
+* [[बाइनरी निर्णय आरेख]]
-* [[Büchi automaton]]
+* [[बुची स्वचल प्ररूप]]
-* [[Computation tree logic]]
+* [[कम्प्यूटेशनल ट्री तर्क]]
-* [[Formal verification]]
+* [[औपचारिक सत्यापन]]
-* [[Linear temporal logic]]
+* [[रेखीय अस्थायी तर्क]]
-* [[List of model checking tools]]
+* [[मॉडल जाँच उपकरणों की सूची]]
-* [[Partial order reduction]]
+* [[आंशिक आदेश कमी]]
-* [[Program analysis (computer science)]]
+* [[प्रोग्राम विश्लेषण (कंप्यूटर विज्ञान)]]
-* [[Static code analysis]]
+* [[स्थैतिक कोड विश्लेषण]]
 }}
 == संदर्भ ==
 {{Reflist}}
 == अग्रिम पठन ==
 {{refbegin}}
@@ Line 170: / Line 172: @@
 *{{cite book | url=https://link.springer.com/chapter/10.1007/978-3-540-69850-0_2 |first=E. Allen |last=Emerson | contribution=The Beginning of Model Checking: A Personal Perspective | pages=27–45 | isbn=978-3-540-69849-4 |editor1-first=Orna |editor1-last=Grumberg |editor2-first=Helmut |editor2-last=Veith | title=25 Years of Model Checking — History, Achievements, Perspectives | publisher=Springer | series=LNCS | volume=5000 | year=2008 | doi=10.1007/978-3-540-69850-0_2 |ref={{harvid|25 Years|2008}}}} (this is also a very good introduction and overview of model checking)
 {{refend}}
+{{DEFAULTSORT:Model Checking}}
-{{Program analysis}}
+[[Category:Articles with hatnote templates targeting a nonexistent page|Model Checking]]
-{{DEFAULTSORT:Model Checking}}[[Category: मॉडल जाँच | मॉडल जाँच ]] [[Category: कंप्यूटर विज्ञान में तर्क | कंप्यूटर विज्ञान में तर्क ]]
+[[Category:Created On 02/03/2023|Model Checking]]
+[[Category:Lua-based templates|Model Checking]]
+[[Category:Machine Translated Page|Model Checking]]
+[[Category:Multi-column templates|Model Checking]]
-[[Category: Machine Translated Page]]
+[[Category:Pages using div col with small parameter|Model Checking]]
-[[Category:Created On 02/03/2023]]
+[[Category:Pages with script errors|Model Checking]]
+[[Category:Short description with empty Wikidata description|Model Checking]]
+[[Category:Templates Vigyan Ready|Model Checking]]
+[[Category:Templates that add a tracking category|Model Checking]]
+[[Category:Templates that generate short descriptions|Model Checking]]
+[[Category:Templates using TemplateData|Model Checking]]
+[[Category:Templates using under-protected Lua modules|Model Checking]]
+[[Category:Webarchive template wayback links|Model Checking]]
+[[Category:Wikipedia fully protected templates|Div col]]
+[[Category:कंप्यूटर विज्ञान में तर्क| कंप्यूटर विज्ञान में तर्क ]]
+[[Category:मॉडल जाँच| मॉडल जाँच ]]

Anonymous

Search

मॉडल की जाँच: Difference between revisions

Namespaces

More

Page actions

Latest revision as of 09:54, 29 August 2023

Contents

अवलोकन

प्रतीकात्मक मॉडल की जाँच

उदाहरण

तकनीक

प्रथम क्रम तर्क

उपकरण

यह भी देखें

संदर्भ

अग्रिम पठन

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

मॉडल की जाँच: Difference between revisions

Latest revision as of 09:54, 29 August 2023

अवलोकन

प्रतीकात्मक मॉडल की जाँच

उदाहरण

तकनीक

प्रथम क्रम तर्क

उपकरण

यह भी देखें

संदर्भ

अग्रिम पठन

Navigation

Wiki tools

Page tools

Other projects

Categories