मॉडल की जाँच

This article is about यह लेख कंप्यूटर विज्ञान में मॉडलों की जाँच के बारे में है।. For आँकड़ों में मॉडलों की जाँच के लिए, see सांख्यिकीय मॉडल सत्यापन देखें।.

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

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

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

अवलोकन

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

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

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

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

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

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

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

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

उदाहरण

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

${\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$ और "नहीं" के लिए हैं।

तकनीक

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

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

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

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

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

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

यह समस्या सर्किट वर्ग 'AC0 (जटिलता)|AC' में है^{0</उप>। इनपुट संरचना पर कुछ प्रतिबंध लगाते समय यह Computational_complexity_theory#tractable_problem है: उदाहरण के लिए, यह आवश्यक है कि इसकी पेड़ की चौड़ाई एक स्थिरांक से बंधी हो (जो आमतौर पर मोनाडिक दूसरे क्रम का तर्क के लिए मॉडल जाँच की ट्रैक्टेबिलिटी को दर्शाता है), डिग्री को बाउंड करना (ग्राफ़ सिद्धांत) ) हर डोमेन तत्व, और अधिक सामान्य स्थितियाँ जैसे कि परिबद्ध विस्तार, स्थानीय रूप से परिबद्ध विस्तार, और कहीं-सघन संरचनाएँ। इन परिणामों को गणना एल्गोरिथम के कार्य तक बढ़ा दिया गया है, मुक्त चर के साथ प्रथम-क्रम सूत्र के सभी समाधान।}

उपकरण

Main article: List of model checking tools

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

• मिश्र धातु (विनिर्देश भाषा) (मिश्र धातु विश्लेषक)
• ब्लास्ट मॉडल चेकर (बर्कले आलसी अमूर्त सॉफ्टवेयर सत्यापन उपकरण)
• सीएडीपी (वितरित प्रक्रियाओं का निर्माण और विश्लेषण) संचार प्रोटोकॉल और वितरित प्रणालियों के डिजाइन के लिए एक टूलबॉक्स
• CPAchecker: C प्रोग्राम के लिए एक ओपन सोर्स सॉफ्टवेयर मॉडल चेकर, जो CPA फ्रेमवर्क पर आधारित है
• ECLAIR: स्वचालित विश्लेषण, सत्यापन, परीक्षण और सी और सी ++ कार्यक्रमों के परिवर्तन के लिए एक मंच
• FDR2: रीयल-टाइम सिस्टम को सत्यापित करने के लिए एक मॉडल चेकर और अनुक्रमिक प्रक्रियाओं के संचार के रूप में निर्दिष्ट किया गया है।
• संदेश पासिंग इंटरफ़ेस प्रोग्राम के लिए आईएसपी औपचारिक सत्यापन उपकरण कोड लेवल वेरिफायर
• जावा पाथफाइंडर: जावा प्रोग्राम के लिए एक ओपन-सोर्स मॉडल चेकर
• Libdmc: वितरित मॉडल जाँच के लिए एक रूपरेखा
• mCRL2 टूलसेट, बूस्ट सॉफ्टवेयर लाइसेंस, संचार प्रक्रियाओं के बीजगणित पर आधारित
• NuSMV: एक नया सांकेतिक मॉडल चेकर
• पीएटी (मॉडल चेकर): समवर्ती और रीयल-टाइम सिस्टम के लिए एक उन्नत सिम्युलेटर, मॉडल चेकर और रिफाइनमेंट चेकर
• PRISM (मॉडल चेकर): एक संभाव्य प्रतीकात्मक मॉडल चेकर
• रोमियो मॉडल चेकर | रोमियो: पैरामीट्रिक, टाइम और स्टॉपवॉच पेट्री नेट के रूप में मॉडलिंग, सिमुलेशन और रीयल-टाइम सिस्टम के सत्यापन के लिए एक एकीकृत उपकरण वातावरण
• स्पिन मॉडल चेकर: एक कठोर और अधिकतर स्वचालित फैशन में वितरित सॉफ़्टवेयर मॉडल की शुद्धता को सत्यापित करने के लिए एक सामान्य उपकरण
• तूफान (मॉडल चेकर): संभाव्य प्रणालियों के लिए एक मॉडल चेकर।
• TAPAs मॉडल चेकर: प्रक्रिया बीजगणित के विश्लेषण के लिए एक उपकरण
• टीएपीए मॉडल चेकर: टाइम्ड-आर्क पेट्री नेट्ज़ के मॉडलिंग, सत्यापन और सत्यापन के लिए एक एकीकृत उपकरण वातावरण
• लेस्ली लामपोर्ट द्वारा टीएलए+ मॉडल चेकर
• उप्पल मॉडल चेकर: समयबद्ध ऑटोमेटा के नेटवर्क के रूप में मॉडलिंग, सत्यापन और रीयल-टाइम सिस्टम के सत्यापन के लिए एक एकीकृत उपकरण वातावरण
• ज़िंग (मॉडल-चेकर) - विभिन्न स्तरों पर सॉफ़्टवेयर के राज्य मॉडल को मान्य करने के लिए Microsoft से प्रायोगिक उपकरण: ऑपरेटिंग सिस्टम के मूल में उच्च-स्तरीय प्रोटोकॉल विवरण, कार्य-प्रवाह विनिर्देश, वेब सेवाएँ, डिवाइस ड्राइवर और प्रोटोकॉल। Zing का उपयोग वर्तमान में Windows के लिए ड्राइवर विकसित करने के लिए किया जा रहा है।

यह भी देखें

• 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

अग्रिम पठन

• 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)