मॉडल की जाँच

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

File:Two One G (cropped).jpg

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

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

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

अवलोकन

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

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

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

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

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

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

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

ऐतिहासिक रूप से, पहली प्रतीकात्मक विधियों में द्विआधारी निर्णय आरेख का उपयोग किया गया था। 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. प्रतीकात्मक एल्गोरिदम कभी भी स्पष्ट रूप से परिमित राज्य मशीनों (एफएसएम) के लिए ग्राफ का निर्माण करने से बचते हैं; इसके बजाय, वे मात्रात्मक प्रस्तावपरक तर्क में एक सूत्र का उपयोग करते हुए अंतर्निहित रूप से ग्राफ का प्रतिनिधित्व करते हैं। केन मैकमिलन के काम से बाइनरी डिसीजन डायग्राम (BDDs) के उपयोग को लोकप्रिय बनाया गया था और CUDD जैसे ओपन-सोर्स BDD हेरफेर लाइब्रेरी का विकास और बडी।
2. बंधे हुए मॉडल-चेकिंग एल्गोरिदम निश्चित संख्या में चरणों के लिए FSM को अनलॉक करते हैं, $k$, और जांचें कि संपत्ति का उल्लंघन हो सकता है या नहीं $k$ या कम कदम। इसमें आम तौर पर प्रतिबंधित मॉडल को बूलियन संतुष्टि समस्या के उदाहरण के रूप में एन्कोड करना शामिल है। प्रक्रिया को बड़े और बड़े मूल्यों के साथ दोहराया जा सकता है $k$ जब तक कि सभी संभावित उल्लंघनों से इंकार नहीं किया जाता है (cf. पुनरावृत्त गहन गहराई-प्रथम खोज)।
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)