मॉडल की जाँच

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

लिफ्ट नियंत्रण सॉफ्टवेयर को दोनों सुरक्षा गुणों को सत्यापित करने के लिए मॉडल-जांच किया जा सकता है, जैसे कि केबिन कभी भी अपने दरवाजे के साथ नहीं चलता है, और जीवंतता गुण, जैसे जब भी 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$ के लिए नहीं ।

तकनीक

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