कंप्यूटर वैज्ञानिक यह साबित कर सकते हैं कि कार्यक्रम में कोई निश्चितता नहीं है क्योंकि गणितज्ञ प्रमेय साबित कर सकते हैं। इन अग्रिमों का उपयोग ड्रोन से लेकर इंटरनेट तक कई क्षेत्रों में सुरक्षा बढ़ाने के लिए किया जाता है।

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

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

कहती हैं, "वे ऑपरेशन को क्रैक या बाधित नहीं कर सकते थे।"टफ्ट्स यूनिवर्सिटी में कंप्यूटर साइंस के प्रोफेसर और हाई-एश्योरेंस साइबर मिलिट्री सिस्टम (HACMS) के प्रोजेक्ट मैनेजर हैं। "परिणामस्वरूप, DARPA के प्रतिनिधियों ने उठकर कहा, हे भगवान, आप वास्तव में महत्वपूर्ण प्रणालियों में इस तकनीक का उपयोग कर सकते हैं।"

हैकर्स का विरोध करने वाली प्रौद्योगिकी एक प्रोग्रामिंग शैली है जिसे औपचारिक पुष्टि कहा जाता है । अनौपचारिक रूप से लिखे गए साधारण कोड के विपरीत और आमतौर पर केवल उसके प्रदर्शन से मूल्यांकन किया जाता है, औपचारिक रूप से सत्यापित सॉफ़्टवेयर गणितीय प्रमाण की तरह दिखता है: प्रत्येक कथन पिछले एक से तार्किक रूप से अनुसरण करता है। पूरे कार्यक्रम को गणितीय प्रमेय के रूप में एक ही निश्चितता के साथ सत्यापित किया जा सकता है।

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

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

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

"20 वीं शताब्दी में, जब एक कार्यक्रम में एक गलती थी, तो यह खराब था, यह गिर सकता है, ठीक है, भगवान उसे आशीर्वाद दें," प्रिंसटन विश्वविद्यालय में कंप्यूटर विज्ञान के प्रोफेसर और कार्यक्रम सत्यापन में एक नेता एंड्रयू एपेल ने कहा । लेकिन 21 वीं सदी में, एक गलती हैकर्स के लिए कार्यक्रम का नियंत्रण हासिल करने और आपका डेटा चोरी करने का रास्ता खोल सकती है। एक सहनीय गलती से, यह एक भेद्यता बन गई है, जो बहुत बुरा है, ”वह कहते हैं।

कैथलीन फिशर

संपूर्ण कार्यक्रमों के सपने

अक्टूबर 1973 में, Edsger Dijkstra बिना त्रुटियों के कोड बनाने के विचार के साथ आया। रात में, एक सम्मेलन में एक होटल में रहते हुए, उन्होंने अचानक सोचा कि प्रोग्रामिंग को और अधिक गणितीय कैसे बनाया जाए। बाद में विचार के बारे में बताते हुए उन्होंने कहा, "उत्साहित दिमाग के साथ, मैं सुबह 2:30 बजे बिस्तर से बाहर निकला, और एक घंटे से अधिक समय तक लिखा।" यह सामग्री उनकी फलदायी 1976 की पुस्तक, द डिसिप्लिन ऑफ़ प्रोग्रामिंग की शुरुआत थी, जिसमें चार्ल्स होरे (जैसे डेज्स्ट्रा, जिन्होंने ट्यूरिंग पुरस्कार प्राप्त किया था ) के काम के साथ, लेखन कार्यक्रमों में शुद्धता के प्रमाण के उपयोग पर विचारों को परिभाषित किया।

लेकिन कंप्यूटर विज्ञान ने इस विचार का पालन नहीं किया, मुख्यतः क्योंकि कई सालों तक यह औपचारिक तर्क के नियमों का उपयोग करके कार्यक्रम के कार्य को निर्धारित करने के लिए अव्यवहारिक, या असंभव भी लग रहा था।

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

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

“एक छेद सॉफ्टवेयर में कहीं है, और यह एक भेद्यता है। परनो कहते हैं, '' हर संभव इनपुट के लिए सभी रास्तों की जाँच करना बहुत मुश्किल है।

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

मानव भाषा में, यह वर्णन करना आसान है। एक विनिर्देश को औपचारिक भाषा में बदलना जो एक कंप्यूटर समझता है वह बहुत कठिन है - जो प्रोग्राम लिखने की मुख्य समस्या को बताता है।

"एक औपचारिक विनिर्देश का निर्माण जो कंप्यूटर के लिए समझ में आता है, सार में मुश्किल है," पारनो कहते हैं। "यह कहना" पासवर्ड लीक न होने देना "शीर्ष स्तर पर आसान है, लेकिन आपको यह सोचने की ज़रूरत है कि इसे गणितीय परिभाषा में कैसे बदलना है।"

एक अन्य उदाहरण एक प्रोग्राम है जो संख्याओं की सूची को सॉर्ट करता है। उसके लिए एक विनिर्देशन को औपचारिक बनाने की कोशिश में एक प्रोग्रामर इसके साथ आ सकता है:

सूची में प्रत्येक आइटम j के लिए, सुनिश्चित करें कि j 1 j + 1

लेकिन इस औपचारिक विनिर्देश में भी - यह सुनिश्चित करने के लिए कि सूची में प्रत्येक तत्व अगले से कम या बराबर है - कोई त्रुटि है। प्रोग्रामर मानता है कि आउटपुट में संशोधित इनपुट होगा। यदि सूची [7, 3, 5] है, तो वह उम्मीद करता है कि कार्यक्रम [3, 5, 7] वापस आ जाएगा। परनो का कहना है कि कार्यक्रम [1, 2] का आउटपुट विनिर्देशों को संतुष्ट करेगा - क्योंकि "यह एक छांटी हुई सूची भी है, लेकिन उस सूची में नहीं, जिसकी आपको उम्मीद थी।"

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

ब्लॉक सुरक्षा

वास्तव में, कोड के बारे में निष्कर्ष निकालने के लिए सॉफ्टवेयर के लिए आवश्यक विनिर्देशों और अतिरिक्त टिप्पणियों दोनों को लिखना आवश्यक है। एक कार्यक्रम, इसकी औपचारिक पुष्टि सहित, एक ही उद्देश्य के लिए लिखे गए एक नियमित कार्यक्रम के आकार का पांच गुना हो सकता है।

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

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

( ) , … , , .

फिर इंटरनेट आया, जिसने कोड में त्रुटियों के लिए वही किया जो हवाई यात्रा ने संक्रमण के लिए किया था: जब सभी कंप्यूटर एक-दूसरे से जुड़े होते हैं, तो असहज लेकिन सहनशील त्रुटियां बढ़ती सुरक्षा समस्याओं को जन्म दे सकती हैं।

"हम पूरी तरह से समझ नहीं पाए," एपल कहते हैं। "सभी इंटरनेट हैकर्स के लिए प्रोग्राम खुले हैं, और अगर इस तरह के प्रोग्राम में कोई गलती है, तो यह एक भेद्यता बन सकती है।"

जब तक शोधकर्ताओं ने इंटरनेट द्वारा उत्पन्न सुरक्षा खतरों की गंभीरता को समझना शुरू किया, तब तक कार्यक्रम की पुष्टि लौटने वाली थी। शुरुआत करने के लिए, शोधकर्ताओं ने औपचारिक तरीकों के बुनियादी हिस्सों में प्रगति की है। यह Coq और Isabelle जैसे सहायक कार्यक्रमों में सुधार है; तार्किक प्रणालियों का विकास ( आश्रित प्रकारों का सिद्धांत)) एक विकास मंच प्रदान करना जो कंप्यूटर को कोड का मूल्यांकन करने में मदद करता है; "ऑपरेशनल शब्दार्थ" एक ऐसी भाषा है जिसमें कार्यक्रम के लिए आवश्यक शब्दों को व्यक्त करने के लिए सही शब्द हैं।

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

माइक्रोसॉफ्ट रिसर्च के जेनेट विंग

इसके अलावा, औपचारिक विधि शोधकर्ताओं ने अपने लक्ष्यों को फिर से परिभाषित किया है। 1970 और 1980 के दशक में, वे इलेक्ट्रॉनिक सर्किट से कार्यक्रमों तक पूरी तरह से परीक्षण किए गए कंप्यूटर सिस्टम बनाना चाहते थे। आज, अधिकांश शोधकर्ता सिस्टम के छोटे, लेकिन सबसे महत्वपूर्ण या कमजोर भागों पर काम करते हैं - उदाहरण के लिए, ऑपरेटिंग सिस्टम या क्रिप्टोग्राफ़िक प्रोटोकॉल।

"हम यह नहीं कह रहे हैं कि हम साबित करेंगे कि पूरा सिस्टम 100% सही है, इलेक्ट्रॉनिक सर्किट के ठीक नीचे है," विंग कहते हैं। - इस तरह के बयान हास्यास्पद हैं। हम वह कर सकते हैं जो हम कर सकते हैं या नहीं कर सकते हैं। "

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

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

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

लेखापरीक्षा के बाद के वर्ष में, DARPA ने सैन्य प्रौद्योगिकी के अन्य क्षेत्रों के लिए परियोजना के उपकरण और तकनीकें लागू कीं, उदाहरण के लिए, उपग्रह और स्वचालित ट्रक। नई पहल पिछले दस वर्षों में औपचारिक पुष्टि कैसे हुई है, इसके साथ मेल खाता है: प्रत्येक सफल परियोजना अगले को प्रोत्साहित करती है। "इस सिद्धांत की जटिलता के बारे में बहाने अब काम नहीं करते हैं," फिशर कहते हैं।

इंटरनेट की जाँच करें

सुरक्षा और विश्वसनीयता दो मुख्य लक्ष्य हैं जो औपचारिक तरीकों को प्रेरित करते हैं। हर दिन, सुधार की आवश्यकता अधिक स्पष्ट होती जा रही है। 2014 में, एक छोटी सी सॉफ़्टवेयर त्रुटि, जो एक औपचारिक विवरण पकड़ लेती है, ने हार्टब्लड त्रुटि के लिए रास्ता खोल दिया जिसने इंटरनेट को तोड़ने की धमकी दी। एक साल बाद, "कानूनी" हैकर्स के एक जोड़े ने जीप चेरोकी पर रिमोट कंट्रोल हासिल करने, इंटरनेट से जुड़ी कारों के बारे में सबसे खराब आशंकाओं की पुष्टि की ।

उच्च दर के साथ, औपचारिक विधि शोधकर्ताओं ने तेजी से महत्वाकांक्षी लक्ष्य निर्धारित किए। अप्पेल (HACMS पर भी काम कर रही) के नेतृत्व में दीपस्पीक टीम, वेब सर्वर के रूप में इस तरह के एक जटिल, पूरी तरह से परीक्षण प्रणाली का निर्माण करने की कोशिश कर रही है। सफल होने पर, राज्य विज्ञान फाउंडेशन से $ 10 मिलियन का अनुदान प्राप्त करने वाली परियोजना, पिछले दशक की कई छोटी सफल परियोजनाओं को एक साथ लाएगी। शोधकर्ताओं ने ऑपरेटिंग सिस्टम के कर्नेल जैसे कई सिद्ध सुरक्षित घटक बनाए हैं। "अब तक जो नहीं किया गया है वह इन घटकों के विनिर्देशन-विशिष्ट इंटरफेस में एकीकरण है," एपल कहते हैं।

Microsoft अनुसंधान में, प्रोग्रामरों की दो महत्वाकांक्षी परियोजनाएं हैं। पहला, एवरेस्ट का उद्देश्य एचटीटीपीएस का एक मान्य संस्करण बनाना है, जो वेब ब्राउज़र को सुरक्षित करने के लिए एक प्रोटोकॉल है जिसे विंग "इंटरनेट की एच्लीस हील" कहते हैं।

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

अखंड कोड मौजूद है

संपूर्ण कार्यक्रमों के सपने

ब्लॉक सुरक्षा

इंटरनेट की जाँच करें

More articles: