ESBMC-PLC+: A Unified IEC~61131-3 Formal Verification Framework as a PLCverif Successor
यह शोध पत्र ESBMC-PLC+ प्रस्तुत करता है, जो एक एकीकृत ओपन-सोर्स फ्रेमवर्क है जो ESBMC बैकएंड को सभी प्रमुख IEC 61131-3 भाषाओं (लैडर डायग्राम और स्ट्रक्चर्ड टेक्स्ट सहित) और अनबाउंडेड वेरिफिकेशन (unbounded verification) का समर्थन करने के लिए विस्तारित करता है, जिससे यह अपने पूर्ववर्ती PLCverif की इनपुट फॉर्मेट सीमाओं और बाउंडेड प्रूफ बाधाओं को दूर करता है और टाइमर-हैवी प्रोग्रामों को सत्यापित करने में nuXmv से काफी बेहतर प्रदर्शन करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
एक प्रोग्रामेबल लॉजिक कंट्रोलर (PLC) की कल्पना एक फैक्ट्री मशीन के मस्तिष्क के रूप में करें। यह एक कठिन, औद्योगिक कंप्यूटर है जो रोबोटों, वाल्वों और लाइटों को बताता है कि उन्हें कब हिलना है, रुकना है, या अपना रंग बदलना है। ये मशीनें एक सख्त, दोहराने वाले लूप पर चलती हैं जिसे "स्कैन साइकिल" कहा जाता है, जो सेकंड में हजारों बार सेंसर की जांच करती है और निर्णय लेती है। चूंकि ये मशीनें परमाणु ऊर्जा संयंत्रों और ट्रेन संकेतों जैसी चीजों को नियंत्रित करती हैं, इसलिए कोड में एक भी गलती विनाशकारी हो सकती है।
फॉर्मल वेरिफिकेशन (Formal verification) एक सुपर-स्मार्ट, गणितीय प्रूफरीडर की तरह है जो मशीन के हर एक संभावित परिदृश्य (scenario) की जांच करता है जिसे वह कभी भी झेल सकती है, ताकि यह सुनिश्चित किया जा सके कि वह कभी क्रैश न हो या खतरनाक व्यवहार न करे।
वर्षों तक, इस काम के लिए सबसे अच्छा ओपन-सोर्स टूल PLCverif नाम का था। सोचिए कि PLCverif एक अत्यधिक कुशल मैकेनिक है जो कारें (टेक्स्ट-आधारित कोड) ठीक करने में बहुत अच्छा है, लेकिन मोटरसाइकिल (लैडर डायग्राम) के हुड के नीचे देखने से इनकार करता है या उसके पास यह साबित करने के लिए सही उपकरण नहीं हैं कि इंजन बिना ओवरहीट हुए हमेशा चलता रहेगा।
यह पेपर ESMC-PLC+ पेश करता है, जो एक नया, अपग्रेड किया गया "सुपर-मैकेनिक" है जिसे PLCverif को बदलने और सुधारने के लिए डिज़ाइन किया गया है। यह क्या करता है, इसे सरल भाषा में यहाँ समझाया गया है:
1. हर भाषा बोलना (एक एकीकृत ढांचा - The Unified Framework)
PLC प्रोग्रामर तीन मुख्य भाषाएँ बोलते हैं:
- लैडर डायग्राम (LD): यह एक इलेक्ट्रिकल सर्किट डायग्राम की तरह दिखता है जिसमें रन्स (rungs) और रेल्स (rails) होते हैं। यह उद्योगों में सबसे लोकप्रिय भाषा है (जैसे उद्योग की "अंग्रेजी")।
- स्ट्रक्चर्ड टेक्स्ट (ST): यह मानक कंप्यूटर कोड की तरह दिखता है (पैस्कल या सी के समान)।
- ग्राफिकल LD: लैडर डायग्राम का विजुअल वर्जन।
समस्या: पुराना टूल (PLCverif) केवल "स्ट्रक्चर्ड टेक्स्ट" भाषा को पढ़ सकता था। यदि किसी इंजीनियर के पास लैडर डायग्राम होता, तो उसे इसे मैन्युअल रूप से टेक्स्ट में फिर से लिखना पड़ता था, जो धीमा था और गलतियों की संभावना से भरा था। साथ ही, यदि लैडर डायग्राम में जटिल "फंक्शन ब्लॉक्स" (जैसे टाइमर या काउंटर) थे, तो पुराना टूल उन्हें बिल्कुल भी हैंडल नहीं कर पाता था।
समाधान: ESBMC-PLC+ एक यूनिवर्सल ट्रांसलेटर है। यह मूल रूप से तीनों भाषाओं को पढ़ सकता है।
- स्ट्रक्चर्ड टेक्स्ट (ST) के लिए, यह एक भरोसेमंद ओपन-सोर्स कंपाइलर (MATIEC) का उपयोग करता है ताकि कोड को उस प्रारूप में अनुवादित किया जा सके जिसे वेरिफिकेशन इंजन समझ सके।
- लैडर डायग्राम (LD) के लिए, इसमें एक नया "डिकोडर" है जो अब उन जटिल टाइमर और काउंटरों को समझ सकता है जिन्हें पहले अनदेखा कर दिया जाता था।
2. "हमेशा के लिए" गारंटी (अनबाउंडेड प्रूफ - Unbounded Proofs)
कल्पना कीजिए कि आप एक पुल का परीक्षण कर रहे हैं।
- बाउंडेड चेकिंग (पुराना तरीका): आप पुल के ऊपर से 100 बार ट्रक चलाते हैं। यदि यह टिक जाता है, तो आप कहते हैं, "यह शायद सुरक्षित है।" लेकिन आपको नहीं पता कि 101वीं बार में क्या होगा, या यदि 1,000 साल बाद पुल ढह जाता है। यही वह काम था जो पुराने टूल का प्राथमिक इंजन (CBMC) करता था।
- अनबाउंडेड प्रूफ (नया तरीका): ESBMC-PLC+ k-induction नामक तकनीक का उपयोग करता है। केवल 100 बार जांचने के बजाय, यह गणित का उपयोग करके यह सिद्ध करता है कि यदि पुल पहले कुछ सेकंड के लिए सुरक्षित रहता है, तो यह अनंत काल (infinity) तक सुरक्षित रहेगा। यह गारंटी देता है कि मशीन कभी विफल नहीं होगी, चाहे वह कितने भी लंबे समय तक चले।
3. स्पीड डेमन (SMT बनाम BDD)
पेपर ESBMC-PLC+ की तुलना पुराने टूल के "अनबाउंडेड" इंजन (nuXmv) से करता है, जो BDD (बाइनरी डिसीजन डायग्राम्स) नामक विधि का उपयोग करता है।
- उपमा (Analogy): कल्पना कीजिए कि आपके पास किताबों का एक विशाल पुस्तकालय है (मशीन की सभी संभावित अवस्थाएं)।
- पुराना टूल (BDD) एक-एक करके हर किताब को पढ़ने की कोशिश करता है। यदि पुस्तकालय बहुत बड़ा है (क्योंकि मशीन में कई टाइमर या काउंटर हैं), तो यह अभिभूत हो जाता है और काम करना बंद कर देता है (टाइम आउट हो जाता है)।
- ESBMC-PLC+ (SMT) एक जादुई इंडेक्स का उपयोग करता है। हर किताब को एक-एक करके पढ़ने के बजाय, यह पूरे पुस्तकालय के तर्क (logic) की जांच करने के लिए एक सुपर-इंटेलिजेंट लाइब्रेरियन (एक SMT सॉल्वर) से पूछता है।
- परिणाम: टाइमर वाले प्रोग्रामों पर, ESBMC-PLC+ पुराने टूल की तुलना में 400 से 2,000 गुना तेज़ था। कुछ मामलों में, पुराने टूल ने 2 मिनट के बाद हार मान ली, जबकि ESBC-PLC+ ने एक सेकंड से भी कम समय में प्रमाण (proof) पूरा कर लिया।
4. इसने वास्तव में क्या ठीक किया
पेपर दो विशिष्ट "अंतरालों" (gaps) को उजागर करता जिन्हें इसने भरा:
- लुप्त टेक्स्ट: इसने स्ट्रक्चर्ड टेक्स्ट (ST) प्रोग्रामों के लिए समर्थन जोड़ा, जिसे पुराना टूल खराब तरीके से हैंडल करता था या बिल्कुल नहीं करता था।
- "घोस्ट" टाइमर: विजुअल लैडर डायग्राम्स में, कुछ "फंक्शन ब्लॉक्स" थे (जैसे टाइमर जो लाइट जलाने से पहले 5 सेकंड प्रतीक्षा करते हैं)। पुराना टूल इन ब्लॉक्स को अनदेखा कर देता था, प्रभावी रूप से यह मान लेता था कि वे मौजूद ही नहीं हैं। इससे "वैक्यूअस" (vacuous) परिणाम मिलते थे—जहाँ टूल कहता था "सुरक्षित!" सिर्फ इसलिए क्योंकि वह खतरनाक हिस्सों को देख ही नहीं रहा था। ESBMC-PLC+ अब इन टाइमरों को सही ढंग से मॉडल करता है, जिससे यह सुनिश्चित होता है कि सुरक्षा जांच वास्तविक है, न कि कोई दिखावा।
सारांश
ESBMC-PLC+ एक नया, ओपन-सोर्स टूल है जो औद्योगिक मशीन कोड के लिए एक यूनिवर्सल ट्रांसलेटर के रूप में कार्य करता है। यह उन सभी प्रमुख भाषाओं को बोलता है जिनका इंजीनियर उपयोग करते हैं, टाइमर और काउंटर के साथ जटिल विजुअल डायग्राम को संभालता है, और यह सिद्ध करने के लिए एक तेज़, स्मार्ट गणितीय इंजन का उपयोग करता है कि मशीनें केवल एक छोटे परीक्षण के लिए नहीं, बल्कि हमेशा के लिए सुरक्षित रहेंगी। इसे पिछले उद्योग मानक, PLCverif के सीधे और बेहतर उत्तराधिकारी के रूप में डिज़ाइन किया गया है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।