मॉडल की जाँच: Difference between revisions
From Vigyanwiki
No edit summary |
|||
| (14 intermediate revisions by 6 users not shown) | |||
| Line 1: | Line 1: | ||
{{short description|Computer science field}} | {{short description|Computer science field}} | ||
{{about|यह लेख कंप्यूटर विज्ञान में मॉडलों की जाँच के बारे में है।|आँकड़ों में मॉडलों की जाँच के लिए |सांख्यिकीय मॉडल सत्यापन देखें।}} | {{about|यह लेख कंप्यूटर विज्ञान में मॉडलों की जाँच के बारे में है।|आँकड़ों में मॉडलों की जाँच के लिए |सांख्यिकीय मॉडल सत्यापन देखें।}} | ||
[[File:Two One G (cropped).jpg|thumb|लिफ्ट नियंत्रण सॉफ्टवेयर को दोनों सुरक्षा गुणों को सत्यापित करने के लिए मॉडल-जांच किया जा सकता है, जैसे | [[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 |लाइवलॉक]] से बचाव) के साथ-साथ सुरक्षा आवश्यकताएं (जैसे कि [[क्रैश (कंप्यूटिंग)|सिस्टम दुर्घटना]] का प्रतिनिधित्व करने वाली अवस्थाओं से बचाव) सम्मिलित होती हैं। | ||
इस तरह की समस्या को एल्गोरिथम से हल करने के लिए, सिस्टम के मॉडल और उसके विनिर्देश दोनों को कुछ सटीक गणितीय भाषा में तैयार किया जाता है। इसके लिए, समस्या को [[तर्क]] में एक कार्य के रूप में तैयार किया जाता है, अर्थात् यह जाँचने के लिए कि क्या कोई [[संरचना (गणितीय तर्क)|संरचना]] दिए गए तार्किक सूत्र को संतुष्ट करती है। यह सामान्य अवधारणा कई प्रकार के तर्क और कई प्रकार की संरचनाओं पर लागू होती है। साधारण मॉडल-जाँच समस्या में यह सत्यापित करना सम्मिलित है कि क्या प्रस्तावपरक तर्क में कोई सूत्र किसी दी गई संरचना से संतुष्ट है। | इस तरह की समस्या को एल्गोरिथम से हल करने के लिए, सिस्टम के मॉडल और उसके विनिर्देश दोनों को कुछ सटीक गणितीय भाषा में तैयार किया जाता है। इसके लिए, समस्या को [[तर्क]] में एक कार्य के रूप में तैयार किया जाता है, अर्थात् यह जाँचने के लिए कि क्या कोई [[संरचना (गणितीय तर्क)|संरचना]] दिए गए तार्किक सूत्र को संतुष्ट करती है। यह सामान्य अवधारणा कई प्रकार के तर्क और कई प्रकार की संरचनाओं पर लागू होती है। साधारण मॉडल-जाँच समस्या में यह सत्यापित करना सम्मिलित है कि क्या प्रस्तावपरक तर्क में कोई सूत्र किसी दी गई संरचना से संतुष्ट होता है। | ||
== अवलोकन == | == अवलोकन == | ||
| Line 42: | Line 42: | ||
| series = Lecture Notes in Computer Science | | series = Lecture Notes in Computer Science | ||
| isbn = 978-3-540-11494-9 | | isbn = 978-3-540-11494-9 | ||
}}</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> | ||
मॉडल जाँच को प्रायः हार्डवेयर डिज़ाइनों पर लागू किया जाता है। सॉफ्टवेयर के लिए, अनिर्वचनीयता के कारण (कंप्यूटेबिलिटी सिद्धांत देखें) दृष्टिकोण पूरी तरह से एल्गोरिथम नहीं हो सकता है, सभी सिस्टम पर लागू होता है, और हमेशा सामान्य स्थिति में उत्तर देता है, यह किसी दिए गए गुण को | मॉडल जाँच को प्रायः हार्डवेयर डिज़ाइनों पर लागू किया जाता है। सॉफ्टवेयर के लिए, अनिर्वचनीयता के कारण (कंप्यूटेबिलिटी सिद्धांत देखें) दृष्टिकोण पूरी तरह से एल्गोरिथम नहीं हो सकता है, सभी सिस्टम पर लागू होता है, और हमेशा सामान्य स्थिति में उत्तर देता है, यह किसी दिए गए गुण को सिद्ध या अस्वीकृत करने में विफल हो सकता है। [[ अंतः स्थापित प्रणाली |अंतर्निहित-सिस्टम]] हार्डवेयर में, दिए गए विनिर्देशों को सत्यापित करना संभव है, उदाहरण के लिए, [[यूएमएल गतिविधि आरेख|यूएमएल (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)) से मेल खाता है, अर्थात्, [[निर्देशित ग्राफ]] जिसमें नोड्स (या कोने) और किनारे सम्मिलित हैं। प्रत्येक नोड के साथ परमाणु प्रस्तावों का एक सेट जुड़ा हुआ है, प्रायः यह बताते हुए कि कौन से मेमोरी तत्व एक हैं। [[नोड (कंप्यूटर विज्ञान)|नोड्स]] सिस्टम की अवस्थाओं का प्रतिनिधित्व करते हैं, किनारे संभावित संक्रमणों का प्रतिनिधित्व करते हैं जो अवस्था को बदल सकते हैं, जबकि परमाणु प्रस्ताव मूल गुणों का प्रतिनिधित्व करते हैं जो निष्पादन के बिंदु पर होते हैं। | संरचना को प्रायः औद्योगिक [[हार्डवेयर विवरण भाषा]] या विशेष प्रयोजन भाषा में स्रोत कोड विवरण के रूप में दिया जाता है। इस तरह का प्रोग्राम परिमित अवस्था मशीन (एफएसएम(FSM)) से मेल खाता है, अर्थात्, [[निर्देशित ग्राफ]] जिसमें नोड्स (या कोने) और किनारे सम्मिलित होते हैं। प्रत्येक नोड के साथ परमाणु प्रस्तावों का एक सेट जुड़ा हुआ होता है, प्रायः यह बताते हुए कि कौन से मेमोरी तत्व एक हैं। [[नोड (कंप्यूटर विज्ञान)|नोड्स]] सिस्टम की अवस्थाओं का प्रतिनिधित्व करते हैं, किनारे संभावित संक्रमणों का प्रतिनिधित्व करते हैं जो अवस्था को बदल सकते हैं, जबकि परमाणु प्रस्ताव मूल गुणों का प्रतिनिधित्व करते हैं जो निष्पादन के बिंदु पर होते हैं। | ||
औपचारिक रूप से, समस्या को निम्नानुसार कहा जा सकता है- वांछित गुण दिए गए है, जिसे अस्थायी तर्क सूत्र <math> | औपचारिक रूप से, समस्या को निम्नानुसार कहा जा सकता है- वांछित गुण दिए गए है, जिसे अस्थायी तर्क सूत्र <math> | ||
| Line 59: | Line 59: | ||
एक समय में पहुंच योग्य अवस्थाओं की गणना करने के स्थान पर, कभी-कभी बड़ी संख्या में अवस्थाओं को एक ही चरण में विचार करके अवस्था स्थान को अधिक कुशलता से पार किया जा सकता है। जब इस तरह के अवस्था-स्थान ट्रैवर्सल तार्किक सूत्रों, [[द्विआधारी निर्णय आरेख|बाइनरी निर्णय आरेख]] (बीडीडी) या अन्य संबंधित डेटा संरचनाओं के रूप में अवस्थाओं और संक्रमण संबंधों के एक सेट के प्रतिनिधित्व पर आधारित होते हैं, तो मॉडल-जांच विधि प्रतीकात्मक होती है। | एक समय में पहुंच योग्य अवस्थाओं की गणना करने के स्थान पर, कभी-कभी बड़ी संख्या में अवस्थाओं को एक ही चरण में विचार करके अवस्था स्थान को अधिक कुशलता से पार किया जा सकता है। जब इस तरह के अवस्था-स्थान ट्रैवर्सल तार्किक सूत्रों, [[द्विआधारी निर्णय आरेख|बाइनरी निर्णय आरेख]] (बीडीडी) या अन्य संबंधित डेटा संरचनाओं के रूप में अवस्थाओं और संक्रमण संबंधों के एक सेट के प्रतिनिधित्व पर आधारित होते हैं, तो मॉडल-जांच विधि प्रतीकात्मक होती है। | ||
ऐतिहासिक रूप से, पहले प्रतीकात्मक विधियों में बीडीडी (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> सीमित मॉडल जाँच में [[बूलियन संतुष्टि समस्या|बूलियन संतोषजनकता समाधानकर्ता]] की सफलता ने प्रतीकात्मक मॉडल जाँच में संतोषजनकता समाधानकर्ता के व्यापक उपयोग को प्रेरित | ऐतिहासिक रूप से, पहले प्रतीकात्मक विधियों में बीडीडी (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 | ||
| Line 86: | Line 86: | ||
# प्रतीकात्मक एल्गोरिदम परिमित अवस्था मशीनों (एफएसएम) के लिए स्पष्ट रूप से ग्राफ का निर्माण करने से बचते हैं इसके स्थान पर, वे मात्रात्मक प्रस्तावपरक तर्क में सूत्र का उपयोग करते हुए अंतर्निहित रूप से ग्राफ का प्रतिनिधित्व करते हैं। केन मैकमिलन<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> | # प्रतीकात्मक एल्गोरिदम परिमित अवस्था मशीनों (एफएसएम) के लिए स्पष्ट रूप से ग्राफ का निर्माण करने से बचते हैं इसके स्थान पर, वे मात्रात्मक प्रस्तावपरक तर्क में सूत्र का उपयोग करते हुए अंतर्निहित रूप से ग्राफ का प्रतिनिधित्व करते हैं। केन मैकमिलन<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> | ||
# सीमित मॉडल-जाँच एल्गोरिदम निश्चित चरणों की संख्या,<math>k</math> के लिए एफएसएम (FSM) को खोलते हैं, और जाँचते हैं कि <math>k</math> या उससे कम चरणों में गुण का उल्लंघन हो सकता है या नहीं। इसमें प्रायः प्रतिबंधित मॉडल को एसएटी (SAT) के उदाहरण के रूप में एन्कोड करना सम्मिलित है। इस प्रक्रिया को <math>k</math> के बड़े और बड़े मानों के साथ तब तक दोहराया जा सकता है जब तक कि सभी संभावित उल्लंघनों से इंकार नहीं किया जाता है (सीएफ. पुनरावृत्त गहनन गहराई-प्रथम खोज)। | # सीमित मॉडल-जाँच एल्गोरिदम निश्चित चरणों की संख्या,<math>k</math> के लिए एफएसएम (FSM) को खोलते हैं, और जाँचते हैं कि <math>k</math> या उससे कम चरणों में गुण का उल्लंघन हो सकता है या नहीं। इसमें प्रायः प्रतिबंधित मॉडल को एसएटी (SAT) के उदाहरण के रूप में एन्कोड करना सम्मिलित होता है। इस प्रक्रिया को <math>k</math> के बड़े और बड़े मानों के साथ तब तक दोहराया जा सकता है जब तक कि सभी संभावित उल्लंघनों से इंकार नहीं किया जाता है (सीएफ. पुनरावृत्त गहनन गहराई-प्रथम खोज)। | ||
# पृथक्करण किसी सिस्टम के गुणों को पहले सरलीकृत करके सिद्ध करने का प्रयास करता है। सरलीकृत प्रणाली प्रायः मूल के समान गुणों को संतुष्ट नहीं करती है ताकि शोधन की प्रक्रिया आवश्यक हो सके। प्रायः, किसी के पृथक्करण होने की आवश्यकता होती है (पृथक्करण पर सिद्ध गुण मूल प्रणाली के सत्य हैं) हालाँकि, कभी-कभी पृथक्करण पूर्ण नहीं होता है (मूल प्रणाली के सभी वास्तविक गुण पृथक्करण के सत्य नहीं होते हैं)। पृथक्करण का एक उदाहरण गैर-बूलियन चर के मानों की उपेक्षा करना और केवल बूलियन चर और प्रोग्राम के नियंत्रण प्रवाह पर विचार करना है इस तरह का पृथक्करण, हालांकि यह मोटे दिखाई दे सकते है, वास्तव में, सिद्ध करने के लिए पर्याप्त हो सकता है, उदाहरण के लिए- पारस्परिक बहिष्करण के गुण। | # पृथक्करण किसी सिस्टम के गुणों को पहले सरलीकृत करके सिद्ध करने का प्रयास करता है। सरलीकृत प्रणाली प्रायः मूल के समान गुणों को संतुष्ट नहीं करती है ताकि शोधन की प्रक्रिया आवश्यक हो सके। प्रायः, किसी के पृथक्करण होने की आवश्यकता होती है (पृथक्करण पर सिद्ध गुण मूल प्रणाली के सत्य हैं) हालाँकि, कभी-कभी पृथक्करण पूर्ण नहीं होता है (मूल प्रणाली के सभी वास्तविक गुण पृथक्करण के सत्य नहीं होते हैं)। पृथक्करण का एक उदाहरण गैर-बूलियन चर के मानों की उपेक्षा करना और केवल बूलियन चर और प्रोग्राम के नियंत्रण प्रवाह पर विचार करना है इस तरह का पृथक्करण, हालांकि यह मोटे दिखाई दे सकते है, वास्तव में, सिद्ध करने के लिए पर्याप्त हो सकता है, उदाहरण के लिए- पारस्परिक बहिष्करण के गुण। | ||
# विपरीत उदाहरण- निर्देशित पृथक्करण शोधन (सीईजीएआर) मोटे (अर्थात सटीक) पृथक्करण के साथ जांच प्रारम्भ करता है और इसे पुनरावृत्त रूप से परिष्कृत करता है। जब कोई उल्लंघन (अर्थात विपरीत उदाहरण) पाया जाता है, तो उपकरण व्यवहार्यता के लिए इसका विश्लेषण करता है (अर्थात, उल्लंघन वास्तविक है या अपूर्ण पृथक्करण का परिणाम है?) यदि उल्लंघन संभव है, तो इसकी सूचना उपयोगकर्ता को दी जाती है। यदि ऐसा नहीं है, तो पृथक्करण को परिष्कृत करने के लिए अव्यवहार्यता के प्रमाण का उपयोग किया जाता है और जाँच फिर से प्रारम्भ होती है।<ref name=Clarke2000>{{citation | # विपरीत उदाहरण- निर्देशित पृथक्करण शोधन (सीईजीएआर) मोटे (अर्थात सटीक) पृथक्करण के साथ जांच प्रारम्भ करता है और इसे पुनरावृत्त रूप से परिष्कृत करता है। जब कोई उल्लंघन (अर्थात विपरीत उदाहरण) पाया जाता है, तो उपकरण व्यवहार्यता के लिए इसका विश्लेषण करता है (अर्थात, उल्लंघन वास्तविक है या अपूर्ण पृथक्करण का परिणाम है?) यदि उल्लंघन संभव है, तो इसकी सूचना उपयोगकर्ता को दी जाती है। यदि ऐसा नहीं है, तो पृथक्करण को परिष्कृत करने के लिए अव्यवहार्यता के प्रमाण का उपयोग किया जाता है और जाँच फिर से प्रारम्भ होती है।<ref name=Clarke2000>{{citation | ||
| Line 112: | Line 112: | ||
परिमित [[व्याख्या (तर्क)|व्याख्या]] को देखते हुए, उदाहरण के लिए, संबंधपरक डेटाबेस के रूप में वर्णित, यह तय करें कि क्या व्याख्या सूत्र का एक मॉडल है। | परिमित [[व्याख्या (तर्क)|व्याख्या]] को देखते हुए, उदाहरण के लिए, संबंधपरक डेटाबेस के रूप में वर्णित, यह तय करें कि क्या व्याख्या सूत्र का एक मॉडल है। | ||
यह समस्या [[ सर्किट वर्ग |परिपथ वर्ग]] '''AC<sup>0</sup>''' में है। इनपुट संरचना पर कुछ प्रतिबंध लगाते समय यह सुविधाजनक होता है- उदाहरण के लिए, यह आवश्यक है कि इसकी ट्रीविड्थ स्थिरांक से बंधी हो (जो प्रायः मोनाडिक द्वितीय क्रम तर्क के लिए मॉडल जाँच की शिक्षणीयता को दर्शाता है), प्रत्येक क्षेत्र तत्व की सीमा को सीमित करना, और अधिक सामान्य स्थितियाँ जैसे कि परिबद्ध विस्तार, स्थानीय रूप से परिबद्ध विस्तार, और कहीं नहीं-सघन | यह समस्या [[ सर्किट वर्ग |परिपथ वर्ग]] '''AC<sup>0</sup>''' में है। इनपुट संरचना पर कुछ प्रतिबंध लगाते समय यह सुविधाजनक होता है- उदाहरण के लिए, यह आवश्यक है कि इसकी ट्रीविड्थ स्थिरांक से बंधी हो (जो प्रायः मोनाडिक द्वितीय क्रम तर्क के लिए मॉडल जाँच की शिक्षणीयता को दर्शाता है), प्रत्येक क्षेत्र तत्व की सीमा को सीमित करना, और अधिक सामान्य स्थितियाँ जैसे कि परिबद्ध विस्तार, स्थानीय रूप से परिबद्ध विस्तार, और कहीं नहीं-सघन संरचनाएँ है। इन परिणामों को मुक्त चरों के साथ प्रथम-क्रम सूत्र के सभी समाधानों की गणना करने के कार्य के लिए विस्तारित किया गया है। | ||
== उपकरण == | == उपकरण == | ||
{{main| | {{main|मॉडल जाँच उपकरणों की सूची}} | ||
यहाँ महत्वपूर्ण मॉडल-जाँच उपकरणों की सूची दी गई है | यहाँ महत्वपूर्ण मॉडल-जाँच उपकरणों की सूची दी गई है- | ||
* मिश्र धातु | * मिश्र धातु (मिश्र धातु विश्लेषक) | ||
* [[ब्लास्ट मॉडल चेकर]] (बर्कले | * [[ब्लास्ट मॉडल चेकर|बीएलएएसटी (BLAST)]] (बर्कले लेजी पृथक्करण सॉफ्टवेयर सत्यापन उपकरण) | ||
* [[सीएडीपी]] (वितरित प्रक्रियाओं का निर्माण और विश्लेषण) संचार प्रोटोकॉल और वितरित प्रणालियों के डिजाइन के लिए | * [[सीएडीपी|सीएडीपी (CADP)]] (वितरित प्रक्रियाओं का निर्माण और विश्लेषण) संचार प्रोटोकॉल और वितरित प्रणालियों के डिजाइन के लिए उपकरण बॉक्स | ||
* [[CPAchecker]] | * [[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)- समवर्ती और वास्तविक समय प्रणालियों के लिए उन्नत अनुरूपक, मॉडल जाँचकर्ता और शोधन जाँचकर्ता | ||
* | *प्रिज्म- संभाव्य प्रतीकात्मक मॉडल जाँचकर्ता | ||
* रोमियो | *रोमियो- पैरामीट्रिक, टाइम और स्टॉपवॉच पेट्री नेट के रूप में मॉडलिंग, अनुरूपक और वास्तविक-समय सिस्टम के सत्यापन के लिए एकीकृत उपकरण परिवेश | ||
* [[स्पिन मॉडल चेकर]] | *[[स्पिन मॉडल चेकर|स्पिन]]- कठोर और अधिकतर स्वचालित फैशन में वितरित सॉफ़्टवेयर मॉडल की शुद्धता को सत्यापित करने के लिए सामान्य उपकरण | ||
* [[तूफान (मॉडल चेकर)]] | *[[तूफान (मॉडल चेकर)|स्टॉर्म]]-<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> - विभिन्न स्तरों पर सॉफ़्टवेयर के | *[[ज़िंग (मॉडल-चेकर)|ज़िंग]]<ref>[https://www.microsoft.com/en-us/research/project/zing Zing]</ref>- विभिन्न स्तरों पर सॉफ़्टवेयर के अवस्था मॉडल को मान्य करने के लिए [[Microsoft|माइक्रोसॉफ्ट]] का प्रायोगिक उपकरण- उच्च-स्तरीय प्रोटोकॉल विवरण, कार्य-प्रवाह विनिर्देश, वेब सेवाएँ, डिवाइस ड्राइवर और ऑपरेटिंग सिस्टम के मूल में प्रोटोकॉल है। ज़िंग का उपयोग वर्तमान में विंडोज के लिए ड्राइवर विकसित करने के लिए किया जा रहा है। | ||
== यह भी देखें == | == यह भी देखें == | ||
{{cmn| | {{cmn| | ||
* [[ | * [[संक्षेप व्याख्या]] | ||
* [[ | * [[स्वचालित प्रमेय सिद्ध करना]] | ||
* [[ | * [[बाइनरी निर्णय आरेख]] | ||
* [[ | * [[बुची स्वचल प्ररूप]] | ||
* [[ | * [[कम्प्यूटेशनल ट्री तर्क]] | ||
* [[ | * [[औपचारिक सत्यापन]] | ||
* [[ | * [[रेखीय अस्थायी तर्क]] | ||
* [[ | * [[मॉडल जाँच उपकरणों की सूची]] | ||
* [[ | * [[आंशिक आदेश कमी]] | ||
* [[ | * [[प्रोग्राम विश्लेषण (कंप्यूटर विज्ञान)]] | ||
* [[ | * [[स्थैतिक कोड विश्लेषण]] | ||
}} | }} | ||
== संदर्भ == | == संदर्भ == | ||
{{Reflist}} | {{Reflist}} | ||
== अग्रिम पठन == | == अग्रिम पठन == | ||
{{refbegin}} | {{refbegin}} | ||
| Line 175: | 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) | *{{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}} | {{refend}} | ||
{{DEFAULTSORT:Model Checking}} | |||
[[Category:Articles with hatnote templates targeting a nonexistent page|Model Checking]] | |||
[[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: | [[Category:Pages using div col with small parameter|Model Checking]] | ||
[[Category: | [[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:मॉडल जाँच| मॉडल जाँच ]] | |||
Latest revision as of 09:54, 29 August 2023
.jpg)
लिफ्ट नियंत्रण सॉफ्टवेयर को दोनों सुरक्षा गुणों को सत्यापित करने के लिए मॉडल-जांच किया जा सकता है, जैसे "केबिन अपने दरवाजे खुले के साथ कभी नहीं चलता",[1] और जीवंतता गुण, जैसे "जब भी nवें फ्लोर का कॉल बटन दबाया जाता है, केबिन अंततः nवें फ्लोर पर रुक जाएगा और दरवाजा खोल देगा"।
कंप्यूटर विज्ञान में, मॉडल की जाँचया गुण की जाँच यह जाँचने की एक विधि है कि क्या सिस्टम का परिमित-अवस्था मॉडल किसी दिए गए विनिर्देश (जिसे