मॉडल की जाँच

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

तकनीक

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