रनटाइम सत्यापन

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

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

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

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

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

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

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

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

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

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

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

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

उदाहरण

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

has Next ()

File:Hasnext.jpg

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 लौटाता हैं।

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

Error creating thumbnail:

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

जावा में वेक्टर वर्ग के अपने तत्वों पर पुनरावृति के लिए दो साधन हैं। कोई भी इटरेटर इंटरफ़ेस का उपयोग कर सकता है, जैसा कि पिछले उदाहरण में देखा गया है, या कोई इनुम्रेशन इंटरफ़ेस का उपयोग कर सकता है। इटरेटर इंटरफ़ेस के लिए निकालने की विधि को जोड़ने के अतिरिक्त, मुख्य अंतर यह है कि इटरेटर तेजी से विफल होता है जबकि इनुमरेशन नहीं है। इसका अर्थ यह है कि यदि कोई वेक्टर को संशोधित करता है (इटरेटर हटाने की विधि का उपयोग करने के अतिरिक्त) इस प्रकार जब कोई इटरेटर का उपयोग करके वेक्टर पर पुनरावृति करता है, तो /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)

File:Safelocktrace.jpg

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

पैटर्न प्रत्येक थ्रेड और लॉक के लिए नेस्टेड प्रारंभ/समाप्ति और अधिग्रहण/रिलीज जोड़े के संतुलित अनुक्रम निर्दिष्ट ($\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 मान लौटाता है, यह मुख्य रूप से नियंत्रण-प्रवाह ग्राफ़ पर दिखाई देता है।
• कुशल मॉनिटर निर्माण और प्रबंधन के लिए उपयोग किया जाता हैं, इस प्रकार उपरोक्त उदाहरणों में पैरामीट्रिक गुणों की जाँच करते समय, जाँच प्रणाली की प्रत्येक पैरामीटर उदाहरण के संबंध में जाँच की गई संपत्ति की स्थिति का ट्रैक रखने की आवश्यकता होती है। ऐसे उदाहरणों की संख्या सैद्धांतिक रूप से अबाध है और इस प्रकार व्यवहार में बहुत अधिक हो जाती है। इसकी महत्वपूर्ण शोध चुनौती यह है कि कैसे देखी गई घटनाओं को कुशलतापूर्वक उन घटनाओं को ठीक से प्रेषित किया जाए जिनकी उन्हें आवश्यकता है। इस प्रकार संबंधित चुनौती यह है कि ऐसे उदाहरणों की संख्या को कैसे कम रखा जाए (जिससे कि प्रेषण तेजी से हो), या दूसरे शब्दों में, यथासंभव लंबे समय तक अनावश्यक उदाहरण बनाने से कैसे बचा जाए और साथ ही, पहले से बनाए गए उदाहरणों को जल्द से जल्द कैसे हटाया जाए वे अनावश्यक हो जाते हैं। अंत में, पैरामीट्रिक मॉनिटरिंग एल्गोरिदम सामान्यतः गैर-पैरामीट्रिक मॉनिटर बनाने के लिए समान एल्गोरिदम का सामान्यीकरण करते हैं। इस प्रकार, उत्पन्न गैर-पैरामीट्रिक मॉनिटर की गुणवत्ता परिणामी पैरामीट्रिक मॉनिटर की गुणवत्ता तय करती है। चूंकि, अन्य सत्यापन विधियों (जैसे, मॉडल जाँच) के विपरीत, रनटाइम सत्यापन में स्थिति की संख्या या उत्पन्न मॉनिटर का आकार कम महत्वपूर्ण है; वास्तव में, कुछ मॉनिटरों में अधिकता से कई अवस्थाएँ हो सकती हैं, जैसे कि उपरोक्त सेफ लाॅक संपत्ति के लिए, चूंकि किसी भी समय केवल स्थिति की सीमित संख्या हो सकती है। महत्वपूर्ण यह है कि निष्पादन प्रणाली से घटना प्राप्त होने पर मॉनिटर स्थिति से अपने अगले स्थिति में कितनी कुशलता से स्थानांतरित होता है।

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

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

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