सॉफ्टवेयर में औपचारिक तरीके

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

Definition

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

Scope

इस विषय में Z, B, और TLA+ जैसी औपचारिक विनिर्देशन भाषाएँ शामिल हैं; प्रोग्राम की शुद्धता के बारे में तर्क करने के लिए स्वयंसिद्ध सिमेंटिक्स (axiomatic semantics) और होरे लॉजिक (Hoare logic); परिमित-स्थिति (finite-state) और समवर्ती (concurrent) प्रणालियों के सत्यापन के लिए मॉडल चेकिंग (model checking); प्रमेय सिद्ध करना (theorem proving) और प्रूफ असिस्टेंट (proof assistants); और सुरक्षा- तथा संरक्षा-महत्वपूर्ण सॉफ्टवेयर में औपचारिक तरीकों का उपयोग शामिल है।

Core questions

• सॉफ्टवेयर व्यवहार को औपचारिक भाषा में स्पष्ट रूप से कैसे निर्दिष्ट किया जा सकता है?
• किसी विनिर्देशन के संबंध में प्रोग्राम की शुद्धता कैसे सिद्ध की जाती है?
• मॉडल चेकिंग परिमित-स्थिति और समवर्ती प्रणालियों का संपूर्ण सत्यापन कैसे करती है?
• औपचारिक तरीकों की लागत और लाभ उनके उपयोग को कहाँ उचित ठहराते हैं?

Key theories

होरे लॉजिक और स्वयंसिद्ध सिमेंटिक्स (Hoare logic and axiomatic semantics)

होरे ने पूर्व-शर्तों (preconditions) और उत्तर-शर्तों (postconditions) का एक तर्क प्रस्तुत किया जिसमें प्रोग्राम कंस्ट्रक्ट्स (program constructs) की शुद्धता को स्वयंसिद्धों (axioms) और अनुमान नियमों (inference rules) द्वारा व्यक्त किया जाता है, जो यह सिद्ध करने का आधार प्रदान करता है कि प्रोग्राम अपने विनिर्देशों को पूरा करते हैं।

मॉडल चेकिंग (Model checking)

मॉडल चेकिंग अस्थायी-तर्क गुणों (temporal-logic properties) को सत्यापित करने के लिए एक परिमित-स्थिति मॉडल की पहुंच योग्य स्थितियों का स्वचालित रूप से और संपूर्ण रूप से अन्वेषण करती है, जिससे डेडलॉक (deadlocks) और उल्लंघनों का पता चलता है जिन्हें परीक्षण से चूकने की संभावना होती है।

Clinical relevance

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

Evidence & guidelines

औद्योगिक अभ्यास के सर्वेक्षण सुरक्षा-महत्वपूर्ण डोमेन में औपचारिक तरीकों के सफल अनुप्रयोग का दस्तावेजीकरण करते हैं, और DO-178C और कॉमन क्राइटेरिया (Common Criteria) जैसे मानक उच्चतम आश्वासन स्तरों पर औपचारिक तकनीकों को मान्यता देते हैं।

History

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

Debates

औपचारिक तरीकों की मापनीयता (scalability) और लागत

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

Key figures

• C. A. R. Hoare
• Edsger Dijkstra
• Edmund Clarke
• Leslie Lamport

Seminal works

• hoare1969
• clarke1999
• woodcock2009

Frequently asked questions

क्या औपचारिक तरीके परीक्षण की जगह लेते हैं?

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

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

उनके लिए विशेष विशेषज्ञता और प्रयास की आवश्यकता होती है जिसे अधिकांश सॉफ्टवेयर के लिए उचित ठहराना मुश्किल है, जहाँ परीक्षण कम लागत पर पर्याप्त आत्मविश्वास प्रदान करता है; औपचारिक तरीके वहाँ केंद्रित होते हैं जहाँ विफलता के परिणाम निवेश को उचित ठहराने के लिए पर्याप्त गंभीर होते हैं।