कार्यक्रम सत्यापन के औपचारिक तरीकों के उद्योग में एक जगह है?

Question

मैंने कॉलेज में Hoare Logic पर एक झलक ली। हमने जो किया वह वास्तव में सरल था। मैंने जो कुछ किया वह सरल कार्यक्रमों की शुद्धता साबित कर रहा था जिसमें while लूप, if कथन, और निर्देशों का अनुक्रम शामिल था, लेकिन कुछ भी नहीं। ये विधियां बहुत उपयोगी लगती हैं!

क्या औपचारिक तरीकों का व्यापक रूप से उद्योग में उपयोग किया जाता है?

क्या ये विधियां मिशन-महत्वपूर्ण सॉफ़्टवेयर को साबित करने के लिए उपयोग की जाती हैं?

Answer 1

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

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

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

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

यह शायद एक अच्छा विचार है मुझे मेरी वेबलॉग फिर से शुरू करने, और इस सामान पर कुछ और पोस्ट कर के लिए ...

Answer 2

"क्या उद्योग में औपचारिक तरीकों का उपयोग किया जाता है?"

हां।

assert कई प्रोग्रामिंग भाषाओं में कथन एक कार्यक्रम की पुष्टि के लिए औपचारिक तरीकों से संबंधित है।

"क्या औपचारिक तरीकों का व्यापक रूप से उद्योग में उपयोग किया जाता है?"

सं

"इन तरीकों मिशन के लिए महत्वपूर्ण सॉफ्टवेयर साबित करने के लिए प्रयोग किया जाता है?"

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

Answer 3

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

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

Answer 4

हां, उनका उपयोग किया जाता है, लेकिन सभी क्षेत्रों में व्यापक रूप से नहीं। केवल तर्कसंगत तर्क से अधिक विधियां हैं, कुछ दिए गए कार्य के लिए उपयुक्तता के आधार पर कुछ और अधिक उपयोग किए जाते हैं। आम समस्या यह है कि सोफवेयर biiiiiiig है और यह सत्यापित करना कि यह सब सही है अभी भी एक समस्या है।

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

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

कठोर परीक्षण को औपचारिक सत्यापन के रूप में भी सोचा जा सकता है - कुछ औपचारिक विनिर्देश हैं जिनके कार्यक्रम के पथों का परीक्षण किया जाना चाहिए और इसी तरह।

Answer 5

Polyspace एक एक (घोर रूप से महंगा है, लेकिन बहुत अच्छा) वाणिज्यिक कार्यक्रम सत्यापन के आधार पर उत्पाद है। यह काफी व्यावहारिक है, जिसमें यह 'वर्धित यूनिट परीक्षण' से निकलता है जो शायद आपके जीवन के अगले तीन वर्षों में कुछ बग्स को दिखाएगा, इन 10 फाइलों में शून्य दोष होते हैं।

यह नकारात्मक सत्यापन ('यह प्रोग्राम आपके स्टैक को दूषित नहीं करेगा') पर सकारात्मक सत्यापन के आधार पर अधिक आधारित है ('यह प्रोग्राम सटीक रूप से यह करेगा कि समीकरणों के इन 50 पृष्ठों का क्या कहना है')।

Answer 6

मैं मिशन-महत्वपूर्ण सॉफ़्टवेयर पर ज्यादा टिप्पणी नहीं कर सकता, हालांकि मुझे पता है कि एवियनिक्स उद्योग होयर शैली शैली सहित सॉफ़्टवेयर को सत्यापित करने के लिए विभिन्न प्रकार की तकनीकों का उपयोग करता है।

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

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

औपचारिक तरीकों का अभी तक उद्योग में व्यापक रूप से उपयोग नहीं किया जाता है, लेकिन वे 20 साल पहले की तुलना में अधिक व्यापक रूप से उपयोग किए जाते हैं, और अब से 20 साल अब भी अधिक व्यापक रूप से उपयोग किए जाएंगे। तो आप भविष्य के प्रमाणित हैं :-)

Answer 7

जोर्ग के answer में जोड़ने के लिए, यहां टोनी होयर के साथ interview है। जोर्ग का जिक्र है, मुझे लगता है, प्रीफास्ट और प्रीफिक्स हैं। अधिक जानकारी के लिए here देखें।

Answer 8

उद्योग में औपचारिक तरीकों के दो अलग-अलग दृष्टिकोण हैं।

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

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

http://dblp.uni-trier.de/db/indices/a-tree/d/Delmas:David.html

(माफ करना, केवल एक हाइपरलिंक नए उपयोगकर्ताओं के लिए अनुमति दी :()

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

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

Answer 9

अन्य अधिक प्रक्रियात्मक तरीकों में से इसके अलावा, होरे तर्क अनुबंध द्वारा डिजाइन के आधार में था, एफिल में बर्ट्रेंड मेयेर (see Meyer's article of 1992, पेज 4) द्वारा एक वस्तु उन्मुख तकनीक के रूप में पेश किया। जबकि अनुबंध द्वारा डिज़ाइन औपचारिक सत्यापन विधियों के समान नहीं है (एक बात के लिए, डीबीसी साबित नहीं करता है जब तक सॉफ़्टवेयर निष्पादित नहीं किया जाता है), मेरी राय में यह अधिक व्यावहारिक उपयोग प्रदान करता है।

Answer 10

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

आपके प्रश्न के संबंध में: "क्या औपचारिक तरीके व्यापक रूप से उद्योग में उपयोग की जाती हैं?" और "क्या ये विधियां मिशन-महत्वपूर्ण सॉफ़्टवेयर साबित करने के लिए उपयोग की जाती हैं?"

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

मुझे विश्वास नहीं है कि इन 100% उद्योग खंड इन उपकरणों का उपयोग कर रहे हैं, लेकिन उपयोग बढ़ रहा है। मेरी राय यह है कि एयरोस्पेस और मोटर वाहन उद्योग मेडिकल डिवाइस उद्योग के साथ तेजी से उपयोग को बढ़ाते हैं।