मॉडल की जाँच

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$ परिमित है, जैसा कि हार्डवेयर में है, तो मॉडल की जाँच ग्राफ़ खोज में कम हो जाती है।

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

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

ऐतिहासिक रूप से, पहले प्रतीकात्मक विधियों में बीडीडी (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. विपरीत उदाहरण- निर्देशित पृथक्करण शोधन (सीईजीएआर) मोटे (अर्थात सटीक) पृथक्करण के साथ जांच प्रारम्भ करता है और इसे पुनरावृत्त रूप से परिष्कृत करता है। जब कोई उल्लंघन (अर्थात विपरीत उदाहरण) पाया जाता है, तो उपकरण व्यवहार्यता के लिए इसका विश्लेषण करता है (अर्थात, उल्लंघन वास्तविक है या अपूर्ण पृथक्करण का परिणाम है?) यदि उल्लंघन संभव है, तो इसकी सूचना उपयोगकर्ता को दी जाती है। यदि ऐसा नहीं है, तो पृथक्करण को परिष्कृत करने के लिए अव्यवहार्यता के प्रमाण का उपयोग किया जाता है और जाँच फिर से प्रारम्भ होती है।

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

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

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

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

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

उपकरण

Main article: मॉडल जाँच उपकरणों की सूची

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

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

यह भी देखें

• संक्षेप व्याख्या
• स्वचालित प्रमेय सिद्ध करना
• बाइनरी निर्णय आरेख
• बुची स्वचल प्ररूप
• कम्प्यूटेशनल ट्री तर्क
• औपचारिक सत्यापन
• रेखीय अस्थायी तर्क
• मॉडल जाँच उपकरणों की सूची
• आंशिक आदेश कमी
• प्रोग्राम विश्लेषण (कंप्यूटर विज्ञान)
• स्थैतिक कोड विश्लेषण