वाणिज्यिक सॉफ़्टवेयर में औपचारिक सत्यापन: एक क्षेत्र रिपोर्ट

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

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

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