मॉडल की जाँच

This article is about checking of models in computer science. For the checking of models in statistics, see statistical model validation.

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

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

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

सिंहावलोकन

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

औपचारिक रूप से, समस्या को निम्नानुसार कहा जा सकता है: एक वांछित संपत्ति दी गई है, जिसे अस्थायी तर्क सूत्र के रूप में व्यक्त किया गया है $p$, और एक संरचना $M$ प्रारंभिक अवस्था के साथ $s$, अगर तय करें $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