💬 NLP

ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking

यह शोध पत्र ESBMC-GraphPLC प्रस्तुत करता है, जो एक औपचारिक सत्यापन उपकरण (formal verification tool) है जो ग्राफ-आधारित रंंग लॉजिक (rung logic) को SMT-आधारित मॉडल चेकिंग के लिए एक वैध GOTO मध्यवर्ती प्रतिनिधित्व (intermediate representation) में परिवर्तित करने हेतु एक DFS-आधारित रिज़ॉल्वर को लागू करके ग्राफिकल PLCopen XML लैडर डायग्राम्स को संभालने में मौजूद अंतर को हल करता है, जिससे मौजूदा टेक्स्टुअल फॉर्मेट सपोर्ट को प्रभावित किए बिना CONTROLLINO और OpenPLC Editor जैसे एडिटर्स से प्रोग्रामों का सही सत्यापन सक्षम होता है।

मूल लेखक: Pierre Dantas, Lucas Cordeiro, Waldir Junior

प्रकाशित 2026-06-19

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Pierre Dantas, Lucas Cordeiro, Waldir Junior

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

एक प्रोग्रामेबल लॉजिक कंट्रोलर (PLC) की कल्पना एक फैक्ट्री मशीन के दिमाग के रूप में करें, जैसे कि एक वॉटर पंप या ट्रैफिक लाइट। इस दिमाग को यह बताने के लिए कि क्या करना है, इंजीनियर लैडर डायग्राम (Ladder Diagrams) बनाते हैं। ये बिजली की सीढ़ियों की तरह दिखते हैं जिनमें पायदान (rungs) होते हैं, जहाँ प्रत्येक पायदान एक नियम है: "यदि पानी का टैंक भर जाता है, तो पंप को बंद कर दें।"

लंबे समय तक, कंप्यूटर पर इन लैडर ड्रॉइंग्स को सहेजने के दो तरीके थे:

टेक्स्ट लिस्ट (The Text List): निर्देशों की एक सरल, चरण-दर-चरण सूची (जैसे कि एक रेसिपी)।
ग्राफिकल मैप (The Graphical Map): एक दृश्य मानचित्र जहाँ टुकड़ों को अदृश्य तारों से जोड़ा जाता है, जिन्हें ID नंबरों द्वारा पहचाना जाता है (जैसे कि एक सबवे मैप जहाँ स्टेशनों को लाइनों से जोड़ा जाता है)।

समस्या: "घोस्ट" (भूतिया) प्रोग्राम

शोधकर्ताओं के पास ESBMC-PLC नामक एक शक्तिशाली टूल था जो सुरक्षा त्रुटियों की जाँच करने के लिए इन प्रोग्रामों को चेक कर सकता था। यह टेक्स्ट लिस्ट फॉर्मेट पर पूरी तरह से काम करता था।

हालाँकि, जब उन्होंने इसमें ग्राफिकल मैप फॉर्मेट (जो कि CONTROLLINO और OpenPLC जैसे आधुनिक सॉफ्टवेयर वास्तव में उपयोग करते हैं) डाला, तो टूल भ्रमित हो गया। इसने मैप को देखा, ID नंबरों और तारों को देखा, लेकिन यह नहीं समझ पाया कि वे कैसे जुड़े हुए हैं।

चूँकि यह मैप को पढ़ नहीं सका, इसने मान लिया कि कुछ भी नहीं हो रहा है। इसने सोचा कि हर स्विच बंद है और हर पंप रुका हुआ है।

परिणाम: टूल ने कहा, "सब कुछ सुरक्षित है!"
पकड़ने वाली बात: यह झूठ बोल रहा था। यह इसलिए सुरक्षित नहीं था क्योंकि लॉजिक मौजूद था; बल्कि यह इसलिए "सुरक्षित" था क्योंकि टूल एक खाली कमरे को देख रहा था। इसे वैक्यूअस वेरिफिकेशन (vacuous verification) कहा जाता है—यह ऐसा है जैसे यह कहना कि एक बंद दरवाजा सुरक्षित है क्योंकि आप यह जांचना भूल गए कि कोई खिड़की खुली है या नहीं।

समाधान: ESBMC-GraphPLC

लेखकों ने इस समस्या को ठीक करने के लिए ESBMC-GraphPLC नामक एक नया मॉड्यूल बनाया। इसे एक डिटेक्टिव (जासूस) को नियुक्त करने जैसा समझें जो ग्राफिकल मैप में घूमकर उसे वापस उस भाषा में अनुवाद कर सके जिसे सुरक्षा जाँचने वाला टूल समझ सके।

यहाँ उनका "डिटेक्टिव" सरल उपमाओं का उपयोग करके कैसे काम करता है, यह दिया गया है:

1. टॉर्च के साथ डिटेक्टिव (DFS एल्गोरिदम)
यह टूल डेप्थ-फर्स्ट सर्च (DFS) नामक एक विधि का उपयोग करता है। कल्पना करें कि एक जासूस तारों की भूलभुलैया में घूम रहा है। वे लैडर के बाईं ओर (पावर सोर्स) से शुरू करते हैं और दाईं ओर के हर संभावित रास्ते का अनुसरण करते हैं।

वे तार के हर कनेक्शन को ट्रेस करते हैं।
वे हर स्विच (कॉन्टैक्ट) को लिखते हैं जिससे वे गुजरते हैं।
वे तब रुकते हैं जब वे डिवाइस (कॉइल/पंप) तक पहुँच जाते हैं।
ऐसा करके, वे लैडर रंंग के सटीक लॉजिक को फिर से बनाते हैं, जिससे विजुअल मैप वापस एक स्पष्ट "If-Then" नियम में बदल जाता है।

2. ट्रैफिक पुलिस (क्रम का महत्व)
इन डायग्रामों में, कभी-कभी एक ही डिवाइस के लिए एक "सेट" स्विच (चालू करने वाला) और एक "रीसेट" स्विच (बंद करने वाला) होता है। क्रम मायने रखता है!

यदि एक ही पल के भीतर "सेट" के बाद "रीसेट" होता है, तो डिवाइस बंद रहता है।
यदि "सेट", "रीसेट" के बाद होता है, तो डिवाइस चालू रहता है।
नया टूल फ़ाइल में एक विशिष्ट सूची (rightPowerRail सीक्वेंस) को देखता है ताकि यह देख सके कि कौन सा स्विच पहले आता है, जो एक ट्रैफिक पुलिस की तरह काम करता है जो सुनिश्चित करता है कि "सेट" कार "रीसेट" कार से पहले जाए। यह सुनिश्चित करता है कि लॉजिक वैसा ही हो जैसा वास्तविक मशीनें व्यवहार करती हैं।

3. अनुमान लगाने का खेल (I/O Inference)
कभी-कभी मैप यह नहीं बताता कि कौन से तार "इनपुट" (सेंसर) हैं और कौन से "आउटपुट" (मोटर) हैं। टूल अनुमान लगाने का तीन-चरणीय खेल खेलता है:

चरण 1: आधिकारिक एड्रेस लेबल (जैसे इनपुट के लिए %IX) देखें। यदि मिले, तो यह सटीक है।
चरण 2: यदि कोई लेबल नहीं है, तो व्यवहार देखें। यदि कोई तार केवल एक स्विच के रूप में उपयोग किया जाता है, तो वह शायद एक इनपुट है। यदि वह केवल किसी चीज़ को चालू करने के लिए उपयोग किया जाता है, तो वह शायद एक आउटपुट है।
चरण 3: यदि अभी भी अनिश्चित हैं, तो इसे एक "रहस्यमय वेरिएबल" के रूप में मानें जो कुछ भी हो सकता है। यह एक सुरक्षित दांव है क्योंकि यह सभी संभावनाओं की जाँच करता है, जिससे यह सुनिश्चित होता है कि कुछ भी छूटा नहीं है।

परिणाम

टीम ने इस नए डिटेक्टिव का परीक्षण तीन वास्तविक-दुनिया के प्रोग्रामों (वॉटर पंप, सीढ़ी की लाइटें, और डिमर लाइटें) पर किया।

पहले: टूल ने एक खाली कमरा देखा और "सुरक्षित" कहा (गलत तरीके से)।
बाद में: टूल ने पूरा लॉजिक देखा, सेंसर इनपुट के हर संभावित संयोजन की जाँच की, और पुष्टि की कि प्रोग्राम वास्तव में सुरक्षित थे।
गति: इसने यह काम 70 मिलीसेकंड से भी कम समय में किया (इंसानी पलक झपकने से भी तेज़)।
सुरक्षा: इसने पुराने टूल को खराब नहीं किया। 11 प्रोग्राम जो टेक्स्ट लिस्ट के साथ पहले से ही काम कर रहे थे, वे भी पूरी तरह से काम करते रहे।

यह अभी क्या नहीं कर सकता (सीमाएँ)

पेपर ईमानदारी से बताता है कि डिटेक्टिव अभी भी किन चीजों के साथ संघर्ष कर रहा है:

जटिल टाइमर (Complex Timers): यदि किसी रंंग में टाइमर शामिल है (जैसे, "5 सेकंड प्रतीक्षा करें, फिर चालू करें"), तो टूल वर्तमान में "प्रतीक्षा" वाले हिस्से को अनदेखा कर देता है और इसे एक रैंडम गेस की तरह मानता है। यह सुरक्षित है, लेकिन यह टाइमिंग को नहीं समझता है।
नेस्टेड मैप्स (Nested Maps): कुछ जटिल डायग्राम अन्य सेक्शन के अंदर छोटे मैप्स छिपा देते हैं (जैसे स्टेप के अंदर एक्शन)। डिटेक्टिव कभी-कभी इन छिपे हुए कमरों को मिस कर देता है।

सारांश

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

तकनीकी सारांश: ESBMC-GraphPLC

समस्या विवरण
यह शोध पत्र ESBMC-PLC टूल का उपयोग करके प्रोग्रामेबल लॉजिक कंट्रोलर (PLC) प्रोग्रामों के औपचारिक सत्यापन (formal verification) में एक महत्वपूर्ण अंतराल को संबोधित करता है। जबकि ESBMC-PLC ने PLCopen XML (tc6_0201) के टेक्स्टुअल फॉर्मेट (textual format) का सफलतापूर्वक समर्थन किया, यह ग्राफिकल फॉर्मेट (graphical format) को सही ढंग से संसाधित करने में विफल रहा, जो कि CONTROLLINO, Beremiz और OpenPLC Editor जैसे प्रमुख विकास परिवेशों के लिए मूल निर्यात (native export) प्रारूप है।

ग्राफिकल फॉर्मेट में, लैडर डायग्राम (LD) लॉजिक को स्पष्ट <rung> तत्वों के बजाय localId और refLocalId कनेक्शनों के एक निर्देशित ग्राफ (directed graph) के रूप में एनकोड किया जाता है। मौजूदा पार्सर ने इन फाइलों का पता तो लगाया लेकिन इसमें कोई रंंग (rungs) नहीं पाए, जिसके परिणामस्वरूप एक खाली GOTO इंटरमीडिएट रिप्रेजेंटेशन (IR) प्राप्त हुआ। फलस्वरूप, सभी वेरिएबल्स शून्य-आरंभीकृत (zero-initialized) रहे, जिससे सत्यापन रिक्त रूप से (vacuously) सफल हुआ: गुण (properties) स्वाभाविक रूप से सत्य सिद्ध हुए क्योंकि कोई लॉजिक उत्पन्न ही नहीं हुआ था। इसने PLC लॉजिक की सुरक्षा के संबंध में कोई वास्तविक गारंटी प्रदान नहीं की।

कार्यप्रणाली (Methodology)
लेखक ESBMC-GraphPLC पेश करते हैं, जो एक मॉड्यूल है जो ग्राफिकल कनेक्शन ग्राफ से रंंग लॉजिक को पुनर्गठित करने के लिए डेप्थ-फर्स्ट सर्च (DFS) आधारित रिज़ॉल्वर को लागू करके इस अंतर को पाटता है। कार्यप्रणाली में तीन मुख्य घटक शामिल हैं:

ग्राफिकल LD रिज़ॉल्वर और रंंग निष्कर्षण (Rung Extraction):
- सिस्टम leftPowerRail से प्रत्येक coil तक के पथों की पहचान करने के लिए localId/refLocalId ग्राफ को पार्स करता है।
- यह ग्राफ का भ्रमण (traverse) करता है ताकि संपर्कों (contacts) के अनुक्रमों को निकाला जा सके, और उन्हें बूलियन कंजंक्शन्स (Boolean conjunctions) में परिवर्तित किया जा सके।
- महत्वपूर्ण क्रम संबंधी अंतर्दृष्टि (Critical Ordering Insight): IEC 61131-3 स्कैन-साइकिल सिमेंटिक्स का पालन करने के लिए, एल्गोरिदम rightPowerRail की connectionPointIn सूची में refLocalId प्रविष्टियों के अनुक्रम के आधार पर कॉइल प्रोसेसिंग को व्यवस्थित करता है। यह सुनिश्चित करता है कि एक ही स्कैन साइकिल के भीतर SET कॉइल्स को RESET कॉइल्स से पहले प्रोसेस किया जाए, जिससे सही लैच व्यवहार (latch behavior) बना रहे।
तीन-स्तरीय I/O अनुमान (Three-Tier I/O Inference):
इनपुट्स (नॉन-डिटरमिनिस्टिक री-सैंपलिंग) और आउटपुट्स (परसिस्टेंट स्टेट) को सही ढंग से मॉडल करने के लिए, टूल एक स्तरीय वर्गीकरण योजना का उपयोग करता है:
- टियर 1: स्पष्ट IEC 61131-3 हार्डवेयर एड्रेस (%IX इनपुट्स के लिए, %QX आउटपुट्स के लिए) का उपयोग करता है।
- टियर 2: एड्रेस-मुक्त प्रोग्रामों के लिए एक ह्यूरिस्टिक विश्लेषण लागू करता है, जिसमें केवल संपर्कों (contacts) के रूप में दिखने वाले वेरिएबल्स को इनपुट और केवल कॉइल्स के रूप में दिखने वाले वेरिएबल्स को आउटपुट के रूप में वर्गीकृत किया जाता है।
- टियर 3: बिना वर्गीकृत वेरिएबल्स को आंतरिक परसिस्टेंट स्टेट (internal persistent state) के रूप में मानता है।
कार्यान्वयन रणनीति (Implementation Strategy):
समाधान को पूरी तरह से फ्रंटएंड पार्सर (plcopen_xml_parser.cpp, +274 पंक्तियाँ) के भीतर लागू किया गया है। इसके लिए ESBMC बैकएंड (जिसमें GOTO IR एनकोडर, k-इंडक्शन इंजन, Z3 SMT सॉल्वर, या प्रॉपर्टी एनकोडर शामिल हैं) में शून्य परिवर्तन की आवश्यकता है। रिज़ॉल्वर एक मानक RungNode सूची आउटपुट करता है, जो टेक्स्टुअल पार्सर द्वारा उत्पन्न संरचना के समान है।

प्रमुख योगदान

औपचारिक मॉडल (Formal Model): ग्राफिकल LD कनेक्शन ग्राफ की एक औपचारिक परिभाषा और एक साउंडनेस थ्योरम (soundness theorem) जो यह सिद्ध करती है कि DFS-एक्सट्रैक्टेड पथ IEC 61131-3 स्कैन-साइकिल सिमेंटिक्स के समकक्ष हैं।
एल्गोरिद्मिक समाधान: ग्राफिकल PLCopen XML के लिए पहले DFS-आधारित रंंग एक्सट्रैक्टर का ओपन-सोर्स कार्यान्वयन जो SET/RESET ऑर्डरिंग को सही ढंग से संभालता है।
बैकवर्ड कम्पैटिबिलिटी: विस्तार (extension) शून्य रिग्रेशन के साथ टेक्स्टुअल LD बेंचमार्क के लिए सभी मौजूदा कार्यक्षमता को सुरक्षित रखता है।
आर्टिफैक्ट: टूल, बेंचमार्क और सत्यापन के लिए एक पायथन प्रोटोटाइप सहित एक पूर्ण, प्रतिलिपि योग्य (reproducible) आर्टिफैक्ट।

प्रायोगिक परिणाम
टूल का मूल्यांकन CONTROLLINO और OpenPLC Editor से निर्यात किए गए 3 ग्राफिकल LD प्रोग्रामों पर किया गया:

वॉटर कंट्रोल (water_control): 5 रंंग (2 SET, 3 RESET)।
स्टेयरकेस लाइट (stairs_light): 6 रंंग (2 SET, 2 RESET, 2 प्लेन)।
डिमर लाइट (dimmer_light_control): 4 रंंग (प्लेन)।

परिणाम:

IR पूर्णता (Completeness): तीनों प्रोग्राम "खाली IR" (vacuous) से "पूर्ण IR" में परिवर्तित हो गए, जिसमें नॉन-डिटरमिनिस्टिक इनपुट्स और पूर्ण रंंग लॉजिक शामिल है।
सत्यापन (Verification): तीनों प्रोग्राम $k=2$ पर 70 ms से कम समय में (औसत समय: 50ms, 40ms, 60ms) SAFE सत्यापित हुए।
रिग्रेशन: 11 वास्तविक टेक्स्टुअल LD बेंचमार्क ने समान परिणाम दिए, जो शून्य रिग्रेशन की पुष्टि करते हैं।

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

महत्व
शोध पत्र का दावा है कि ESBMC-GraphPLC ग्राफिकल PLCopen XML प्रोग्रामों का साउंड, नॉन-वैकअस (non-vacuous) औपचारिक सत्यापन सक्षम करता है, जो आधुनिक PLC विकास परिवेशों का मानक आउटपुट है। ग्राफिकल एक्सपोर्ट और SMT-आधारित मॉडल चेकिंग के बीच के अंतर को पाटकर, यह टूल ऑटोमेशन इंजीनियरों को मैनुअल टेक्स्टुअल रूपांतरण के बिना सुरक्षा गुणों (जैसे पंप नियंत्रण, ट्रैफिक लाइट) को सत्यापित करने की अनुमति देता है। लेखक इस बात पर जोर देते हैं कि जबकि वर्तमान कार्यान्वयन संपर्क/कॉइल नेटवर्क और SET/RESET लैच को प्रभावी ढंग से संभालता है, अधिक जटिल अनुक्रमिक नियंत्रण लॉजिक का समर्थन करने के लिए फंक्शन-ब्लॉक सिमेंटिक्स को एकीकृत करने के लिए भविष्य के कार्य की आवश्यकता है।

समस्या: "घोस्ट" (भूतिया) प्रोग्राम

समाधान: ESBMC-GraphPLC

परिणाम

यह अभी क्या नहीं कर सकता (सीमाएँ)

सारांश

इसी तरह के और पेपर