रनटाइम सत्यापन: Difference between revisions

Latest revision as of 10:16, 15 March 2023

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

इतिहास और संदर्भ

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

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

रनटाइम सत्यापन के व्यापक क्षेत्र के भीतर, कई श्रेणियों में अंतर किया जा सकता है, जैसे:

विनिर्देश-रहित जाँच जो अधिकांशतः संगामिति-संबंधित गुणों जैसे परमाणुता के निश्चित सेट को लक्षित करती है। सैवेज एट अल द्वारा इस क्षेत्र में अग्रणी कार्य किया गया है। इरेज़र एल्गोरिथ्म के साथ किया जाता हैं।^[4]
लौकिक तर्क विशिष्टताओं के संबंध में जाँच; इस दिशा में प्रारंभिक योगदान ली, कन्नन और हैवलंड और रोजू, और उनके सहयोगियों द्वारा किया गया है।^[5]^[6]^[7]^[8]

मूल दृष्टिकोण

रनटाइम सत्यापन पर ट्यूटोरियल में फैल्काॅन, हैवलंड और रीजर द्वारा वर्णित मॉनिटर आधारित सत्यापन प्रक्रिया का अवलोकन।

रनटाइम सत्यापन विधियों के व्यापक क्षेत्र को तीन आयामों द्वारा वर्गीकृत किया जा सकता है:^[9]* निष्पादन के समय ही (ऑनलाइन) या निष्पादन के बाद प्रणाली की जाँच की जा सकती है। लॉग विश्लेषण (ऑफ़लाइन) के रूप में किया जाता हैं।

सत्यापन कोड प्रणाली में एकीकृत है (जैसा कि रनटाइम सत्यापन आस्पेक्ट-ओरिएंटेड प्रोग्रामिंग|एस्पेक्ट-ओरिएंटेड प्रोग्रामिंग में किया गया है) या बाहरी इकाई के रूप में प्रदान किया गया है।
मॉनिटर वांछित विनिर्देश के उल्लंघन या सत्यापन की रिपोर्ट कर सकता है।

फिर भी, रनटाइम सत्यापन में मूल प्रक्रिया समान रहती है:^[9]

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

उदाहरण

नीचे दिए गए उदाहरण कुछ सरल गुणों पर चर्चा करते हैं, जिन पर इस लेखन के समय (अप्रैल 2011) तक कई रनटाइम सत्यापन समूहों द्वारा संभवतः छोटे बदलावों के साथ विचार किया गया है। उन्हें और अधिक रोचक बनाने के लिए, नीचे दी गई प्रत्येक संपत्ति अलग विनिर्देश औपचारिकता का उपयोग करती है और ये सभी पैरामीट्रिक हैं। पैरामीट्रिक गुण पैरामीट्रिक घटनाओं के साथ बनने वाले निशान के बारे में गुण हैं, जो ऐसी घटनाएँ हैं जो डेटा को मापदंडों से बाँधती हैं। यहाँ पैरामीट्रिक संपत्ति $\forall parameters:\varphi$ का रूप है, जहाँ $\varphi$ सामान्य (अस्थिर) पैरामीट्रिक घटनाओं का जिक्र करते हुए कुछ उचित औपचारिकता में विनिर्देश है। ऐसे पैरामीट्रिक गुणों के लिए अंतर्ज्ञान यह है कि संपत्ति द्वारा व्यक्त की गई $\varphi$ देखे गए ट्रेस में सभी पैरामीटर उदाहरणों (पैरामीट्रिक घटनाओं के माध्यम से) का सामना करना चाहिए। इस प्रकार निम्नलिखित में से कोई भी उदाहरण किसी विशेष रनटाइम सत्यापन प्रणाली के लिए विशिष्ट नहीं है, चूंकि मापदंडों के लिए समर्थन स्पष्ट रूप से आवश्यक है। निम्नलिखित उदाहरणों में जावा सिंटैक्स माना जाता है, इस प्रकार == तार्किक समानता को प्रदर्शित करता हैं, जबकि = असाइनमेंट को प्रदर्शित करता हैं। कुछ विधियाँ (जैसे, update() UnsafeEnumExample में) डमी विधियाँ हैं, जो जावा एपीआई का हिस्सा नहीं हैं, जिनका उपयोग स्पष्टता के लिए किया जाता है।

has Next ()

HasNext संपत्ति

जावा इटरेटर इंटरफ़ेस के लिए आवश्यक है कि hasNext() विधि को काॅल किया जाना चाहिए और इससे पहले सच हो जाना चाहिए next() पद्धति कहलाती है।

ऐसा नहीं होता है, यह बहुत संभव है कि उपयोगकर्ता संग्रह के अंत में पुनरावृति करता हैं। इस प्रकार दाईं ओर का आंकड़ा परिमित स्थिति मशीन दिखाता है जो रनटाइम सत्यापन के साथ इस संपत्ति को जांचने और लागू करने के लिए संभावित मॉनीटर को परिभाषित करता है। इस प्रकार अज्ञात स्थिति से, कॉल करने में हमेशा त्रुटि होती है next() विधि क्योंकि ऐसा ऑपरेशन असुरक्षित हो सकता है। अगर hasNext() कहा जाता है और true लौटाता है, कॉल करना सुरक्षित है next(), इसलिए मॉनिटर अधिक स्थिति में प्रवेश करता है। चूंकि, अगर hasNext() विधि गलत लौटाती है, इसका कोई और तत्व नहीं हैं, और मॉनिटर 'कोई नहीं' स्थिति में प्रवेश करता है। इस प्रकार इससे अधिक और कोई नहीं होता हैं जिसकी स्थिति में, कॉलिंग hasNext() विधि कोई नई जानकारी प्रदान नहीं करती है। इसको कॉल करना सुरक्षित है next() इसकी अधिक स्थिति से इस विधि के एलिमेंट सम्मिलित होने पर यह अज्ञात हो जाता है, इसलिए मॉनिटर प्रारंभिक अज्ञात स्थिति में फिर से प्रवेश करता है। इस प्रकार अंत में इसे काॅल किया जाता हैं, next() किसी भी स्थिति से विधि त्रुटि स्थिति में प्रवेश नहीं करती है। पैरामीट्रिक पास्ट टाइम लीनियर टेम्पोरल लॉजिक का उपयोग करते हुए इस संपत्ति का प्रतिनिधित्व क्या है।

$\forall ~{\text{Iterator}}~i\quad i.{\text{next}}()~\rightarrow ~\odot (i.{\text{hasNext}}()==true)$

यह सूत्र कहता है कि किसी भी कॉल को next() विधि को तुरंत कॉल से पहले होना चाहिए hasNext() विधि जो सत्य लौटाती है। यहां की संपत्ति इटरेटर i में पैरामीट्रिक है। इस संकल्पनात्मक रूप से, इसका आशय है कि परीक्षण फंक्शन में प्रत्येक संभावित इटरेटर के लिए मॉनिटर की प्रति होगी, चूंकि रनटाइम सत्यापन प्रणाली की अपने पैरामीट्रिक मॉनिटर को इस प्रकार लागू करने की आवश्यकता नहीं है। इस संपत्ति के लिए मॉनिटर हैंडलर को ट्रिगर करने के लिए सेट किया जाएगा जब सूत्र का उल्लंघन किया जाता है (समकक्ष जब परिमित स्थिति मशीन त्रुटि स्थिति में प्रवेश करती है), जो कि तब होगा next() पहले कॉल किए बिना कॉल किया जाता है hasNext(), या जब hasNext() पूर्व कहा जाता है next(), किन्तु false लौटाता हैं।

असुरक्षित ईनम

कोड जो असुरक्षित ईनम संपत्ति का उल्लंघन करता है

जावा में वेक्टर वर्ग के अपने तत्वों पर पुनरावृति के लिए दो साधन हैं। कोई भी इटरेटर इंटरफ़ेस का उपयोग कर सकता है, जैसा कि पिछले उदाहरण में देखा गया है, या कोई इनुम्रेशन इंटरफ़ेस का उपयोग कर सकता है। इटरेटर इंटरफ़ेस के लिए निकालने की विधि को जोड़ने के अतिरिक्त, मुख्य अंतर यह है कि इटरेटर तेजी से विफल होता है जबकि इनुमरेशन नहीं है। इसका अर्थ यह है कि यदि कोई वेक्टर को संशोधित करता है (इटरेटर हटाने की विधि का उपयोग करने के अतिरिक्त) इस प्रकार जब कोई इटरेटर का उपयोग करके वेक्टर पर पुनरावृति करता है, तो /java/util/ConcurrentModificationException.html ConcurrentModificationException फेंका गया है। चूंकि, गणना का उपयोग करते समय यह स्थिति नहीं है, जैसा कि उल्लेख किया गया है। इसका परिणाम फंक्शन से गैर-नियतात्मक परिणाम हो सकता है क्योंकि वेक्टर को गणना के परिप्रेक्ष्य से असंगत स्थिति में छोड़ दिया जाता है। इस प्रकार लीगेसी प्रोग्राम के लिए जो अभी भी गणना इंटरफ़ेस का उपयोग करते हैं, कोई यह लागू करना चाह सकता है कि जब उनके अंतर्निहित वेक्टर को संशोधित किया जाता है तो गणना का उपयोग नहीं किया जाता है। इस व्यवहार को लागू करने के लिए निम्नलिखित पैरामीट्रिक नियमित पैटर्न का उपयोग किया जा सकता है:

∀ वेक्टर वी, गणना ई: (ई = v.elements ()) (e.nextElement ())^* v.update() e.nextElement()

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

सेफलॉक

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

∀ Thread T, Lock L: S → ε | S start (T) S end (T) | S L अधिग्रहण (T) S L रिलीज (T)

सेफलॉक संपत्ति के दो उल्लंघनों को दर्शाने वाला ट्रेस।

पैटर्न प्रत्येक थ्रेड और लॉक के लिए नेस्टेड प्रारंभ/समाप्ति और अधिग्रहण/रिलीज जोड़े के संतुलित अनुक्रम निर्दिष्ट ( $\epsilon$ खाली क्रम है) करता है। यहां प्रारंभ और अंत फंक्शन में प्रत्येक विधि के प्रारंभ और अंत को संदर्भित करता है, इस प्रकार यह स्वयं को प्राप्त करने और प्रस्तुत करने के लिए कॉल को छोड़कर किया जाता हैं। वे थ्रेड में पैरामीट्रिक हैं क्योंकि विधियों के प्रारंभ और अंत को जोड़ना आवश्यक है यदि और केवल तभी जब वे ही थ्रेड से संबंधित हों। उसी कारण से थ्रेड में अधिग्रहण और रिलीज़ इवेंट भी पैरामीट्रिक हैं। इसके अतिरिक्त लॉक में पैरामीट्रिक स्थिति होती हैं क्योंकि हम लॉक की रिलीज़ को दूसरे के अधिग्रहण के साथ संबद्ध नहीं करना चाहते हैं। इसकी उत्तम स्थिति में, यह संभव है कि संपत्ति का उदाहरण होगा, अर्थात, थ्रेड के साथ लॉक के प्रत्येक संभावित संयोजन के लिए संदर्भ-मुक्त पार्सिंग प्रणाली की प्रति; यह फिर से, सहज रूप से होता है, क्योंकि रनटाइम सत्यापन प्रणाली समान कार्यक्षमता को अलग तरीके से लागू कर सकते हैं। उदाहरण के लिए, यदि किसी प्रणाली में थ्रेड्स हैं $t_{1}$ , $t_{2}$ , और $t_{3}$ लाॅक के साथ $l_{1}$ और $l_{2}$ , तो जोड़े < के लिए संपत्ति के उदाहरणों $t_{1}$ , $l_{1}$ >, < $t_{1}$ , $l_{2}$ >, < $t_{2}$ , $l_{1}$ >, < $t_{2}$ , $l_{2}$ >, < $t_{3}$ , $l_{1}$ >, और < $t_{3}$ , $l_{2}$ > को बनाए रखना संभव है। पैटर्न से मिलान करने में विफलताओं के लिए इस संपत्ति की जाँच की जानी चाहिए क्योंकि पैटर्न सही व्यवहार निर्दिष्ट करता है। इस प्रकार दाईं ओर का आंकड़ा निशान दिखाता है जो इस संपत्ति के दो उल्लंघनों का उत्पादन करता है। इस प्रकार नीचे दिए गए चरण विधि के प्रारंभ का प्रतिनिधित्व करते हैं, जबकि ऊपर के चरण अंत हैं। चित्र में ग्रे तीर ही लॉक के दिए गए अधिग्रहण और रिलीज के बीच मिलान दिखाते हैं। इसके लिए ट्रेस केवल थ्रेड और लॉक दिखाता है।

अनुसंधान चुनौतियाँ और अनुप्रयोग

अधिकांश रनटाइम सत्यापन शोध नीचे सूचीबद्ध या अधिक विषयों को संबोधित करते हैं।

रनटाइम ओवरहेड कम करना

एक निष्पादन प्रणाली का अवलोकन करने में सामान्यतः कुछ रनटाइम ओवरहेड होता है जो हार्डवेयर मॉनिटर अपवाद बना सकता है। इस प्रकार जितना संभव हो सके रनटाइम सत्यापन उपकरणों के ओवरहेड को कम करना महत्वपूर्ण है, मुख्यकर जब उत्पन्न मॉनिटर प्रणाली के साथ तैनात किए जाते हैं। इस प्रकार इसमें रनटाइम ओवरहेड कम करने वाली तकनीकों में सम्मिलित हैं:

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

गुण निर्दिष्ट करना

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

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

निष्पादन मॉडल और भविष्य कहनेवाला विश्लेषण

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

व्यवहार संशोधन

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

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

यह भी देखें

गतिशील फंक्शन विश्लेषण
प्रोफाइलिंग (कंप्यूटर प्रोग्रामिंग)
रनटाइम त्रुटि का पता लगाना
रनटाइम एप्लिकेशन सेल्फ-प्रोटेक्शन (RASP)

संदर्भ

↑ Ezio Bartocci and Yliès Falcone (eds), Lectures on Runtime Verification - Introductory and Advanced Topics, Part of the Lecture Notes in Computer Science book series (LNCS, volume 10457), also part of the Programming and Software Engineering book subseries (LNPSE, volume 10457), 2018. Lecture Notes in Computer Science. Vol. 10457. 2018. doi:10.1007/978-3-319-75632-5. ISBN 978-3-319-75631-8. S2CID 23246713.
↑ "RV'01 - रनटाइम सत्यापन पर पहली कार्यशाला". Runtime Verification Conferences. 23 July 2001. Retrieved 25 February 2017.
↑ Klaus Havelund and Grigore Rosu. 2004. An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods in System Design, 24(2), March 2004.
↑ Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. 1997. Eraser: a Dynamic Data Race Detector for Multithreaded Programs. ACM Trans. Comput. Syst. 15(4), November 1997, pp. 391-411.
↑ Moonjoo Kim, Mahesh Viswanathan, Insup Lee, Hanêne Ben-Abdellah, Sampath Kannan, and Oleg Sokolsky, Formally Specified Monitoring of Temporal Properties, Proceedings of the European Conference on Real-Time Systems, June 1999.
↑ Insup Lee, Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, Mahesh Viswanathan, Runtime Assurance Based On Formal Specifications, Proceedings of International Conference on Parallel and Distributed Processing Techniques and Applications, June 1999.
↑ Klaus Havelund, Using Runtime Analysis to Guide Model Checking of Java Programs, 7th International SPIN Workshop, August 2000.
↑ Klaus Havelund and Grigore Rosu, Monitoring Programs using Rewriting, Automated Software Engineering (ASE'01), November 2001.
↑ ^9.0 ^9.1 Yliès Falcone, Klaus Havelund and Giles, A Tutorial on Runtime Verification, 2013

[1] Ezio Bartocci and Yliès Falcone (eds), Lectures on Runtime Verification - Introductory and Advanced Topics, Part of the Lecture Notes in Computer Science book series (LNCS, volume 10457), also part of the Programming and Software Engineering book subseries (LNPSE, volume 10457), 2018. Lecture Notes in Computer Science. Vol. 10457. 2018. doi:10.1007/978-3-319-75632-5. ISBN 978-3-319-75631-8. S2CID 23246713.

[2] "RV'01 - रनटाइम सत्यापन पर पहली कार्यशाला". Runtime Verification Conferences. 23 July 2001. Retrieved 25 February 2017.

[Havelund2001Overview-3] Klaus Havelund and Grigore Rosu. 2004. An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods in System Design, 24(2), March 2004.

[SavageTCS1997-4] Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. 1997. Eraser: a Dynamic Data Race Detector for Multithreaded Programs. ACM Trans. Comput. Syst. 15(4), November 1997, pp. 391-411.

[5] Moonjoo Kim, Mahesh Viswanathan, Insup Lee, Hanêne Ben-Abdellah, Sampath Kannan, and Oleg Sokolsky, Formally Specified Monitoring of Temporal Properties, Proceedings of the European Conference on Real-Time Systems, June 1999.

[6] Insup Lee, Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, Mahesh Viswanathan, Runtime Assurance Based On Formal Specifications, Proceedings of International Conference on Parallel and Distributed Processing Techniques and Applications, June 1999.

[HavelundSPIN2000-7] Klaus Havelund, Using Runtime Analysis to Guide Model Checking of Java Programs, 7th International SPIN Workshop, August 2000.

[HavelundRosuASE2001-8] Klaus Havelund and Grigore Rosu, Monitoring Programs using Rewriting, Automated Software Engineering (ASE'01), November 2001.

[havelundRVTutorial2012-9] 9.0 ^9.1 Yliès Falcone, Klaus Havelund and Giles, A Tutorial on Runtime Verification, 2013

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

@@ Line 1: / Line 1: @@
-रनटाइम सत्यापन एक कंप्यूटिंग सिस्टम विश्लेषण और निष्पादन दृष्टिकोण है जो एक चल रहे सिस्टम से जानकारी निकालने और कुछ गुणों को संतुष्ट या उल्लंघन करने वाले देखे गए व्यवहारों का पता लगाने और संभावित रूप से प्रतिक्रिया करने के लिए इसका उपयोग करने पर आधारित है।<ref>{{cite book |title=Ezio Bartocci and Yliès Falcone (eds), Lectures on Runtime Verification - Introductory and Advanced Topics, Part of the Lecture Notes in Computer Science book series (LNCS, volume 10457), also part of the Programming and Software Engineering book subseries (LNPSE, volume 10457), 2018 |volume = 10457|doi=10.1007/978-3-319-75632-5 |series = Lecture Notes in Computer Science|year = 2018|isbn = 978-3-319-75631-8| s2cid=23246713 }}</ref> [[ दौड़ की स्थिति ]] और [[ गतिरोध ]] फ्रीडम जैसे कुछ बहुत ही खास गुण, आमतौर पर सभी सिस्टम द्वारा संतुष्ट होने के लिए वांछित होते हैं और एल्गोरिथम द्वारा सर्वोत्तम रूप से कार्यान्वित किए जा सकते हैं। [[औपचारिक विनिर्देश]]ों के रूप में अन्य गुणों को अधिक आसानी से कैप्चर किया जा सकता है। रनटाइम सत्यापन विनिर्देशों को आमतौर पर ट्रेस विधेय औपचारिकताओं में व्यक्त किया जाता है, जैसे परिमित राज्य मशीन, [[नियमित अभिव्यक्ति]], [[संदर्भ-मुक्त भाषा]] | संदर्भ-मुक्त पैटर्न, रैखिक लौकिक लॉजिक्स, आदि, या इनके विस्तार। यह [[सॉफ़्टवेयर परीक्षण]] की तुलना में कम तदर्थ दृष्टिकोण की अनुमति देता है। हालांकि, निष्पादन प्रणाली की निगरानी के लिए किसी भी तंत्र को रनटाइम सत्यापन माना जाता है, जिसमें टेस्ट ऑरेकल और संदर्भ कार्यान्वयन के खिलाफ सत्यापन शामिल है {{Citation needed|date=August 2012}}. जब औपचारिक आवश्यकताओं के विनिर्देश प्रदान किए जाते हैं, तो मॉनिटर उनसे संश्लेषित होते हैं और इंस्ट्रूमेंटेशन के माध्यम से सिस्टम के भीतर संचार करते हैं। रनटाइम सत्यापन का उपयोग कई उद्देश्यों के लिए किया जा सकता है, जैसे कि सुरक्षा या सुरक्षा नीति की निगरानी, डिबगिंग, परीक्षण, सत्यापन, सत्यापन, प्रोफाइलिंग, दोष संरक्षण, व्यवहार संशोधन (जैसे, पुनर्प्राप्ति), आदि। रनटाइम सत्यापन पारंपरिक [[औपचारिक सत्यापन]] तकनीकों की जटिलता से बचा जाता है। , जैसे मॉडल जांच और प्रमेय साबित करना, केवल एक या कुछ निष्पादन निशानों का विश्लेषण करके और वास्तविक प्रणाली के साथ सीधे काम करके, इस प्रकार अपेक्षाकृत अच्छी तरह से स्केलिंग करना और विश्लेषण के परिणामों में अधिक आत्मविश्वास देना (क्योंकि यह कठिन और त्रुटि से बचाता है) सिस्टम को औपचारिक रूप से मॉडलिंग करने का प्रोन कदम), कम कवरेज की कीमत पर। इसके अलावा, इसकी चिंतनशील क्षमताओं के माध्यम से रनटाइम सत्यापन को लक्ष्य प्रणाली का एक अभिन्न अंग बनाया जा सकता है, तैनाती के दौरान इसके निष्पादन की निगरानी और मार्गदर्शन किया जा सकता है।
+'''रनटाइम सत्यापन''' कंप्यूटिंग प्रणाली विश्लेषण और निष्पादन का मुख्य दृष्टिकोण हैं, जो किसी रन हो रही प्रणाली से जानकारी प्राप्त करने और उनके कुछ गुणों को संतुष्ट या उल्लंघन करने वाले व्यवहारों का पता लगाने और संभावित रूप से प्रतिक्रिया करने के लिए इसका उपयोग करने पर आधारित है।<ref>{{cite book |title=Ezio Bartocci and Yliès Falcone (eds), Lectures on Runtime Verification - Introductory and Advanced Topics, Part of the Lecture Notes in Computer Science book series (LNCS, volume 10457), also part of the Programming and Software Engineering book subseries (LNPSE, volume 10457), 2018 |volume = 10457|doi=10.1007/978-3-319-75632-5 |series = Lecture Notes in Computer Science|year = 2018|isbn = 978-3-319-75631-8| s2cid=23246713 }}</ref> [[ दौड़ की स्थिति |रनटाइम की स्थिति]] और [[ गतिरोध |गतिरोध]] फ्रीडम जैसे कुछ बहुत ही मुख्य गुण, सामान्यतः सभी प्रणाली द्वारा संतुष्ट होने के लिए वांछित होते हैं और एल्गोरिथम द्वारा सर्वोत्तम रूप से कार्यान्वित किए जा सकते हैं। [[औपचारिक विनिर्देश]] के रूप में अन्य गुणों को अधिक सरलता से कैप्चर किया जाता है। इस प्रकार रनटाइम सत्यापन विनिर्देशों को सामान्यतः ट्रेस विधेय औपचारिकताओं में व्यक्त किया जाता है, जैसे परिमित स्थिति मशीन, [[नियमित अभिव्यक्ति]], [[संदर्भ-मुक्त भाषा]] या संदर्भ-मुक्त पैटर्न, रैखिक लौकिक लॉजिक्स, आदि, या इनके विस्तार इत्यादि। यह [[सॉफ़्टवेयर परीक्षण]] की तुलना में कम तदर्थ दृष्टिकोण की अनुमति देता है। चूंकि निष्पादन प्रणाली की जाँच के लिए किसी भी प्रणाली को रनटाइम सत्यापन माना जाता है, जिसमें टेस्ट ऑरेकल और संदर्भ कार्यान्वयन के विरूद्ध सत्यापन सम्मिलित है। जब औपचारिक आवश्यकताओं के विनिर्देश प्रदान किए जाते हैं, तो मॉनिटर उनसे संश्लेषित होते हैं और इस प्रकार इंस्ट्रूमेंटेशन के माध्यम से प्रणाली के भीतर संचार करते हैं। इस प्रकार रनटाइम सत्यापन का उपयोग कई उद्देश्यों के लिए किया जा सकता है, जैसे कि सुरक्षा या सुरक्षा नीति की जाँच, डिबगिंग, परीक्षण, सत्यापन, सत्यापन, प्रोफाइलिंग, दोष संरक्षण, व्यवहार संशोधन (जैसे, पुनर्प्राप्ति) आदि। इस प्रकार रनटाइम सत्यापन पारंपरिक [[औपचारिक सत्यापन]] विधियों की जटिलता से बचा जाता है। जैसे मॉडल जांच और प्रमेय प्रमाणित करना, केवल या कुछ निष्पादन निशानों का विश्लेषण करके और वास्तविक प्रणाली के साथ सीधे कार्य करके, इस प्रकार अपेक्षाकृत अच्छी तरह से स्केलिंग करना और विश्लेषण के परिणामों में अधिक आत्मविश्वास देना (क्योंकि यह कठिन और त्रुटि से बचाता है) प्रणाली की औपचारिक रूप से मॉडलिंग करने का प्रोन चरण जो कि कम कवरेज की कीमत पर किया जाता हैं। इसके अतिरिक्त, इसकी चिंतनशील क्षमताओं के माध्यम से रनटाइम सत्यापन को लक्ष्य प्रणाली का अभिन्न अंग बनाया जा सकता है, इस स्थिति के समय इसके निष्पादन की जाँच और मार्गदर्शन किया जाता हैं।
 == इतिहास और संदर्भ ==
-सिस्टम या प्रोग्राम को निष्पादित करने के विरुद्ध औपचारिक या अनौपचारिक रूप से निर्दिष्ट गुणों की जाँच करना एक पुराना विषय है (उल्लेखनीय उदाहरण सॉफ़्टवेयर में [[गतिशील टाइपिंग]], या विफल-सुरक्षित उपकरण या हार्डवेयर में वॉचडॉग टाइमर हैं), जिनकी सटीक जड़ों की पहचान करना कठिन है। शब्दावली रनटाइम सत्यापन को औपचारिक रूप से 2001 की कार्यशाला के नाम के रूप में पेश किया गया था<ref>{{cite web |url=http://runtime-verification.org/rv2001/index.html |title=RV'01 - रनटाइम सत्यापन पर पहली कार्यशाला|date=23 July 2001 |website=Runtime Verification Conferences |access-date=25 February 2017}}</ref> औपचारिक सत्यापन और परीक्षण के बीच सीमा पर समस्याओं का समाधान करने के उद्देश्य से। बड़े कोड आधारों के लिए, मैन्युअल रूप से टेस्ट केस लिखने में बहुत समय लगता है। इसके अलावा, विकास के दौरान सभी त्रुटियों का पता नहीं लगाया जा सकता है। अंतरिक्ष यान, रोवर्स और एवियोनिक्स प्रौद्योगिकी में उच्च सुरक्षा मानकों को संग्रहीत करने के लिए क्लाउस हैवेलंड और [[ग्रेगरी रेड]] द्वारा नासा एम्स रिसर्च सेंटर में स्वचालित सत्यापन के लिए प्रारंभिक योगदान दिया गया था।<ref name="Havelund2001Overview">Klaus Havelund and Grigore Rosu. 2004. An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods in System Design, 24(2), March 2004.</ref> उन्होंने टेम्पोरल लॉजिक में विनिर्देशों को सत्यापित करने और एकल निष्पादन पथों का विश्लेषण करके [[जावा (प्रोग्रामिंग भाषा)]] प्रोग्राम में दौड़ की स्थिति और गतिरोध का पता लगाने के लिए एक उपकरण प्रस्तावित किया।
+प्रणाली या प्रोग्राम को निष्पादित करने के विरुद्ध औपचारिक या अनौपचारिक रूप से निर्दिष्ट गुणों की जाँच करना पुराना विषय है (उल्लेखनीय उदाहरण सॉफ़्टवेयर में [[गतिशील टाइपिंग]], या विफल-सुरक्षित उपकरण या हार्डवेयर में वॉचडॉग टाइमर हैं), जिनकी सटीक जड़ों की पहचान करना कठिन है। इस शब्दावली के लिए '''रनटाइम सत्यापन''' को औपचारिक रूप से 2001 की कार्यशाला के नाम के रूप में प्रस्तुत किया गया था<ref>{{cite web |url=http://runtime-verification.org/rv2001/index.html |title=RV'01 - रनटाइम सत्यापन पर पहली कार्यशाला|date=23 July 2001 |website=Runtime Verification Conferences |access-date=25 February 2017}}</ref> औपचारिक सत्यापन और परीक्षण के बीच सीमा पर समस्याओं का समाधान करने के उद्देश्य से किया जाता हैं। इस प्रकार बड़े कोड आधारों के लिए, मैन्युअल रूप से टेस्ट केस लिखने में बहुत समय लगता है। इस प्रकार इसके अतिरिक्त विकास के समय सभी त्रुटियों का पता नहीं लगाया जा सकता है। अंतरिक्ष यान, रोवर्स और एवियोनिक्स प्रौद्योगिकी में उच्च सुरक्षा मानकों को संग्रहीत करने के लिए क्लाउस हैवेलंड और [[ग्रेगरी रेड]] द्वारा नासा एम्स रिसर्च सेंटर में स्वचालित सत्यापन के लिए प्रारंभिक योगदान दिया गया था।<ref name="Havelund2001Overview">Klaus Havelund and Grigore Rosu. 2004. An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods in System Design, 24(2), March 2004.</ref> इस प्रकार उन्होंने टेम्पोरल लॉजिक में विनिर्देशों को सत्यापित करने और एकल निष्पादन पथों का विश्लेषण करके [[जावा (प्रोग्रामिंग भाषा)]] प्रोग्राम में रनटाइम की स्थिति और गतिरोध का पता लगाने के लिए उपकरण प्रस्तावित किया गया हैं।
-वर्तमान में, रनटाइम सत्यापन तकनीकों को अक्सर विभिन्न वैकल्पिक नामों के साथ प्रस्तुत किया जाता है, जैसे रनटाइम मॉनिटरिंग, रनटाइम चेकिंग, रनटाइम रिफ्लेक्शन, रनटाइम एनालिसिस, [[गतिशील कार्यक्रम विश्लेषण]], रनटाइम / डायनेमिक सिंबॉलिक एनालिसिस, ट्रेस एनालिसिस, लॉग फाइल एनालिसिस आदि। एक ही उच्च-स्तरीय अवधारणा के उदाहरण या तो विभिन्न क्षेत्रों में या विभिन्न समुदायों के विद्वानों द्वारा लागू होते हैं। रनटाइम सत्यापन अन्य अच्छी तरह से स्थापित क्षेत्रों से घनिष्ठ रूप से संबंधित है, जैसे परिनियोजन से पहले परीक्षण (विशेष रूप से मॉडल-आधारित परीक्षण) और परिनियोजन के दौरान उपयोग किए जाने पर दोष-सहिष्णु सिस्टम।
+वर्तमान में, रनटाइम सत्यापन तकनीकों को अधिकांशतः विभिन्न वैकल्पिक नामों के साथ प्रस्तुत किया जाता है, जैसे रनटाइम मॉनिटरिंग, रनटाइम चेकिंग, रनटाइम रिफ्लेक्शन, रनटाइम एनालिसिस, [[गतिशील कार्यक्रम विश्लेषण|गतिशील फंक्शन विश्लेषण]], रनटाइम / डायनेमिक सिंबॉलिक एनालिसिस, ट्रेस एनालिसिस, लॉग फाइल एनालिसिस आदि। इस प्रकार ही उच्च-स्तरीय अवधारणा के उदाहरण या तो विभिन्न क्षेत्रों में या विभिन्न समुदायों के विद्वानों द्वारा लागू होते हैं। रनटाइम सत्यापन अन्य अच्छी तरह से स्थापित क्षेत्रों से घनिष्ठ रूप से संबंधित है, जैसे परिनियोजन से पहले परीक्षण (विशेष रूप से मॉडल-आधारित परीक्षण) और परिनियोजन के समय उपयोग किए जाने पर दोष-सहिष्णु प्रणाली होती हैं।
 रनटाइम सत्यापन के व्यापक क्षेत्र के भीतर, कई श्रेणियों में अंतर किया जा सकता है, जैसे:
-* विनिर्देश-रहित निगरानी जो अधिकांशतः संगामिति-संबंधित गुणों जैसे परमाणुता के एक निश्चित सेट को लक्षित करती है। सैवेज एट अल द्वारा इस क्षेत्र में अग्रणी कार्य किया गया है। इरेज़र एल्गोरिथ्म के साथ<ref name="SavageTCS1997">Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. 1997. Eraser: a Dynamic Data Race Detector for Multithreaded Programs. ACM Trans. Comput. Syst. 15(4), November 1997, pp. 391-411.</ref>
+* विनिर्देश-रहित जाँच जो अधिकांशतः संगामिति-संबंधित गुणों जैसे परमाणुता के निश्चित सेट को लक्षित करती है। सैवेज एट अल द्वारा इस क्षेत्र में अग्रणी कार्य किया गया है। इरेज़र एल्गोरिथ्म के साथ किया जाता हैं।<ref name="SavageTCS1997">Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. 1997. Eraser: a Dynamic Data Race Detector for Multithreaded Programs. ACM Trans. Comput. Syst. 15(4), November 1997, pp. 391-411.</ref>
-* लौकिक तर्क विशिष्टताओं के संबंध में निगरानी; इस दिशा में प्रारंभिक योगदान ली, कन्नन और उनके सहयोगियों द्वारा किया गया है,<ref>Moonjoo Kim, Mahesh Viswanathan, Insup Lee, Hanêne Ben-Abdellah, Sampath Kannan, and Oleg Sokolsky, Formally Specified Monitoring of Temporal Properties, Proceedings of the European Conference on Real-Time Systems, June 1999.</ref><ref>Insup Lee, Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, Mahesh Viswanathan, Runtime Assurance Based On Formal Specifications, Proceedings of International Conference on Parallel and Distributed Processing Techniques and Applications, June 1999.</ref> और Havelund और Rosu,।<ref name="HavelundSPIN2000">Klaus Havelund, Using Runtime Analysis to Guide Model Checking of Java Programs, 7th International SPIN Workshop, August 2000.</ref><ref name="HavelundRosuASE2001">Klaus Havelund and Grigore Rosu, Monitoring Programs using Rewriting, Automated Software Engineering (ASE'01), November 2001.</ref>
+* लौकिक तर्क विशिष्टताओं के संबंध में जाँच; इस दिशा में प्रारंभिक योगदान ली, कन्नन और हैवलंड और रोजू, और उनके सहयोगियों द्वारा किया गया है।<ref>Moonjoo Kim, Mahesh Viswanathan, Insup Lee, Hanêne Ben-Abdellah, Sampath Kannan, and Oleg Sokolsky, Formally Specified Monitoring of Temporal Properties, Proceedings of the European Conference on Real-Time Systems, June 1999.</ref><ref>Insup Lee, Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, Mahesh Viswanathan, Runtime Assurance Based On Formal Specifications, Proceedings of International Conference on Parallel and Distributed Processing Techniques and Applications, June 1999.</ref><ref name="HavelundSPIN2000">Klaus Havelund, Using Runtime Analysis to Guide Model Checking of Java Programs, 7th International SPIN Workshop, August 2000.</ref><ref name="HavelundRosuASE2001">Klaus Havelund and Grigore Rosu, Monitoring Programs using Rewriting, Automated Software Engineering (ASE'01), November 2001.</ref>
 == मूल दृष्टिकोण ==
-[[File:Runtime Verification Monitor.svg|250px|thumb|right|रनटाइम सत्यापन पर एक ट्यूटोरियल में Falcone, Havelund और Reger द्वारा वर्णित मॉनिटर आधारित सत्यापन प्रक्रिया का अवलोकन।]]रनटाइम सत्यापन विधियों के व्यापक क्षेत्र को तीन आयामों द्वारा वर्गीकृत किया जा सकता है:<ref name="havelundRVTutorial2012" />* निष्पादन के दौरान ही (ऑनलाइन) या निष्पादन के बाद सिस्टम की निगरानी की जा सकती है। [[लॉग विश्लेषण]] (ऑफ़लाइन) के रूप में।
+[[File:Runtime Verification Monitor.svg|250px|thumb|right|रनटाइम सत्यापन पर ट्यूटोरियल में फैल्काॅन, हैवलंड और रीजर द्वारा वर्णित मॉनिटर आधारित सत्यापन प्रक्रिया का अवलोकन।]]'''रनटाइम सत्यापन''' विधियों के व्यापक क्षेत्र को तीन आयामों द्वारा वर्गीकृत किया जा सकता है:<ref name="havelundRVTutorial2012" />* निष्पादन के समय ही (ऑनलाइन) या निष्पादन के बाद प्रणाली की जाँच की जा सकती है। [[लॉग विश्लेषण]] (ऑफ़लाइन) के रूप में किया जाता हैं।
-* सत्यापन कोड सिस्टम में एकीकृत है (जैसा कि रनटाइम सत्यापन#आस्पेक्ट-ओरिएंटेड प्रोग्रामिंग|एस्पेक्ट-ओरिएंटेड प्रोग्रामिंग में किया गया है) या बाहरी इकाई के रूप में प्रदान किया गया है।
+* सत्यापन कोड प्रणाली में एकीकृत है (जैसा कि रनटाइम सत्यापन आस्पेक्ट-ओरिएंटेड प्रोग्रामिंग|एस्पेक्ट-ओरिएंटेड प्रोग्रामिंग में किया गया है) या बाहरी इकाई के रूप में प्रदान किया गया है।
 * मॉनिटर वांछित विनिर्देश के उल्लंघन या सत्यापन की रिपोर्ट कर सकता है।
 फिर भी, रनटाइम सत्यापन में मूल प्रक्रिया समान रहती है:<ref name="havelundRVTutorial2012">Yliès Falcone, Klaus Havelund and Giles, A Tutorial on Runtime Verification, 2013</ref>
-# कुछ औपचारिक विनिर्देशन से एक मॉनिटर बनाया जाता है। यह प्रक्रिया आमतौर पर स्वचालित रूप से की जा सकती है यदि संपत्ति में निर्दिष्ट [[औपचारिक भाषा]] के सूत्रों के लिए समकक्ष [[ऑटोमेटा]] हैं। एक नियमित अभिव्यक्ति को बदलने के लिए, एक परिमित-राज्य मशीन का उपयोग किया जा सकता है; रेखीय लौकिक तर्क में एक संपत्ति को बुची ऑटोमेटन में परिवर्तित किया जा सकता है (बुची ऑटोमेटन के लिए रैखिक लौकिक तर्क भी देखें)।
+# कुछ औपचारिक विनिर्देशन से मॉनिटर बनाया जाता है। यह प्रक्रिया सामान्यतः स्वचालित रूप से की जा सकती है यदि संपत्ति में निर्दिष्ट [[औपचारिक भाषा]] के सूत्रों के लिए समकक्ष [[ऑटोमेटा]] हैं। इस प्रकार नियमित अभिव्यक्ति को परिवर्तित करने के लिए, परिमित-स्थिति मशीन का उपयोग किया जा सकता है; रेखीय लौकिक तर्क में संपत्ति को बुची ऑटोमेटन (बुची ऑटोमेटन के लिए रैखिक लौकिक तर्क भी देखें) में परिवर्तित किया जा सकता है।
-# सिस्टम मॉनिटर को निष्पादन स्थिति से संबंधित घटनाओं को भेजने के लिए तैयार है।
+# प्रणाली मॉनिटर को निष्पादन स्थिति से संबंधित घटनाओं को भेजने के लिए तैयार है।
-# सिस्टम निष्पादित होता है और मॉनिटर द्वारा सत्यापित किया जाता है।
+# प्रणाली निष्पादित होता है और मॉनिटर द्वारा सत्यापित किया जाता है।
-# मॉनिटर प्राप्त घटना ट्रेस की पुष्टि करता है और एक निर्णय देता है कि विनिर्देश संतुष्ट है या नहीं। इसके अतिरिक्त, मॉनिटर गलत व्यवहार को संभावित रूप से ठीक करने के लिए सिस्टम को फीडबैक भेजता है। ऑफ़लाइन मॉनिटरिंग का उपयोग करते समय कॉज़ ऑफ़ कॉज़ कोई प्रतिक्रिया प्राप्त नहीं कर सकता है, क्योंकि सत्यापन बाद के समय में किया जाता है।
+# मॉनिटर प्राप्त घटना ट्रेस की पुष्टि करता है और निर्णय देता है कि विनिर्देश संतुष्ट है या नहीं इसका पता लगाया जाता हैं। इसके अतिरिक्त, मॉनिटर गलत व्यवहार को संभावित रूप से ठीक करने के लिए प्रणाली की फीडबैक भेजता है। इस प्रकार ऑफ़लाइन मॉनिटरिंग का उपयोग करते समय कॉज़ ऑफ़ कॉज़ कोई प्रतिक्रिया प्राप्त नहीं कर सकता है, क्योंकि सत्यापन बाद के समय में किया जाता है।
 == उदाहरण ==
-नीचे दिए गए उदाहरण कुछ सरल गुणों पर चर्चा करते हैं, जिन पर इस लेखन के समय (अप्रैल 2011) तक कई रनटाइम सत्यापन समूहों द्वारा संभवतः छोटे बदलावों के साथ विचार किया गया है। उन्हें और अधिक रोचक बनाने के लिए, नीचे दी गई प्रत्येक संपत्ति एक अलग विनिर्देश औपचारिकता का उपयोग करती है और ये सभी पैरामीट्रिक हैं। पैरामीट्रिक गुण पैरामीट्रिक घटनाओं के साथ बनने वाले निशान के बारे में गुण हैं, जो ऐसी घटनाएँ हैं जो डेटा को मापदंडों से बाँधती हैं। यहाँ एक पैरामीट्रिक संपत्ति का रूप है <math>\forall parameters : \varphi</math>, कहाँ <math>\varphi</math> सामान्य (अस्थिर) पैरामीट्रिक घटनाओं का जिक्र करते हुए कुछ उचित औपचारिकता में एक विनिर्देश है। ऐसे पैरामीट्रिक गुणों के लिए अंतर्ज्ञान यह है कि संपत्ति द्वारा व्यक्त की गई <math>\varphi</math> देखे गए ट्रेस में सभी पैरामीटर उदाहरणों (पैरामीट्रिक घटनाओं के माध्यम से) का सामना करना चाहिए। निम्नलिखित में से कोई भी उदाहरण किसी विशेष रनटाइम सत्यापन प्रणाली के लिए विशिष्ट नहीं है, हालांकि मापदंडों के लिए समर्थन स्पष्ट रूप से आवश्यक है। निम्नलिखित उदाहरणों में जावा सिंटैक्स माना जाता है, इस प्रकार == तार्किक समानता है, जबकि = असाइनमेंट है। कुछ तरीके (जैसे, <code>update()</code> UnsafeEnumExample में) डमी तरीके हैं, जो जावा एपीआई का हिस्सा नहीं हैं, जिनका उपयोग स्पष्टता के लिए किया जाता है।
+नीचे दिए गए उदाहरण कुछ सरल गुणों पर चर्चा करते हैं, जिन पर इस लेखन के समय (अप्रैल 2011) तक कई रनटाइम सत्यापन समूहों द्वारा संभवतः छोटे बदलावों के साथ विचार किया गया है। उन्हें और अधिक रोचक बनाने के लिए, नीचे दी गई प्रत्येक संपत्ति अलग विनिर्देश औपचारिकता का उपयोग करती है और ये सभी पैरामीट्रिक हैं। पैरामीट्रिक गुण पैरामीट्रिक घटनाओं के साथ बनने वाले निशान के बारे में गुण हैं, जो ऐसी घटनाएँ हैं जो डेटा को मापदंडों से बाँधती हैं। यहाँ पैरामीट्रिक संपत्ति <math>\forall parameters : \varphi</math> का रूप है, जहाँ <math>\varphi</math> सामान्य (अस्थिर) पैरामीट्रिक घटनाओं का जिक्र करते हुए कुछ उचित औपचारिकता में विनिर्देश है। ऐसे पैरामीट्रिक गुणों के लिए अंतर्ज्ञान यह है कि संपत्ति द्वारा व्यक्त की गई <math>\varphi</math> देखे गए ट्रेस में सभी पैरामीटर उदाहरणों (पैरामीट्रिक घटनाओं के माध्यम से) का सामना करना चाहिए। इस प्रकार निम्नलिखित में से कोई भी उदाहरण किसी विशेष रनटाइम सत्यापन प्रणाली के लिए विशिष्ट नहीं है, चूंकि मापदंडों के लिए समर्थन स्पष्ट रूप से आवश्यक है। निम्नलिखित उदाहरणों में जावा सिंटैक्स माना जाता है, इस प्रकार == तार्किक समानता को प्रदर्शित करता हैं, जबकि = असाइनमेंट को प्रदर्शित करता हैं। कुछ विधियाँ (जैसे, <code>update()</code> UnsafeEnumExample में) डमी विधियाँ हैं, जो जावा एपीआई का हिस्सा नहीं हैं, जिनका उपयोग स्पष्टता के लिए किया जाता है।
-=== अगला === है
+== has Next () ==
-[[File:Hasnext.jpg|right|thumb|350px|HasNext संपत्ति]]जावा [http://download.oracle.com/javase/6/docs/api/java/util/Iterator.html Iterator] इंटरफ़ेस के लिए आवश्यक है कि <code>hasNext()</code> विधि को बुलाया जाना चाहिए और इससे पहले सच हो जाना चाहिए <code>next()</code> पद्धति कहलाती है। यदि यह हो तो
+[[File:Hasnext.jpg|right|thumb|350px|HasNext संपत्ति]]जावा [http://download.oracle.com/javase/6/docs/api/java/util/Iterator.html इटरेटर] इंटरफ़ेस के लिए आवश्यक है कि <code>hasNext()</code> विधि को काॅल किया जाना चाहिए और इससे पहले सच हो जाना चाहिए <code>next()</code> पद्धति कहलाती है।
-ऐसा नहीं होता है, यह बहुत संभव है कि एक उपयोगकर्ता [http://download.oracle.com/javase/6/docs/api/java/util/Collection.html संग्रह] के अंत में पुनरावृति करेगा। दाईं ओर का आंकड़ा एक परिमित राज्य मशीन दिखाता है जो रनटाइम सत्यापन के साथ इस संपत्ति को जांचने और लागू करने के लिए संभावित मॉनीटर को परिभाषित करता है। अज्ञात स्थिति से, कॉल करने में हमेशा त्रुटि होती है <code>next()</code> विधि क्योंकि ऐसा ऑपरेशन असुरक्षित हो सकता है। अगर <code>hasNext()</code> कहा जाता है और <var>true</var> लौटाता है, कॉल करना सुरक्षित है <code>next()</code>, इसलिए मॉनिटर अधिक स्थिति में प्रवेश करता है। हालांकि, अगर <code>hasNext()</code> विधि <var>गलत</var> लौटाती है, कोई और तत्व नहीं हैं, और मॉनिटर 'कोई नहीं' स्थिति में प्रवेश करता है। अधिक और कोई नहीं राज्यों में, कॉलिंग <code>hasNext()</code> विधि कोई नई जानकारी प्रदान नहीं करती है। को कॉल करना सुरक्षित है <code>next()</code> अधिक स्थिति से विधि, लेकिन अधिक तत्व मौजूद होने पर यह अज्ञात हो जाता है, इसलिए मॉनिटर प्रारंभिक अज्ञात स्थिति में फिर से प्रवेश करता है। अंत में, बुला रहा है <code>next()</code> किसी भी स्थिति से विधि त्रुटि स्थिति में प्रवेश नहीं करती है। पैरामीट्रिक पास्ट टाइम लीनियर टेम्पोरल लॉजिक का उपयोग करते हुए इस संपत्ति का प्रतिनिधित्व क्या है।
+ऐसा नहीं होता है, यह बहुत संभव है कि उपयोगकर्ता [http://download.oracle.com/javase/6/docs/api/java/util/Collection.html संग्रह] के अंत में पुनरावृति करता हैं। इस प्रकार दाईं ओर का आंकड़ा परिमित स्थिति मशीन दिखाता है जो रनटाइम सत्यापन के साथ इस संपत्ति को जांचने और लागू करने के लिए संभावित मॉनीटर को परिभाषित करता है। इस प्रकार अज्ञात स्थिति से, कॉल करने में हमेशा त्रुटि होती है <code>next()</code> विधि क्योंकि ऐसा ऑपरेशन असुरक्षित हो सकता है। अगर <code>hasNext()</code> कहा जाता है और <var>true</var> लौटाता है, कॉल करना सुरक्षित है <code>next()</code>, इसलिए मॉनिटर अधिक स्थिति में प्रवेश करता है। चूंकि, अगर <code>hasNext()</code> विधि <var>गलत</var> लौटाती है, इसका कोई और तत्व नहीं हैं, और मॉनिटर 'कोई नहीं' स्थिति में प्रवेश करता है। इस प्रकार इससे अधिक और कोई नहीं होता हैं जिसकी स्थिति में, कॉलिंग <code>hasNext()</code> विधि कोई नई जानकारी प्रदान नहीं करती है। इसको कॉल करना सुरक्षित है <code>next()</code> इसकी अधिक स्थिति से इस विधि के एलिमेंट सम्मिलित होने पर यह अज्ञात हो जाता है, इसलिए मॉनिटर प्रारंभिक अज्ञात स्थिति में फिर से प्रवेश करता है। इस प्रकार अंत में इसे काॅल किया जाता हैं, <code>next()</code> किसी भी स्थिति से विधि त्रुटि स्थिति में प्रवेश नहीं करती है। पैरामीट्रिक पास्ट टाइम लीनियर टेम्पोरल लॉजिक का उपयोग करते हुए इस संपत्ति का प्रतिनिधित्व क्या है।
 <math>\forall ~ \text{Iterator} ~ i \quad i.\text{next}() ~ \rightarrow ~ \odot (i.\text{hasNext}() == true)</math>
-यह सूत्र कहता है कि किसी भी कॉल को <code>next()</code> विधि को तुरंत एक कॉल से पहले होना चाहिए <code>hasNext()</code> विधि जो सत्य लौटाती है। यहां की संपत्ति इटरेटर में पैरामीट्रिक है <code>i</code>. संकल्पनात्मक रूप से, इसका मतलब है कि परीक्षण कार्यक्रम में प्रत्येक संभावित इटरेटर के लिए मॉनिटर की एक प्रति होगी, हालांकि रनटाइम सत्यापन सिस्टम को अपने पैरामीट्रिक मॉनिटर को इस तरह लागू करने की आवश्यकता नहीं है। इस संपत्ति के लिए मॉनिटर एक हैंडलर को ट्रिगर करने के लिए सेट किया जाएगा जब सूत्र का उल्लंघन किया जाता है (समकक्ष जब परिमित राज्य मशीन त्रुटि स्थिति में प्रवेश करती है), जो कि तब होगा <code>next()</code> पहले कॉल किए बिना कॉल किया जाता है <code>hasNext()</code>, या जब <code>hasNext()</code> पूर्व कहा जाता है <code>next()</code>, लेकिन <var>false</var> लौटाया।
+यह सूत्र कहता है कि किसी भी कॉल को <code>next()</code> विधि को तुरंत कॉल से पहले होना चाहिए <code>hasNext()</code> विधि जो सत्य लौटाती है। यहां की संपत्ति इटरेटर <code>i</code> में पैरामीट्रिक है। इस संकल्पनात्मक रूप से, इसका आशय है कि परीक्षण फंक्शन में प्रत्येक संभावित इटरेटर के लिए मॉनिटर की प्रति होगी, चूंकि रनटाइम सत्यापन प्रणाली की अपने पैरामीट्रिक मॉनिटर को इस प्रकार लागू करने की आवश्यकता नहीं है। इस संपत्ति के लिए मॉनिटर हैंडलर को ट्रिगर करने के लिए सेट किया जाएगा जब सूत्र का उल्लंघन किया जाता है (समकक्ष जब परिमित स्थिति मशीन त्रुटि स्थिति में प्रवेश करती है), जो कि तब होगा <code>next()</code> पहले कॉल किए बिना कॉल किया जाता है <code>hasNext()</code>, या जब <code>hasNext()</code> पूर्व कहा जाता है <code>next()</code>, किन्तु <var>false</var> लौटाता हैं।
 === असुरक्षित ईनम ===
-[[File:Unsafeenumcode.png|right|thumb|350px|कोड जो असुरक्षित ईनम संपत्ति का उल्लंघन करता है]]जावा में [http://download.oracle.com/javase/6/docs/api/java/util/Vector.html वेक्टर] वर्ग के अपने तत्वों पर पुनरावृति के लिए दो साधन हैं। कोई भी इटरेटर इंटरफ़ेस का उपयोग कर सकता है, जैसा कि पिछले उदाहरण में देखा गया है, या कोई [http://download.oracle.com/javase/6/docs/api/java/util/Enumeration.html Enumeration] इंटरफ़ेस का उपयोग कर सकता है। Iterator इंटरफ़ेस के लिए निकालने की विधि को जोड़ने के अलावा, मुख्य अंतर यह है कि Iterator तेजी से विफल होता है जबकि Enumeration नहीं है। इसका मतलब यह है कि यदि कोई वेक्टर को संशोधित करता है (इटरेटर हटाने की विधि का उपयोग करने के अलावा) जब कोई इटरेटर का उपयोग करके वेक्टर पर पुनरावृति करता है, तो एक [http://download.oracle.com/javase/6/docs/api /java/util/ConcurrentModificationException.html ConcurrentModificationException] फेंका गया है। हालाँकि, गणना का उपयोग करते समय यह एक मामला नहीं है, जैसा कि उल्लेख किया गया है। इसका परिणाम एक कार्यक्रम से गैर-नियतात्मक परिणाम हो सकता है क्योंकि वेक्टर को गणना के परिप्रेक्ष्य से असंगत स्थिति में छोड़ दिया जाता है। लीगेसी प्रोग्राम के लिए जो अभी भी गणना इंटरफ़ेस का उपयोग करते हैं, कोई यह लागू करना चाह सकता है कि जब उनके अंतर्निहित वेक्टर को संशोधित किया जाता है तो गणना का उपयोग नहीं किया जाता है। इस व्यवहार को लागू करने के लिए निम्नलिखित पैरामीट्रिक नियमित पैटर्न का उपयोग किया जा सकता है:
+[[File:Unsafeenumcode.png|right|thumb|350px|कोड जो असुरक्षित ईनम संपत्ति का उल्लंघन करता है]]जावा में [http://download.oracle.com/javase/6/docs/api/java/util/Vector.html वेक्टर] वर्ग के अपने तत्वों पर पुनरावृति के लिए दो साधन हैं। कोई भी इटरेटर इंटरफ़ेस का उपयोग कर सकता है, जैसा कि पिछले उदाहरण में देखा गया है, या कोई [http://download.oracle.com/javase/6/docs/api/java/util/Enumeration.html इनुम्रेशन] इंटरफ़ेस का उपयोग कर सकता है। इटरेटर इंटरफ़ेस के लिए निकालने की विधि को जोड़ने के अतिरिक्त, मुख्य अंतर यह है कि इटरेटर तेजी से विफल होता है जबकि इनुमरेशन नहीं है। इसका अर्थ यह है कि यदि कोई वेक्टर को संशोधित करता है (इटरेटर हटाने की विधि का उपयोग करने के अतिरिक्त) इस प्रकार जब कोई इटरेटर का उपयोग करके वेक्टर पर पुनरावृति करता है, तो [http://download.oracle.com/javase/6/docs/api /java/util/ConcurrentModificationException.html ConcurrentModificationException] फेंका गया है। चूंकि, गणना का उपयोग करते समय यह स्थिति नहीं है, जैसा कि उल्लेख किया गया है। इसका परिणाम फंक्शन से गैर-नियतात्मक परिणाम हो सकता है क्योंकि वेक्टर को गणना के परिप्रेक्ष्य से असंगत स्थिति में छोड़ दिया जाता है। इस प्रकार लीगेसी प्रोग्राम के लिए जो अभी भी गणना इंटरफ़ेस का उपयोग करते हैं, कोई यह लागू करना चाह सकता है कि जब उनके अंतर्निहित वेक्टर को संशोधित किया जाता है तो गणना का उपयोग नहीं किया जाता है। इस व्यवहार को लागू करने के लिए निम्नलिखित पैरामीट्रिक नियमित पैटर्न का उपयोग किया जा सकता है:
 : ∀ वेक्टर वी, गणना ई: (ई = v.elements ()) (e.nextElement ())<sup>*</sup> v.update() e.nextElement()
-यह पैटर्न गणना और वेक्टर दोनों में पैरामीट्रिक है। सहज रूप से, और जैसा कि उपरोक्त रनटाइम सत्यापन सिस्टम को अपने पैरामीट्रिक मॉनिटर को इस तरह से लागू करने की आवश्यकता नहीं है, कोई इस संपत्ति के लिए पैरामीट्रिक मॉनिटर को वेक्टर और गणना के प्रत्येक संभावित जोड़े के लिए एक गैर-पैरामीट्रिक मॉनिटर उदाहरण बनाने और ट्रैक करने के बारे में सोच सकता है। कुछ घटनाएं एक ही समय में कई मॉनीटरों से संबंधित हो सकती हैं, जैसे <code>v.update()</code>, इसलिए रनटाइम सत्यापन प्रणाली को (फिर से वैचारिक रूप से) उन्हें सभी इच्छुक मॉनिटरों को भेजना चाहिए। यहां संपत्ति निर्दिष्ट की गई है ताकि यह कार्यक्रम के खराब व्यवहारों को बताए। पैटर्न के मिलान के लिए इस संपत्ति की निगरानी की जानी चाहिए। दाईं ओर का आंकड़ा जावा कोड दिखाता है जो इस पैटर्न से मेल खाता है, इस प्रकार संपत्ति का उल्लंघन करता है। वेक्टर, वी, गणना के बाद अद्यतन किया जाता है, ई, बनाया जाता है, और फिर ई का उपयोग किया जाता है।
+यह पैटर्न गणना और वेक्टर दोनों में पैरामीट्रिक है। सहज रूप से, और जैसा कि उपरोक्त रनटाइम सत्यापन प्रणाली की अपने पैरामीट्रिक मॉनिटर को इस तरह से लागू करने की आवश्यकता नहीं है, कोई इस संपत्ति के लिए पैरामीट्रिक मॉनिटर को वेक्टर और गणना के प्रत्येक संभावित जोड़े के लिए गैर-पैरामीट्रिक मॉनिटर उदाहरण बनाने और ट्रैक करने के बारे में सोच सकता है। कुछ घटनाएं ही समय में कई मॉनीटरों से संबंधित हो सकती हैं, जैसे <code>v.update()</code>, इसलिए रनटाइम सत्यापन प्रणाली की (फिर से वैचारिक रूप से) उन्हें सभी इच्छुक मॉनिटरों को भेजना चाहिए। इस प्रकार यहां संपत्ति निर्दिष्ट की गई है जिससे कि यह फंक्शन के बुरे व्यवहारों को बताता हैं। इस पैटर्न के मिलान के लिए इस संपत्ति की जाँच की जानी चाहिए। दाईं ओर का आंकड़ा जावा कोड दिखाता है जो इस पैटर्न से मेल खाता है, इस प्रकार संपत्ति का उल्लंघन करता है। वेक्टर, वी, गणना के बाद अद्यतन किया जाता है, यहाँ पर इसे ई बनाया जाता है, और फिर ई का उपयोग किया जाता है।
-<!---
-<code lang="java">
-Vector<String> v = new Vector();
-v.add("hello");
-v.add("world");
-v.add("again");
-Enumeration<String> e = v.elements();
-String s = "";
-v.add("bad!");
-while (e.hasMoreElements()) {
-    s = e.nextElement();
-    System.out.println(s);
-}
-</code>
--->
 === सेफलॉक ===
-पिछले दो उदाहरण परिमित स्थिति गुणों को दिखाते हैं, लेकिन रनटाइम सत्यापन में उपयोग की जाने वाली संपत्तियां अधिक जटिल हो सकती हैं। सेफ लॉक संपत्ति नीति को लागू करती है कि किसी (पुनः प्रवेशी) लॉक क्लास के अधिग्रहण और रिलीज की संख्या किसी दिए गए विधि कॉल के भीतर मेल खाती है। बेशक, यह उन तरीकों के अलावा अन्य तरीकों से तालों को जारी करने की अनुमति नहीं देता है जो उन्हें प्राप्त करते हैं, लेकिन यह संभवतः परीक्षण प्रणाली को प्राप्त करने के लिए एक वांछनीय लक्ष्य है। पैरामीट्रिक संदर्भ-मुक्त पैटर्न का उपयोग करते हुए इस संपत्ति का विवरण नीचे दिया गया है:
+पिछले दो उदाहरण परिमित स्थिति गुणों को दिखाते हैं, किन्तु रनटाइम सत्यापन में उपयोग की जाने वाली संपत्तियां अधिक जटिल हो सकती हैं। इस प्रकार सेफ लॉक संपत्ति नीति को लागू करती है कि किसी (पुनः प्रवेशी) लॉक क्लास के अधिग्रहण और रिलीज की संख्या किसी दिए गए विधि कॉल के भीतर मेल खाती है। मुख्य रूप से यह उन तरीकों के अतिरिक्त अन्य विधियों से लाॅक को प्रस्तुत करने की अनुमति नहीं देता है जो उन्हें प्राप्त करते हैं, किन्तु यह संभवतः परीक्षण प्रणाली की प्राप्त करने के लिए वांछनीय लक्ष्य है। इस प्रकार पैरामीट्रिक संदर्भ-मुक्त पैटर्न का उपयोग करते हुए इस संपत्ति का विवरण नीचे दिया गया है:
-: ∀ थ्रेड टी, लॉक एल: एस → ε | एस शुरू (टी) एस अंत (टी) | एस एल अधिग्रहण (टी) एस एल रिलीज (टी)
+: ∀ Thread T, Lock L: S → ε | S start (T) S end (T) | S L अधिग्रहण (T) S L रिलीज (T)
-[[File:Safelocktrace.jpg|right|thumb|350px|सेफलॉक संपत्ति के दो उल्लंघनों को दर्शाने वाला ट्रेस।]]पैटर्न प्रत्येक थ्रेड और लॉक के लिए नेस्टेड प्रारंभ/समाप्ति और अधिग्रहण/रिलीज जोड़े के संतुलित अनुक्रम निर्दिष्ट करता है (<math>\epsilon</math> खाली क्रम है)। यहां प्रारंभ और अंत कार्यक्रम में प्रत्येक विधि की शुरुआत और अंत को संदर्भित करता है (स्वयं को प्राप्त करने और जारी करने के लिए कॉल को छोड़कर)। वे थ्रेड में पैरामीट्रिक हैं क्योंकि विधियों की शुरुआत और अंत को जोड़ना आवश्यक है यदि और केवल तभी जब वे एक ही थ्रेड से संबंधित हों। उसी कारण से थ्रेड में अधिग्रहण और रिलीज़ इवेंट भी पैरामीट्रिक हैं। वे, अतिरिक्त रूप से, लॉक में पैरामीट्रिक हैं क्योंकि हम एक लॉक की रिलीज़ को दूसरे के अधिग्रहण के साथ संबद्ध नहीं करना चाहते हैं। अत्यधिक में, यह संभव है कि संपत्ति का एक उदाहरण होगा, अर्थात, थ्रेड के साथ लॉक के प्रत्येक संभावित संयोजन के लिए संदर्भ-मुक्त पार्सिंग तंत्र की एक प्रति; यह फिर से, सहज रूप से होता है, क्योंकि रनटाइम सत्यापन सिस्टम समान कार्यक्षमता को अलग तरीके से लागू कर सकते हैं। उदाहरण के लिए, यदि किसी सिस्टम में थ्रेड्स हैं <math>t_1</math>, <math>t_2</math>, और <math>t_3</math> ताले के साथ <math>l_1</math> और <math>l_2</math>, तो जोड़े < के लिए संपत्ति के उदाहरणों को बनाए रखना संभव है<math>t_1</math>,<math>l_1</math>>, <<math>t_1</math>,<math>l_2</math>>, <<math>t_2</math>,<math>l_1</math>>, <<math>t_2</math>,<math>l_2</math>>, <<math>t_3</math>,<math>l_1</math>>, और <<math>t_3</math>,<math>l_2</math>>। पैटर्न से मिलान करने में विफलताओं के लिए इस संपत्ति की निगरानी की जानी चाहिए क्योंकि पैटर्न सही व्यवहार निर्दिष्ट करता है। दाईं ओर का आंकड़ा एक निशान दिखाता है जो इस संपत्ति के दो उल्लंघनों का उत्पादन करता है। नीचे दिए गए चरण एक विधि की शुरुआत का प्रतिनिधित्व करते हैं, जबकि ऊपर के चरण अंत हैं। चित्र में ग्रे तीर एक ही लॉक के दिए गए अधिग्रहण और रिलीज के बीच मिलान दिखाते हैं। सादगी के लिए, ट्रेस केवल एक थ्रेड और एक लॉक दिखाता है।
+[[File:Safelocktrace.jpg|right|thumb|350px|सेफलॉक संपत्ति के दो उल्लंघनों को दर्शाने वाला ट्रेस।]]पैटर्न प्रत्येक थ्रेड और लॉक के लिए नेस्टेड प्रारंभ/समाप्ति और अधिग्रहण/रिलीज जोड़े के संतुलित अनुक्रम निर्दिष्ट  (<math>\epsilon</math> खाली क्रम है) करता है। यहां प्रारंभ और अंत फंक्शन में प्रत्येक विधि के प्रारंभ और अंत को संदर्भित करता है, इस प्रकार यह स्वयं को प्राप्त करने और प्रस्तुत करने के लिए कॉल को छोड़कर किया जाता हैं। वे थ्रेड में पैरामीट्रिक हैं क्योंकि विधियों के प्रारंभ और अंत को जोड़ना आवश्यक है यदि और केवल तभी जब वे ही थ्रेड से संबंधित हों। उसी कारण से थ्रेड में अधिग्रहण और रिलीज़ इवेंट भी पैरामीट्रिक हैं। इसके अतिरिक्त लॉक में पैरामीट्रिक स्थिति होती हैं क्योंकि हम लॉक की रिलीज़ को दूसरे के अधिग्रहण के साथ संबद्ध नहीं करना चाहते हैं। इसकी उत्तम स्थिति में, यह संभव है कि संपत्ति का उदाहरण होगा, अर्थात, थ्रेड के साथ लॉक के प्रत्येक संभावित संयोजन के लिए संदर्भ-मुक्त पार्सिंग प्रणाली की प्रति; यह फिर से, सहज रूप से होता है, क्योंकि रनटाइम सत्यापन प्रणाली समान कार्यक्षमता को अलग तरीके से लागू कर सकते हैं। उदाहरण के लिए, यदि किसी प्रणाली में थ्रेड्स हैं <math>t_1</math>, <math>t_2</math>, और <math>t_3</math> लाॅक के साथ <math>l_1</math> और <math>l_2</math>, तो जोड़े < के लिए संपत्ति के उदाहरणों <math>t_1</math>,<math>l_1</math>>, <<math>t_1</math>,<math>l_2</math>>, <<math>t_2</math>,<math>l_1</math>>, <<math>t_2</math>,<math>l_2</math>>, <<math>t_3</math>,<math>l_1</math>>, और <<math>t_3</math>,<math>l_2</math>> को बनाए रखना संभव है। पैटर्न से मिलान करने में विफलताओं के लिए इस संपत्ति की जाँच की जानी चाहिए क्योंकि पैटर्न सही व्यवहार निर्दिष्ट करता है। इस प्रकार दाईं ओर का आंकड़ा निशान दिखाता है जो इस संपत्ति के दो उल्लंघनों का उत्पादन करता है। इस प्रकार नीचे दिए गए चरण विधि के प्रारंभ का प्रतिनिधित्व करते हैं, जबकि ऊपर के चरण अंत हैं। चित्र में ग्रे तीर ही लॉक के दिए गए अधिग्रहण और रिलीज के बीच मिलान दिखाते हैं। इसके लिए ट्रेस केवल थ्रेड और लॉक दिखाता है।
 == अनुसंधान चुनौतियाँ और अनुप्रयोग ==
-अधिकांश रनटाइम सत्यापन शोध नीचे सूचीबद्ध एक या अधिक विषयों को संबोधित करते हैं।
+अधिकांश '''रनटाइम सत्यापन''' शोध नीचे सूचीबद्ध या अधिक विषयों को संबोधित करते हैं।
 === रनटाइम ओवरहेड कम करना ===
-एक निष्पादन प्रणाली का अवलोकन करने में आमतौर पर कुछ रनटाइम ओवरहेड होता है (हार्डवेयर मॉनिटर एक अपवाद बना सकता है)। जितना संभव हो सके रनटाइम सत्यापन उपकरणों के ओवरहेड को कम करना महत्वपूर्ण है, खासकर जब उत्पन्न मॉनिटर सिस्टम के साथ तैनात किए जाते हैं। रनटाइम ओवरहेड कम करने वाली तकनीकों में शामिल हैं:
+एक निष्पादन प्रणाली का अवलोकन करने में सामान्यतः कुछ रनटाइम ओवरहेड होता है जो हार्डवेयर मॉनिटर अपवाद बना सकता है। इस प्रकार जितना संभव हो सके रनटाइम सत्यापन उपकरणों के ओवरहेड को कम करना महत्वपूर्ण है, मुख्यकर जब उत्पन्न मॉनिटर प्रणाली के साथ तैनात किए जाते हैं। इस प्रकार इसमें रनटाइम ओवरहेड कम करने वाली तकनीकों में सम्मिलित हैं:
-* ''बेहतर उपकरण''। निष्पादन प्रणाली से घटनाओं को निकालने और उन्हें मॉनिटर पर भेजने से बड़े रनटाइम ओवरहेड उत्पन्न हो सकते हैं यदि भोलेपन से किया जाता है। किसी भी रनटाइम सत्यापन उपकरण के लिए अच्छा सिस्टम इंस्ट्रूमेंटेशन महत्वपूर्ण है, जब तक कि उपकरण मौजूदा निष्पादन लॉग को स्पष्ट रूप से लक्षित न करे। वर्तमान उपयोग में कई इंस्ट्रूमेंटेशन दृष्टिकोण हैं, प्रत्येक अपने फायदे और नुकसान के साथ, कस्टम या मैनुअल इंस्ट्रूमेंटेशन से लेकर विशेष पुस्तकालयों तक, आस्पेक्ट-ओरिएंटेड भाषाओं में संकलन करने के लिए, वर्चुअल मशीन को बढ़ाने के लिए, हार्डवेयर सपोर्ट पर निर्माण करने के लिए।
+* ''उत्तम उपकरण''। निष्पादन प्रणाली से घटनाओं को निकालने और उन्हें मॉनिटर पर भेजने से बड़े रनटाइम ओवरहेड उत्पन्न हो सकते हैं यदि भोलेपन से किया जाता है। किसी भी रनटाइम सत्यापन उपकरण के लिए अच्छा प्रणाली इंस्ट्रूमेंटेशन महत्वपूर्ण है, जब तक कि उपकरण मौजूदा निष्पादन लॉग को स्पष्ट रूप से लक्षित नहीं करते हैं। इस प्रकार वर्तमान उपयोग में कई इंस्ट्रूमेंटेशन दृष्टिकोण हैं, प्रत्येक अपने लाभ और हानि के साथ, कस्टम या मैनुअल इंस्ट्रूमेंटेशन से लेकर विशेष लाइब्रेरीज तक, आस्पेक्ट-ओरिएंटेड भाषाओं में संकलन करने के लिए, वर्चुअल मशीन को बढ़ाने के लिए, हार्डवेयर सपोर्ट पर निर्माण करने के लिए किया जाता हैं।
-* ''स्थैतिक विश्लेषण के साथ संयोजन''। एक साधारण{{Citation needed|date=November 2011}} स्थैतिक और गतिशील विश्लेषणों का संयोजन, विशेष रूप से संकलकों में सामना करना, उन सभी आवश्यकताओं की निगरानी करना है जिन्हें स्थिर रूप से निर्वहन नहीं किया जा सकता है। एक दोहरी और अंततः समतुल्य दृष्टिकोण आदर्श बन जाता है{{Citation needed|date=November 2011}} रनटाइम सत्यापन में, अर्थात् संपूर्ण निगरानी की मात्रा को कम करने के लिए [[स्थैतिक कार्यक्रम विश्लेषण]] का उपयोग करने के लिए। निगरानी की जाने वाली संपत्ति और निगरानी की जाने वाली प्रणाली दोनों पर स्थैतिक विश्लेषण किया जा सकता है। मॉनिटर करने के लिए संपत्ति के स्थैतिक विश्लेषण से पता चलता है कि कुछ घटनाएं निगरानी के लिए अनावश्यक हैं, कि कुछ मॉनिटरों के निर्माण में देरी हो सकती है, और यह कि कुछ मौजूदा मॉनिटर कभी ट्रिगर नहीं होंगे और इस प्रकार कचरा एकत्र किया जा सकता है। मॉनिटर करने के लिए सिस्टम का स्थिर विश्लेषण कोड का पता लगा सकता है जो मॉनिटर को कभी प्रभावित नहीं कर सकता है। उदाहरण के लिए, उपरोक्त HasNext संपत्ति की निगरानी करते समय, किसी को कोड के उपकरण भागों की आवश्यकता नहीं होती है जहां प्रत्येक कॉल होती है <code>i.next()</code> कॉल द्वारा किसी भी रास्ते पर तुरंत पहले होता है <code>i.hasnext()</code> जो <var>true</var> लौटाता है (नियंत्रण-प्रवाह ग्राफ़ पर दिखाई देता है)।
+* ''स्थैतिक विश्लेषण के साथ संयोजन''। साधारण स्थैतिक और गतिशील विश्लेषणों का संयोजन, विशेष रूप से संकलकों में सामना करना, उन सभी आवश्यकताओं की जाँच करना है जिन्हें स्थिर रूप से निर्वहन नहीं किया जा सकता है। दोहरी और अंततः समतुल्य दृष्टिकोण आदर्श बन जाता है रनटाइम सत्यापन में, अर्थात् संपूर्ण जाँच की मात्रा को कम करने के लिए [[स्थैतिक कार्यक्रम विश्लेषण|स्थैतिक फंक्शन विश्लेषण]] का उपयोग करने के लिए। जाँच की जाने वाली संपत्ति और जाँच की जाने वाली प्रणाली दोनों पर स्थैतिक विश्लेषण किया जा सकता है। इस प्रकार मॉनिटर करने के लिए संपत्ति के स्थैतिक विश्लेषण से पता चलता है कि कुछ घटनाएं जाँच के लिए अनावश्यक हैं, कि कुछ मॉनिटरों के निर्माण में देरी हो सकती है, और यह कि कुछ मौजूदा मॉनिटर कभी ट्रिगर नहीं होंगे और इस प्रकार कचरा एकत्र किया जा सकता है। मॉनिटर करने के लिए प्रणाली का स्थिर विश्लेषण कोड का पता लगा सकता है जो मॉनिटर को कभी प्रभावित नहीं कर सकता है। उदाहरण के लिए, उपरोक्त HasNext संपत्ति की जाँच करते समय, किसी को कोड के उपकरण भागों की आवश्यकता नहीं होती है जहां प्रत्येक कॉल होती है <code>i.next()</code> कॉल द्वारा किसी भी रास्ते पर तुरंत <code>i.hasnext()</code> फंक्शन पहले होता है जो <var>true</var> मान लौटाता है, यह मुख्य रूप से नियंत्रण-प्रवाह ग्राफ़ पर दिखाई देता है।
-* ''कुशल मॉनिटर निर्माण और प्रबंधन''। उपरोक्त उदाहरणों में पैरामीट्रिक गुणों की निगरानी करते समय, निगरानी प्रणाली को प्रत्येक पैरामीटर उदाहरण के संबंध में निगरानी की गई संपत्ति की स्थिति का ट्रैक रखने की आवश्यकता होती है। ऐसे उदाहरणों की संख्या सैद्धांतिक रूप से अबाध है और व्यवहार में बहुत अधिक हो जाती है। एक महत्वपूर्ण शोध चुनौती यह है कि कैसे देखी गई घटनाओं को कुशलतापूर्वक उन घटनाओं को ठीक से प्रेषित किया जाए जिनकी उन्हें आवश्यकता है। एक संबंधित चुनौती यह है कि ऐसे उदाहरणों की संख्या को कैसे कम रखा जाए (ताकि प्रेषण तेजी से हो), या दूसरे शब्दों में, यथासंभव लंबे समय तक अनावश्यक उदाहरण बनाने से कैसे बचा जाए और साथ ही, पहले से बनाए गए उदाहरणों को जल्द से जल्द कैसे हटाया जाए वे अनावश्यक हो जाते हैं। अंत में, पैरामीट्रिक मॉनिटरिंग एल्गोरिदम आम तौर पर गैर-पैरामीट्रिक मॉनिटर बनाने के लिए समान एल्गोरिदम का सामान्यीकरण करते हैं। इस प्रकार, उत्पन्न गैर-पैरामीट्रिक मॉनिटर की गुणवत्ता परिणामी पैरामीट्रिक मॉनिटर की गुणवत्ता तय करती है। हालाँकि, अन्य सत्यापन विधियों (जैसे, मॉडल जाँच) के विपरीत, रनटाइम सत्यापन में राज्यों की संख्या या उत्पन्न मॉनिटर का आकार कम महत्वपूर्ण है; वास्तव में, कुछ मॉनिटरों में असीम रूप से कई अवस्थाएँ हो सकती हैं, जैसे कि उपरोक्त SafeLock संपत्ति के लिए, हालाँकि किसी भी समय केवल राज्यों की सीमित संख्या हो सकती है। महत्वपूर्ण यह है कि निष्पादन प्रणाली से एक घटना प्राप्त होने पर मॉनिटर एक राज्य से अपने अगले राज्य में कितनी कुशलता से स्थानांतरित होता है।
+* ''कुशल मॉनिटर निर्माण और प्रबंधन के लिए उपयोग किया जाता हैं, इस प्रकार'' उपरोक्त उदाहरणों में पैरामीट्रिक गुणों की जाँच करते समय, जाँच प्रणाली की प्रत्येक पैरामीटर उदाहरण के संबंध में जाँच की गई संपत्ति की स्थिति का ट्रैक रखने की आवश्यकता होती है। ऐसे उदाहरणों की संख्या सैद्धांतिक रूप से अबाध है और इस प्रकार व्यवहार में बहुत अधिक हो जाती है। इसकी महत्वपूर्ण शोध चुनौती यह है कि कैसे देखी गई घटनाओं को कुशलतापूर्वक उन घटनाओं को ठीक से प्रेषित किया जाए जिनकी उन्हें आवश्यकता है। इस प्रकार संबंधित चुनौती यह है कि ऐसे उदाहरणों की संख्या को कैसे कम रखा जाए (जिससे कि प्रेषण तेजी से हो), या दूसरे शब्दों में, यथासंभव लंबे समय तक अनावश्यक उदाहरण बनाने से कैसे बचा जाए और साथ ही, पहले से बनाए गए उदाहरणों को जल्द से जल्द कैसे हटाया जाए वे अनावश्यक हो जाते हैं। अंत में, पैरामीट्रिक मॉनिटरिंग एल्गोरिदम सामान्यतः गैर-पैरामीट्रिक मॉनिटर बनाने के लिए समान एल्गोरिदम का सामान्यीकरण करते हैं। इस प्रकार, उत्पन्न गैर-पैरामीट्रिक मॉनिटर की गुणवत्ता परिणामी पैरामीट्रिक मॉनिटर की गुणवत्ता तय करती है। चूंकि, अन्य सत्यापन विधियों (जैसे, मॉडल जाँच) के विपरीत, रनटाइम सत्यापन में स्थिति की संख्या या उत्पन्न मॉनिटर का आकार कम महत्वपूर्ण है; वास्तव में, कुछ मॉनिटरों में अधिकता से कई अवस्थाएँ हो सकती हैं, जैसे कि उपरोक्त सेफ लाॅक संपत्ति के लिए, चूंकि किसी भी समय केवल स्थिति की सीमित संख्या हो सकती है। महत्वपूर्ण यह है कि निष्पादन प्रणाली से घटना प्राप्त होने पर मॉनिटर स्थिति से अपने अगले स्थिति में कितनी कुशलता से स्थानांतरित होता है।
 === गुण निर्दिष्ट करना ===
-सभी औपचारिक दृष्टिकोणों की प्रमुख व्यावहारिक बाधाओं में से एक यह है कि उनके उपयोगकर्ता अनिच्छुक हैं, या नहीं जानते हैं और यह नहीं सीखना चाहते हैं कि विनिर्देशों को कैसे पढ़ना या लिखना है। कुछ मामलों में विनिर्देश अंतर्निहित होते हैं, जैसे गतिरोध और डेटा-रेस के लिए, लेकिन ज्यादातर मामलों में उन्हें उत्पादित करने की आवश्यकता होती है। एक अतिरिक्त असुविधा, विशेष रूप से रनटाइम सत्यापन के संदर्भ में, यह है कि कई मौजूदा विनिर्देश भाषाएं अभीष्ट गुणों को पकड़ने के लिए पर्याप्त अभिव्यंजक नहीं हैं।
+सभी औपचारिक दृष्टिकोणों की प्रमुख व्यावहारिक बाधाओं में से यह है कि उनके उपयोगकर्ता अनिच्छुक हैं, या नहीं जानते हैं और यह नहीं सीखना चाहते हैं कि विनिर्देशों को कैसे पढ़ना या लिखना है। कुछ स्थितियों में विनिर्देश अंतर्निहित होते हैं, जैसे गतिरोध और डेटा-रेस के लिए, किन्तु ज्यादातर स्थितियों में उन्हें उत्पादित करने की आवश्यकता होती है। इस प्रकार इसके अतिरिक्त असुविधा, विशेष रूप से रनटाइम सत्यापन के संदर्भ में, यह है कि कई मौजूदा विनिर्देश भाषाएं अभीष्ट गुणों को पकड़ने के लिए पर्याप्त अभिव्यंजक नहीं हैं।
-* ''बेहतर औपचारिकताएं।'' रनटाइम सत्यापन समुदाय में काम की एक महत्वपूर्ण राशि डिजाइनिंग विनिर्देश औपचारिकता में डाल दी गई है जो पारंपरिक विनिर्देश औपचारिकताओं की तुलना में रनटाइम सत्यापन के लिए वांछित एप्लिकेशन डोमेन को बेहतर बनाती है। इनमें से कुछ में पारंपरिक औपचारिकताओं में मामूली या कोई वाक्यात्मक परिवर्तन नहीं है, लेकिन केवल उनके शब्दार्थ (जैसे, परिमित ट्रेस बनाम अनंत ट्रेस शब्दार्थ, आदि) में परिवर्तन और उनके कार्यान्वयन (बुची ऑटोमेटा, आदि के बजाय अनुकूलित परिमित राज्य मशीन) शामिल हैं। .). अन्य मौजूदा औपचारिकताओं को उन सुविधाओं के साथ विस्तारित करते हैं जो रनटाइम सत्यापन के लिए अनुकूल हैं लेकिन अन्य सत्यापन दृष्टिकोणों के लिए आसानी से नहीं हो सकते हैं, जैसे उपरोक्त उदाहरणों में देखा गया पैरामीटर जोड़ना। अंत में, विनिर्देश औपचारिकताएं हैं जो विशेष रूप से रनटाइम सत्यापन के लिए डिज़ाइन की गई हैं, इस डोमेन के लिए अपना सर्वश्रेष्ठ हासिल करने का प्रयास करते हैं और अन्य एप्लिकेशन डोमेन के बारे में बहुत कम ध्यान रखते हैं। रनटाइम सत्यापन के लिए सार्वभौमिक रूप से बेहतर या डोमेन-विशेष रूप से बेहतर विनिर्देश औपचारिकताओं को डिजाइन करना इसकी प्रमुख शोध चुनौतियों में से एक है और रहेगा।
+* ''उत्तम औपचारिकताएं।'' रनटाइम सत्यापन समुदाय में कार्य की महत्वपूर्ण राशि डिजाइनिंग विनिर्देश औपचारिकता में डाल दी गई है जो पारंपरिक विनिर्देश औपचारिकताओं की तुलना में रनटाइम सत्यापन के लिए वांछित एप्लिकेशन डोमेन को उत्तम बनाती है। इस प्रकार इनमें से कुछ में पारंपरिक औपचारिकताओं में मामूली या कोई वाक्यात्मक परिवर्तन नहीं है, किन्तु केवल उनके शब्दार्थ (जैसे, परिमित ट्रेस बनाम अनंत ट्रेस शब्दार्थ, आदि) में परिवर्तन और उनके कार्यान्वयन (बुची ऑटोमेटा, आदि के अतिरिक्त अनुकूलित परिमित स्थिति मशीन) सम्मिलित हैं।) इस प्रकार अन्य मौजूदा औपचारिकताओं को उन सुविधाओं के साथ विस्तारित करते हैं जो रनटाइम सत्यापन के लिए अनुकूल हैं किन्तु अन्य सत्यापन दृष्टिकोणों के लिए सरलता से नहीं हो सकते हैं, जैसे उपरोक्त उदाहरणों में देखा गया पैरामीटर जोड़ना इसका एक उदाहरण हैं। अंत में, विनिर्देश औपचारिकताएं हैं जो विशेष रूप से रनटाइम सत्यापन के लिए डिज़ाइन की गई हैं, इस प्रकार इसकी डोमेन के लिए अपना सर्वश्रेष्ठ प्राप्त करने का प्रयास करते हैं और अन्य एप्लिकेशन डोमेन के बारे में बहुत कम ध्यान रखते हैं। रनटाइम सत्यापन के लिए सार्वभौमिक रूप से उत्तम या डोमेन-विशेष रूप से उत्तम विनिर्देश औपचारिकताओं को डिजाइन करना इसकी प्रमुख शोध चुनौतियों में से है और इसी प्रकार रहेगा।
-* ''मात्रात्मक गुण।'' अन्य सत्यापन दृष्टिकोणों की तुलना में, रनटाइम सत्यापन सिस्टम स्टेट वेरिएबल्स के ठोस मूल्यों पर काम करने में सक्षम है, जो प्रोग्राम निष्पादन के बारे में सांख्यिकीय जानकारी एकत्र करना और जटिल मात्रात्मक गुणों का आकलन करने के लिए इस जानकारी का उपयोग करना संभव बनाता है। अधिक अभिव्यंजक संपत्ति भाषाएँ जो हमें इस क्षमता का पूर्ण उपयोग करने की अनुमति देंगी, की आवश्यकता है।
+* ''मात्रात्मक गुण-'' अन्य सत्यापन दृष्टिकोणों की तुलना में, रनटाइम सत्यापन प्रणाली स्टेट वेरिएबल्स के ठोस मूल्यों पर कार्य करने में सक्षम है, जो प्रोग्राम निष्पादन के बारे में सांख्यिकीय जानकारी एकत्र करना और जटिल मात्रात्मक गुणों का आकलन करने के लिए इस जानकारी का उपयोग करना संभव बनाता है। इस प्रकार अधिक अभिव्यंजक संपत्ति भाषाएँ जो हमें इस क्षमता का पूर्ण उपयोग करने की अनुमति देंगी, की आवश्यकता है।
-* ''बेहतर इंटरफेस।'' संपत्ति विनिर्देशों को पढ़ना और लिखना गैर-विशेषज्ञों के लिए आसान नहीं है। यहां तक कि विशेषज्ञ अक्सर अपेक्षाकृत छोटे लौकिक तर्क सूत्रों पर मिनटों के लिए घूरते हैं (विशेष रूप से जब वे ऑपरेटरों तक नेस्टेड होते हैं)। एक महत्वपूर्ण अनुसंधान क्षेत्र विभिन्न विशिष्ट औपचारिकताओं के लिए शक्तिशाली उपयोगकर्ता इंटरफेस विकसित करना है जो उपयोगकर्ताओं को अधिक आसानी से समझने, लिखने और यहां तक कि गुणों की कल्पना करने की अनुमति देगा।
+* ''उत्तम इंटरफेस-'' संपत्ति विनिर्देशों को पढ़ना और लिखना गैर-विशेषज्ञों के लिए सरल नहीं है। यहां तक कि विशेषज्ञ अधिकांशतः अपेक्षाकृत छोटे लौकिक तर्क सूत्रों पर मिनटों के लिए घूरते हैं (विशेष रूप से जब वे ऑपरेटरों तक नेस्टेड होते हैं)। महत्वपूर्ण अनुसंधान क्षेत्र विभिन्न विशिष्ट औपचारिकताओं के लिए शक्तिशाली उपयोगकर्ता इंटरफेस विकसित करना है जो उपयोगकर्ताओं को अधिक सरलता से समझने, लिखने और यहां तक कि गुणों की कल्पना करने की अनुमति देगा।
-* ''माइनिंग स्पेसिफिकेशंस।'' यूजर्स को स्पेसिफिकेशंस तैयार करने में मदद करने के लिए चाहे कोई भी टूल सपोर्ट उपलब्ध हो, वे लगभग हमेशा ज्यादा खुश होंगे कि उन्हें कोई स्पेसिफिकेशंस लिखने की जरूरत नहीं है, खासकर तब जब वे तुच्छ हों। सौभाग्य से, वहाँ बहुत सारे कार्यक्रम हैं जो उन कार्यों / घटनाओं का सही उपयोग करते हैं जिनके बारे में कोई गुण रखना चाहता है। यदि ऐसा है, तो यह बोधगम्य है कि कोई उन सही कार्यक्रमों का उपयोग स्वचालित रूप से उनसे वांछित गुण सीखकर करना चाहेगा। यहां तक कि अगर स्वचालित रूप से खनन विनिर्देशों की समग्र गुणवत्ता मैन्युअल रूप से निर्मित विनिर्देशों की तुलना में कम होने की उम्मीद है, तो वे बाद के लिए एक प्रारंभिक बिंदु के रूप में या स्वचालित रनटाइम सत्यापन उपकरण के आधार के रूप में काम कर सकते हैं, विशेष रूप से बग (जहां एक खराब विनिर्देश गलत सकारात्मक या नकारात्मक में बदल जाता है, अक्सर परीक्षण के दौरान स्वीकार्य होता है)।
+* ''माइनिंग स्पेसिफिकेशंस।'' यूजर्स को स्पेसिफिकेशंस तैयार करने में सहायता करने के लिए चाहे कोई भी टूल सपोर्ट उपलब्ध हो, वे लगभग हमेशा ज्यादा खुश होंगे कि उन्हें कोई स्पेसिफिकेशंस लिखने की जरूरत नहीं है, मुख्यकर तब जब वे तुच्छ हों। सौभाग्य से, वहाँ बहुत सारे फंक्शन हैं जो उन कार्यों / घटनाओं का सही उपयोग करते हैं जिनके बारे में कोई गुण रखना चाहता है। यदि ऐसा है, तो यह बोधगम्य है कि कोई उन सही फंक्शनों का उपयोग स्वचालित रूप से उनसे वांछित गुण सीखकर करना चाहेगा। यहां तक कि अगर स्वचालित रूप से खनन विनिर्देशों की समग्र गुणवत्ता मैन्युअल रूप से निर्मित विनिर्देशों की तुलना में कम होने की आशा है, तो वे बाद के लिए प्रारंभिक बिंदु के रूप में या स्वचालित रनटाइम सत्यापन उपकरण के आधार के रूप में कार्य कर सकते हैं, विशेष रूप से बग (जहां खराब विनिर्देश गलत सकारात्मक या नकारात्मक में बदल जाता है, अधिकांशतः परीक्षण के समय स्वीकार्य होता है)।
 === निष्पादन मॉडल और भविष्य कहनेवाला विश्लेषण ===
-त्रुटियों का पता लगाने के लिए रनटाइम सत्यापनकर्ता की क्षमता सख्ती से निष्पादन के निशान का विश्लेषण करने की क्षमता पर निर्भर करती है। जब मॉनिटर सिस्टम के साथ तैनात किए जाते हैं, तो इंस्ट्रूमेंटेशन आमतौर पर न्यूनतम होता है और रनटाइम ओवरहेड को कम रखने के लिए निष्पादन के निशान यथासंभव सरल होते हैं। जब परीक्षण के लिए रनटाइम सत्यापन का उपयोग किया जाता है, तो कोई भी अधिक व्यापक उपकरण वहन कर सकता है जो महत्वपूर्ण सिस्टम जानकारी के साथ घटनाओं को बढ़ाता है जिसका उपयोग मॉनिटर द्वारा निष्पादन प्रणाली के अधिक परिष्कृत मॉडल के निर्माण और विश्लेषण के लिए किया जा सकता है। उदाहरण के लिए, [[वेक्टर घड़ी]] की जानकारी के साथ और डेटा और नियंत्रण प्रवाह की जानकारी के साथ घटनाओं को बढ़ाने से मॉनिटर को चल रहे सिस्टम का एक कारण मॉडल बनाने की अनुमति मिलती है जिसमें देखा गया निष्पादन केवल एक संभावित उदाहरण था। मॉडल के अनुरूप घटनाओं का कोई अन्य क्रमपरिवर्तन सिस्टम का व्यवहार्य निष्पादन है, जो एक अलग थ्रेड इंटरलीविंग के तहत हो सकता है। इस तरह के अनुमानित निष्पादन (उनकी निगरानी करके) में संपत्ति के उल्लंघन का पता लगाने से मॉनिटर उन त्रुटियों की भविष्यवाणी करता है जो देखे गए निष्पादन में नहीं हुई थीं, लेकिन जो उसी प्रणाली के दूसरे निष्पादन में हो सकती हैं। एक महत्वपूर्ण शोध चुनौती उन मॉडलों को निष्पादन निशान से निकालना है जिनमें यथासंभव अन्य निष्पादन निशान शामिल हैं।
+त्रुटियों का पता लगाने के लिए रनटाइम सत्यापनकर्ता की क्षमता सख्ती से निष्पादन के निशान का विश्लेषण करने की क्षमता पर निर्भर करती है। जब मॉनिटर प्रणाली के साथ तैनात किए जाते हैं, तो इंस्ट्रूमेंटेशन सामान्यतः न्यूनतम होता है और रनटाइम ओवरहेड को कम रखने के लिए निष्पादन के निशान यथासंभव सरल होते हैं। इस प्रकार जब परीक्षण के लिए रनटाइम सत्यापन का उपयोग किया जाता है, तो कोई भी अधिक व्यापक उपकरण वहन कर सकता है जो महत्वपूर्ण प्रणाली जानकारी के साथ घटनाओं को बढ़ाता है जिसका उपयोग मॉनिटर द्वारा निष्पादन प्रणाली के अधिक परिष्कृत मॉडल के निर्माण और विश्लेषण के लिए किया जा सकता है। उदाहरण के लिए, [[वेक्टर घड़ी]] की जानकारी के साथ और डेटा और नियंत्रण प्रवाह की जानकारी के साथ घटनाओं को बढ़ाने से मॉनिटर को चल रहे प्रणाली का कारण मॉडल बनाने की अनुमति मिलती है जिसमें देखा गया निष्पादन केवल संभावित उदाहरण था। इस प्रकार इस मॉडल के अनुरूप घटनाओं का कोई अन्य क्रमपरिवर्तन प्रणाली का व्यवहार्य निष्पादन है, जो अलग थ्रेड इंटरलीविंग के अनुसार हो सकता है। इस तरह के अनुमानित निष्पादन (उनकी जाँच करके) में संपत्ति के उल्लंघन का पता लगाने से मॉनिटर उन त्रुटियों की भविष्यवाणी करता है जो देखे गए निष्पादन में नहीं हुई थीं, किन्तु जो उसी प्रणाली के दूसरे निष्पादन में हो सकती हैं। महत्वपूर्ण शोध चुनौती उन मॉडलों को निष्पादन निशान से निकालना है जिनमें यथासंभव अन्य निष्पादन निशान सम्मिलित हैं।
 === व्यवहार संशोधन ===
-परीक्षण या संपूर्ण सत्यापन के विपरीत, रनटाइम सत्यापन में सिस्टम को पुन: कॉन्फ़िगरेशन, माइक्रो-रीसेट, या कभी-कभी ट्यूनिंग या स्टीयरिंग के रूप में संदर्भित महीन हस्तक्षेप तंत्र के माध्यम से पहचाने गए उल्लंघनों से उबरने की अनुमति देने का वादा होता है। रनटाइम सत्यापन के कठोर ढांचे के भीतर इन तकनीकों का कार्यान्वयन अतिरिक्त चुनौतियों को जन्म देता है।
+परीक्षण या संपूर्ण सत्यापन के विपरीत, '''रनटाइम सत्यापन''' में प्रणाली की पुन: कॉन्फ़िगरेशन, माइक्रो-रीसेट, या कभी-कभी ट्यूनिंग या स्टीयरिंग के रूप में संदर्भित महीन हस्तक्षेप प्रणाली के माध्यम से पहचाने गए उल्लंघनों से उबरने की अनुमति देने का वादा होता है। रनटाइम सत्यापन के कठोर ढांचे के भीतर इन तकनीकों का कार्यान्वयन अतिरिक्त चुनौतियों को जन्म देता है।
-* ''कार्रवाइयों की विशिष्टता।'' किसी को एक सार रूप में किए जाने वाले संशोधन को निर्दिष्ट करने की आवश्यकता होती है, जिसके लिए उपयोगकर्ता को अप्रासंगिक कार्यान्वयन विवरण जानने की आवश्यकता नहीं होती है। इसके अलावा, सिस्टम की अखंडता को बनाए रखने के लिए इस तरह का संशोधन कब हो सकता है, इसे निर्दिष्ट करने की आवश्यकता है।
+* ''कार्रवाइयों की विशिष्टता-'' किसी को सार रूप में किए जाने वाले संशोधन को निर्दिष्ट करने की आवश्यकता होती है, जिसके लिए उपयोगकर्ता को अप्रासंगिक कार्यान्वयन विवरण जानने की आवश्यकता नहीं होती है। इसके अतिरिक्त, प्रणाली की अखंडता को बनाए रखने के लिए इस तरह का संशोधन कब हो सकता है, इसे निर्दिष्ट करने की आवश्यकता है।
-* ''हस्तक्षेप प्रभावों के बारे में तर्क।'' यह जानना महत्वपूर्ण है कि एक हस्तक्षेप से स्थिति में सुधार होता है, या कम से कम स्थिति को बदतर नहीं बनाता है।
+* ''हस्तक्षेप प्रभावों के बारे में तर्क।'' यह जानना महत्वपूर्ण है कि हस्तक्षेप से स्थिति में सुधार होता है, या कम से कम स्थिति को कठोर नहीं बनने देता हैं।
-* ''एक्शन इंटरफेस।'' मॉनिटरिंग के लिए इंस्ट्रूमेंटेशन के समान, हमें सिस्टम को एक्शन इनवोकेशन प्राप्त करने के लिए सक्षम करने की आवश्यकता है। आमंत्रण तंत्र अनिवार्य रूप से सिस्टम के कार्यान्वयन विवरण पर निर्भर होने जा रहे हैं। हालाँकि, विनिर्देश स्तर पर, हमें उपयोगकर्ता को सिस्टम को प्रतिक्रिया प्रदान करने का एक घोषणात्मक तरीका प्रदान करने की आवश्यकता होती है, यह निर्दिष्ट करके कि किन परिस्थितियों में कब कार्रवाई की जानी चाहिए।
+* ''एक्शन इंटरफेस-'' मॉनिटरिंग के लिए इंस्ट्रूमेंटेशन के समान, हमें इस प्रकार इस प्रणाली की एक्शन इनवोकेशन प्राप्त करने के लिए सक्षम करने की आवश्यकता है। आमंत्रण प्रणाली अनिवार्य रूप से प्रणाली के कार्यान्वयन विवरण पर निर्भर होने जा रहे हैं। चूंकि, विनिर्देश स्तर पर, हमें उपयोगकर्ता को प्रणाली की प्रतिक्रिया प्रदान करने का घोषणात्मक विधि प्रदान करने की आवश्यकता होती है, यह निर्दिष्ट करके कि किन परिस्थितियों में कब कार्रवाई की जानी चाहिए।
 == संबंधित कार्य ==
 === पहलू-उन्मुख प्रोग्रामिंग ===
-रनटाइम सत्यापन में शोधकर्ताओं ने मॉड्यूलर तरीके से प्रोग्राम इंस्ट्रूमेंटेशन को परिभाषित करने के लिए एक तकनीक के रूप में पहलू-उन्मुख प्रोग्रामिंग का उपयोग करने की क्षमता को पहचाना। पहलू-उन्मुख प्रोग्रामिंग (एओपी) आम तौर पर क्रॉसकटिंग चिंताओं के मॉड्यूलरलाइजेशन को बढ़ावा देती है। रनटाइम सत्यापन स्वाभाविक रूप से ऐसी ही एक चिंता है और इसलिए एओपी के कुछ गुणों से लाभान्वित हो सकता है। पहलू-उन्मुख मॉनिटर परिभाषाएँ काफी हद तक घोषणात्मक हैं, और इसलिए एक अनिवार्य प्रोग्रामिंग भाषा में लिखे गए [[कार्यक्रम परिवर्तन]] के माध्यम से व्यक्त किए गए इंस्ट्रूमेंटेशन की तुलना में तर्क करना आसान होता है। इसके अलावा, स्थिर विश्लेषण, प्रोग्राम इंस्ट्रूमेंटेशन के अन्य रूपों की तुलना में मॉनिटरिंग पहलुओं के बारे में अधिक आसानी से तर्क कर सकते हैं, क्योंकि सभी इंस्ट्रूमेंटेशन एक ही पहलू के भीतर समाहित हैं। कई वर्तमान रनटाइम सत्यापन उपकरण इसलिए विनिर्देशन संकलक के रूप में बनाए गए हैं, जो इनपुट के रूप में अभिव्यंजक उच्च-स्तरीय विनिर्देश लेते हैं और कुछ पहलू-उन्मुख प्रोग्रामिंग भाषा (जैसे [[AspectJ]]) में लिखे आउटपुट कोड के रूप में उत्पन्न होते हैं।
+'''रनटाइम सत्यापन''' में शोधकर्ताओं ने मॉड्यूलर विधि से प्रोग्राम इंस्ट्रूमेंटेशन को परिभाषित करने के लिए तकनीक के रूप में पहलू-उन्मुख प्रोग्रामिंग का उपयोग करने की क्षमता को पहचाना। पहलू-उन्मुख प्रोग्रामिंग (एओपी) सामान्यतः क्रॉसकटिंग चिंताओं के मॉड्यूलरलाइजेशन को बढ़ावा देती है। रनटाइम सत्यापन स्वाभाविक रूप से ऐसी ही चिंता है और इसलिए एओपी के कुछ गुणों से लाभान्वित हो सकता है। इस प्रकार पहलू-उन्मुख मॉनिटर परिभाषाएँ काफी हद तक घोषणात्मक हैं, और इसलिए अनिवार्य प्रोग्रामिंग भाषा में लिखे गए [[कार्यक्रम परिवर्तन|फंक्शन परिवर्तन]] के माध्यम से व्यक्त किए गए इंस्ट्रूमेंटेशन की तुलना में तर्क करना सरल होता है। इसके अतिरिक्त, स्थिर विश्लेषण, प्रोग्राम इंस्ट्रूमेंटेशन के अन्य रूपों की तुलना में मॉनिटरिंग पहलुओं के बारे में अधिक सरलता से तर्क कर सकते हैं, क्योंकि सभी इंस्ट्रूमेंटेशन ही पहलू के भीतर समाहित हैं। कई वर्तमान रनटाइम सत्यापन उपकरण इसलिए विनिर्देशन संकलक के रूप में बनाए गए हैं, जो इनपुट के रूप में अभिव्यंजक उच्च-स्तरीय विनिर्देश लेते हैं और कुछ पहलू-उन्मुख प्रोग्रामिंग भाषा (जैसे [[AspectJ|एस्पैक्ट जे]]) में लिखे आउटपुट कोड के रूप में उत्पन्न होते हैं।
 === औपचारिक सत्यापन के साथ संयोजन ===
-रनटाइम सत्यापन, यदि उचित रूप से सही पुनर्प्राप्ति कोड के संयोजन में उपयोग किया जाता है, तो प्रोग्राम सत्यापन के लिए एक अमूल्य अवसंरचना प्रदान कर सकता है, जो बाद की जटिलता को काफी कम कर सकता है। उदाहरण के लिए, हीप-सॉर्ट एल्गोरिथम को औपचारिक रूप से सत्यापित करना बहुत चुनौतीपूर्ण है। इसे सत्यापित करने के लिए एक कम चुनौतीपूर्ण तकनीक इसके आउटपुट को सॉर्ट करने के लिए मॉनिटर करना है (एक रैखिक जटिलता मॉनिटर) और, यदि सॉर्ट नहीं किया गया है, तो इसे कुछ आसानी से सत्यापन योग्य प्रक्रिया का उपयोग करके सॉर्ट करें, इंसर्शन सॉर्ट कहें। परिणामी छँटाई कार्यक्रम अब अधिक आसानी से सत्यापित किया जा सकता है, हीप-सॉर्ट से केवल एक चीज की आवश्यकता होती है कि यह मल्टीसेट के रूप में माने जाने वाले मूल तत्वों को नष्ट नहीं करता है, जिसे साबित करना बहुत आसान है। दूसरी दिशा से देखने पर, रनटाइम सत्यापन के ओवरहेड को कम करने के लिए औपचारिक सत्यापन का उपयोग किया जा सकता है, जैसा कि पहले ही औपचारिक सत्यापन के बजाय स्थिर विश्लेषण के लिए ऊपर उल्लेख किया गया है। दरअसल, कोई पूरी तरह से सत्यापित रनटाइम के साथ शुरू कर सकता है, लेकिन शायद धीमा कार्यक्रम। फिर कोई मॉनिटर को डिस्चार्ज करने के लिए औपचारिक सत्यापन (या स्थिर विश्लेषण) का उपयोग कर सकता है, उसी तरह एक कंपाइलर स्टैटिक एनालिसिस का उपयोग टाइप शुद्धता या मेमोरी सुरक्षा के रनटाइम चेक को डिस्चार्ज करने के लिए करता है।
+'''रनटाइम सत्यापन''', यदि उचित रूप से सही पुनर्प्राप्ति कोड के संयोजन में उपयोग किया जाता है, तो प्रोग्राम सत्यापन के लिए अमूल्य अवसंरचना प्रदान कर सकता है, जो बाद की जटिलता को काफी कम कर सकता है। उदाहरण के लिए, हीप-सॉर्ट एल्गोरिथम को औपचारिक रूप से सत्यापित करना बहुत चुनौतीपूर्ण है। इसे सत्यापित करने के लिए कम चुनौतीपूर्ण तकनीक इसके आउटपुट को सॉर्ट करने के लिए मॉनिटर करना है (एक रैखिक जटिलता मॉनिटर) और, यदि सॉर्ट नहीं किया गया है, तो इसे कुछ सरलता से सत्यापन योग्य प्रक्रिया का उपयोग करके सॉर्ट करें, इंसर्शन सॉर्ट कहें जाता हैं। इस प्रकार परिणामी छँटाई फंक्शन अब अधिक सरलता से सत्यापित किया जा सकता है, हीप-सॉर्ट से केवल चीज की आवश्यकता होती है कि यह मल्टीसेट के रूप में माने जाने वाले मूल तत्वों को नष्ट नहीं करता है, जिसे प्रमाणित करना बहुत सरल है। दूसरी दिशा से देखने पर, रनटाइम सत्यापन के ओवरहेड को कम करने के लिए औपचारिक सत्यापन का उपयोग किया जा सकता है, जैसा कि पहले ही औपचारिक सत्यापन के अतिरिक्त स्थिर विश्लेषण के लिए ऊपर उल्लेख किया गया है। दरअसल, कोई पूरी तरह से सत्यापित रनटाइम के साथ प्रारंभ कर सकता है, किन्तु यह लो स्पीड फंक्शन के रूप में कार्य करता हैं। इस प्रकार फिर से किसी मॉनिटर को डिस्चार्ज करने के लिए औपचारिक सत्यापन (या स्थिर विश्लेषण) का उपयोग कर सकता है, उसी तरह कंपाइलर स्टैटिक एनालिसिस का उपयोग टाइप शुद्धता या मेमोरी सुरक्षा के रनटाइम चेक को डिस्चार्ज करने के लिए करता है।
 === बढ़ता कवरेज ===
-अधिक पारंपरिक सत्यापन दृष्टिकोणों की तुलना में, रनटाइम सत्यापन का एक तत्काल नुकसान इसकी कम कवरेज है। यह समस्याग्रस्त नहीं है जब रनटाइम मॉनिटर सिस्टम के साथ तैनात किए जाते हैं (संपत्ति का उल्लंघन होने पर निष्पादित किए जाने वाले उपयुक्त पुनर्प्राप्ति कोड के साथ), लेकिन यह सिस्टम में त्रुटियों को खोजने के लिए उपयोग किए जाने पर रनटाइम सत्यापन की प्रभावशीलता को सीमित कर सकता है। त्रुटि का पता लगाने के उद्देश्यों के लिए रनटाइम सत्यापन के कवरेज को बढ़ाने की तकनीकों में शामिल हैं:
+अधिक पारंपरिक सत्यापन दृष्टिकोणों की तुलना में, रनटाइम सत्यापन का तत्काल हानि इसकी कम कवरेज है। यह समस्याग्रस्त नहीं है जब रनटाइम मॉनिटर प्रणाली के साथ तैनात किए जाते हैं (संपत्ति का उल्लंघन होने पर निष्पादित किए जाने वाले उपयुक्त पुनर्प्राप्ति कोड के साथ), किन्तु यह प्रणाली में त्रुटियों को जाँचने के लिए उपयोग किए जाने पर रनटाइम सत्यापन की प्रभावशीलता को सीमित कर सकता है। त्रुटि का पता लगाने के उद्देश्यों के लिए रनटाइम सत्यापन के कवरेज को बढ़ाने की तकनीकों में सम्मिलित हैं:
-* ''इनपुट जनरेशन।'' यह सर्वविदित है कि इनपुट्स का एक अच्छा सेट (प्रोग्राम इनपुट वेरिएबल वैल्यू, सिस्टम कॉल वैल्यू, थ्रेड शेड्यूल आदि) उत्पन्न करने से परीक्षण की प्रभावशीलता में काफी वृद्धि हो सकती है। यह त्रुटि का पता लगाने के लिए उपयोग किए जाने वाले रनटाइम सत्यापन के लिए भी सही है, लेकिन इनपुट जनरेशन प्रक्रिया को चलाने के लिए प्रोग्राम कोड का उपयोग करने के अलावा, रनटाइम सत्यापन में संपत्ति विनिर्देशों का उपयोग भी किया जा सकता है, जब उपलब्ध हो, और प्रेरित करने के लिए निगरानी तकनीकों का भी उपयोग कर सकता है। वांछित व्यवहार। रनटाइम सत्यापन का यह उपयोग इसे मॉडल-आधारित परीक्षण से निकटता से संबंधित बनाता है, हालांकि रनटाइम सत्यापन विनिर्देश आमतौर पर सामान्य उद्देश्य होते हैं, जरूरी नहीं कि परीक्षण कारणों से तैयार किए गए हों। उदाहरण के लिए, विचार करें कि कोई उपरोक्त सामान्य-उद्देश्य ''UnsafeEnum'' गुण का परीक्षण करना चाहता है। सिस्टम निष्पादन को निष्क्रिय रूप से देखने के लिए उपर्युक्त मॉनिटर को उत्पन्न करने के बजाय, कोई भी एक स्मार्ट मॉनिटर उत्पन्न कर सकता है जो थ्रेड को दूसरे ''e.nextElement()'' ईवेंट (इसे उत्पन्न करने से ठीक पहले) उत्पन्न करने का प्रयास करता है। अन्य धागे इस उम्मीद में निष्पादित होते हैं कि उनमें से एक ''v.update()'' घटना उत्पन्न कर सकता है, जिस स्थिति में एक त्रुटि पाई गई है।
+* ''इनपुट जनरेशन-'' यह सर्वविदित है कि इनपुट्स का अच्छा सेट (प्रोग्राम इनपुट वेरिएबल वैल्यू, प्रणाली कॉल वैल्यू, थ्रेड शेड्यूल आदि) उत्पन्न करने से परीक्षण की प्रभावशीलता में काफी वृद्धि हो सकती है। यह त्रुटि का पता लगाने के लिए उपयोग किए जाने वाले रनटाइम सत्यापन के लिए भी सही है, किन्तु इनपुट जनरेशन प्रक्रिया को चलाने के लिए प्रोग्राम कोड का उपयोग करने के अतिरिक्त, रनटाइम सत्यापन में संपत्ति विनिर्देशों का उपयोग भी किया जा सकता है, जब यह उपलब्ध होता हैं और प्रेरित करने के लिए जाँच तकनीकों का भी उपयोग कर सकता है।
-* ''गतिशील प्रतीकात्मक निष्पादन।'' प्रतीकात्मक निष्पादन में कार्यक्रमों को प्रतीकात्मक रूप से क्रियान्वित और मॉनिटर किया जाता है, अर्थात, बिना ठोस इनपुट के। सिस्टम के एक प्रतीकात्मक निष्पादन में ठोस इनपुट का एक बड़ा सेट शामिल हो सकता है। ऑफ-द-शेल्फ बाधा समाधान या संतुष्टि जांच तकनीकों का उपयोग अक्सर प्रतीकात्मक निष्पादन चलाने या उनके स्थान को व्यवस्थित रूप से एक्सप्लोर करने के लिए किया जाता है। जब अंतर्निहित संतुष्टि जांचकर्ता एक विकल्प बिंदु को संभाल नहीं सकते हैं, तो उस बिंदु को पास करने के लिए एक ठोस इनपुट उत्पन्न किया जा सकता है; 'कॉन्स' रीटे और सिम्ब'ऑलिक निष्पादन के इस संयोजन को कॉनकोलिक निष्पादन भी कहा जाता है।
+*वांछित व्यवहार के कारण रनटाइम सत्यापन का यह उपयोग इसे मॉडल-आधारित परीक्षण से निकटता से संबंधित बनाता है, चूंकि रनटाइम सत्यापन विनिर्देश सामान्यतः सामान्य उद्देश्य होते हैं, इस प्रकार आवश्यक नहीं हैं कि परीक्षण कारणों से तैयार किए गए हों। उदाहरण के लिए, विचार करें कि कोई उपरोक्त सामान्य-उद्देश्य ''UnsafeEnum()'' गुण का परीक्षण करना चाहता है। प्रणाली निष्पादन को निष्क्रिय रूप से देखने के लिए उपर्युक्त मॉनिटर को उत्पन्न करने के अतिरिक्त, कोई भी स्मार्ट मॉनिटर उत्पन्न कर सकता है जो थ्रेड को दूसरे ''e.nextElement()'' ईवेंट (इसे उत्पन्न करने से ठीक पहले) उत्पन्न करने का प्रयास करता है। अन्य धागे इस आशा में निष्पादित होते हैं कि उनमें से ''v.update()'' घटना उत्पन्न कर सकता है, जिस स्थिति में त्रुटि पाई गई है।
+* ''गतिशील प्रतीकात्मक निष्पादन-'' प्रतीकात्मक निष्पादन में फंक्शनों को प्रतीकात्मक रूप से क्रियान्वित और मॉनिटर किया जाता है, अर्थात बिना ठोस इनपुट के इस प्रणाली के प्रतीकात्मक निष्पादन में ठोस इनपुट का बड़ा सेट सम्मिलित हो सकता है। इस प्रकार ऑफ-द-शेल्फ बाधा समाधान या संतुष्टि जांच तकनीकों का उपयोग अधिकांशतः प्रतीकात्मक निष्पादन चलाने या उनके स्थान को व्यवस्थित रूप से एक्सप्लोर करने के लिए किया जाता है। जब अंतर्निहित संतुष्टि जांचकर्ता विकल्प बिंदु को संभाल नहीं सकते हैं, तो उस बिंदु को पास करने के लिए ठोस इनपुट उत्पन्न किया जा सकता है; 'कॉन्स' रीटे और सिम्ब'ऑलिक निष्पादन के इस संयोजन को कॉनकोलिक निष्पादन भी कहा जाता है।
 == यह भी देखें ==
-* गतिशील कार्यक्रम विश्लेषण
+* गतिशील फंक्शन विश्लेषण
 * प्रोफाइलिंग (कंप्यूटर प्रोग्रामिंग)
 * [[रनटाइम त्रुटि का पता लगाना]]
@@ Line 113: / Line 96: @@
 {{Reflist}}
-[[Category: औपचारिक तरीके]] [[Category: कंप्यूटर विज्ञान में तर्क]]
-[[Category: Machine Translated Page]]
 [[Category:Created On 02/03/2023]]
+[[Category:Machine Translated Page]]
+[[Category:Pages with script errors]]
+[[Category:Templates Vigyan Ready]]
+[[Category:औपचारिक तरीके]]
+[[Category:कंप्यूटर विज्ञान में तर्क]]

Anonymous

Search

रनटाइम सत्यापन: Difference between revisions

Namespaces

More

Page actions

Latest revision as of 10:16, 15 March 2023

Contents

इतिहास और संदर्भ

मूल दृष्टिकोण

उदाहरण