💻 computer science

CB-VER: A Stable Foundation for Modular Control Plane Verification

यह शोध पत्र \textsc{CB-Ver} को प्रस्तुत करता है, जो एक मॉड्यूलर फ्रेमवर्क है जो समानांतर SMT-आधारित घटक जाँचों और Lean में औपचारिक साउंडनेस प्रमाणों के माध्यम से एक "कनवर्जेस-बिफोर ग्राफ" को संश्लेषित और मान्य करके अंततः-स्थिर नेटवर्क कंट्रोल प्लेन गुणों को सत्यापित करता है, साथ ही वांछित शुद्धता गुणों से घटक इंटरफेस के स्वचालित निर्माण को भी सक्षम बनाता है।

मूल लेखक: Dexin Zhang, Timothy Alberdingk Thijm, David Walker, Aarti Gupta

प्रकाशित 2026-05-21

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

CC BY 4.0

मूल लेखक: Dexin Zhang, Timothy Alberdingk Thijm, David Walker, Aarti Gupta

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

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

यह शोध पत्र CB-VER (कंट्रोल प्लेन वेरिफिकेशन) नामक एक नया टूल पेश करता है जो एक सुपर-स्मार्ट ट्रैफिक इंजीनियर की तरह कार्य करने के लिए डिज़ाइन किया गया है। इसका काम यह सिद्ध करना है कि, शुरुआत में चीजें कितनी भी अराजक क्यों न हों, नेटवर्क अंततः एक शांत, स्थिर अवस्था में स्थापित हो जाएगा जहाँ हर कोई अपने गंतव्य तक पहुँचने के लिए सही रास्ता जान जाएगा।

यह यहाँ कैसे काम करता है, इसे सरल अवधारणाओं में विभाजित किया गया है:

1. समस्या: "अंततः स्थिर" (Eventually Stable) सत्य

इस नेटवर्क शहर में, चीजें शायद ही कभी तुरंत पूर्ण होती हैं। राउटर कुछ सेकंड के लिए भ्रमित हो सकते हैं। लेकिन नेटवर्क ऑपरेटरों को "अंततः-स्थिर गुणों" (eventually-stable properties) की परवाह होती है। इसका अर्थ है: "यदि हम नियमों को बदलना बंद कर दें और सिस्टम को चलने दें, तो क्या हर कोई अंततः एक पथ पर सहमत हो जाएगा और हमेशा उसी पर बना रहेगा?"

इन गुणों के उदाहरण हैं:

पहुँच (Reachability): "क्या हर कोई अंततः अस्पताल तक पहुँच सकेगा?"
एक्सेस कंट्रोल (Access Control): "क्या वीआईपी (VIPs) अंततः प्रतिबंधित क्षेत्र में प्रवेश करने से ब्लॉक हो जाएंगे?"
पथ की लंबाई (Path Length): "क्या हर कोई अंततः सबसे छोटे मार्ग का उपयोग करेगा?"

2. मुख्य विचार: "वादा" और "मानचित्र"

हर चीज़ को सिम्युलेट किए बिना (जिसमें बहुत समय लगेगा) इसकी पुष्टि करने के लिए, CB-VER दो मुख्य अवधारणाओं—इंटरफेस (Interfaces) और CB-ग्राफ (CB-Graph) का उपयोग करते हुए एक चतुर दो-चरणीय रणनीति का उपयोग करता है।

इंटरफेस (द "वादे")

कल्पना करें कि प्रत्येक राउटर एक कारखाने में एक कार्यकर्ता है। प्रत्येक राउटर के हर एक काम की जाँच करने के बजाय, यह टूल उपयोगकर्ता से प्रत्येक राउटर के लिए दो "वादे" (जिन्हें इंटरफेस कहा जाता है) लिखने के लिए कहता है:

"एनीटाइम" वादा (I): एक ढीला वादा कि राउटर के पास किसी भी क्षण कौन से रूट हो सकते हैं (भले ही वह भ्रमित हो)।
"फाइनल" वादा (Q): एक सख्त वादा कि एक बार स्थिर होने के बाद राउटर के पास कौन से रूट होंगे।

यह टूल जाँच करता है कि क्या ये वादे स्थानीय स्तर पर तर्कसंगत हैं। उदाहरण के लिए, यदि राउटर A एक विशिष्ट प्रकार का पैकेज भेजने का वादा करता है, तो क्या राउटर B का वादा यह गारंटी देता है कि वह उस पैकेज को संभाल सकता है?

CB-ग्राफ (द "रिले रेस मैप")

यह इस शोध पत्र का सबसे बड़ा नवाचार है। यह सिद्ध करने के लिए कि नेटवर्क वास्तव में स्थिर हो जाएगा, यह टूल एक विशेष मानचित्र बनाता है जिसे CB-ग्राफ (कन्वर्जेस-बिफोर ग्राफ) कहा जाता है।

इसे एक रिले रेस की तरह समझें:

स्टार्ट लाइन (CB-Roots): कुछ राउटरों के पास तुरंत सही रूट होता है (जैसे रेस शुरू करने वाला व्यक्ति)।
हैंडऑफ्स (CB-Edges): टूल राउटरों के बीच तीर (arrows) खींचता है ताकि यह दिखाया जा सके कि यदि राउटर A के पास सही रूट है, तो वह सफलतापूर्वक मोर्टा (baton) राउटर B को दे सकता है, जिससे यह सुनिश्चित होता है कि राउटर B को भी सही रूट मिल जाए।

यदि टूल एक ऐसा मानचित्र बना सकता है जहाँ प्रत्येक एकल राउटर इन हैंडऑफ्स के माध्यम से स्टार्ट लाइन से जुड़ा हुआ है, तो यह सिद्ध करता है कि "सही व्यवहार" अंततः पूरे नेटवर्क में फैल जाएगा। यदि मानचित्र टूटा हुआ है (कुछ राउटर अलग-थलग हैं), तो नेटवर्क कभी स्थिर नहीं हो पाएगा।

3. यह टूल कैसे काम करता है (प्रक्रिया)

उपयोगकर्ता इनपुट: उपयोगकर्ता नेटवर्क डिज़ाइन और प्रत्येक राउटर के लिए "वादे" (इंटरफेस) प्रदान करता है।
स्थानीय जाँच (Local Check): टूल एक लॉजिक इंजन (एक SMT सॉल्वर) का उपयोग करके यह जाँचता है कि क्या वादे स्थानीय स्तर पर टिकते हैं। "यदि मेरे पास यह है, तो क्या आपको वह मिलेगा?"
मैप बनाना: टूल स्वचालित रूप से CB-ग्राफ बनाता है। यह पूछता है: "क्या हम इन वैध हैंडऑफ्स का उपयोग करके सभी को स्टार्ट लाइन से जोड़ सकते हैं?"
निर्णय (The Verdict):
- सफलता: यदि मानचित्र सभी को जोड़ता है, तो टूल कहता है, "हाँ, नेटवर्क गारंटी के साथ इन गुणों के साथ स्थिर हो जाएगा।"
- विफलता: यदि मानचित्र टूटा हुआ है, तो टूल कहता है, "नहीं, और यहाँ बताया गया है कि कनेक्शन कहाँ विफल हुआ।"

4. बोनस फीचर्स: फॉल्ट टॉलरेंस और ऑटो-डिज़ाइन

इस टूल के दो अतिरिक्त सुपरपावर्स हैं:

फॉल्ट टॉलरेंस (द "ब्रेक-प्रूफ" टेस्ट):
यह टूल टूटी हुई सड़कों (विफल कनेक्शनों) का अनुकरण कर सकता है। यह पूछता है, "यदि हम इन हैंडऑफ तीरों में से 1, 2, या 3 को काट दें, तो क्या मानचित्र अभी भी जुड़ा रहेगा?" यदि मानचित्र टूटी हुई रेखाओं के बावजूद जुड़ा रहता है, तो नेटवर्क फॉल्ट-टॉलरेंट है। यह इंजीनियरों को ठीक से बताता है कि उनका सिस्टम कितना लचीला है।
ऑटो-सिंथेसिस (द "रिवर्स इंजीनियर"):
आमतौर पर, मनुष्यों को "वादे" लिखने होते हैं। लेकिन CB-VER भी उल्टा काम कर सकता है। यदि आप इसे एक पूर्ण मानचित्र (एक जुड़ा हुआ CB-ग्राफ) देते हैं, तो यह एक अलग लॉजिक इंजन का उपयोग करके प्रत्येक राउटर के लिए स्वचालित रूप से वादे लिख सकता है। यह ऐसा है जैसे कहना, "यहाँ एक पूर्ण रिले रेस प्लान है; मुझे बताएं कि प्रत्येक धावक को इसे पूरा करने के लिए किन नियमों का पालन करने की आवश्यकता है।"

सारांश

CB-VER एक सत्यापन टूल है जो यह सिद्ध करता है कि जटिल कंप्यूटर नेटवर्क अंततः शांत होकर सही ढंग से काम करेंगे। यह इसे तीन चरणों में करता है:

नेटवर्क के प्रत्येक हिस्से से सरल "वादे" (Interfaces) मांगकर।
यह सिद्ध करने के लिए कि सही व्यवहार सभी तक फैलता है, एक "रिले रेस मैप" (CB-Graph) स्वचालित रूप से बनाकर।
यह जाँचकर कि क्या नेटवर्क टूटे हुए कनेक्शनों से बच सकता है।
यहाँ तक कि यदि आप उन्हें मानचित्र प्रदान करते हैं, तो यह आपके लिए नियम भी लिख सकता है।

लेखकों ने सिद्ध किया है कि उनका गणित सही है (Lean नामक एक औपचारिक तर्क प्रणाली का उपयोग करके) और वास्तविक दुनिया के नेटवर्क उदाहरणों पर इसका परीक्षण किया, जिससे पता चला कि यह पुराने तरीकों की तुलना में तेज़ है और बड़े, जटिल सिस्टम को बेहतर ढंग से संभालता है।

तकनीकी सारांश: CB-VER: मॉड्यूलर कंट्रोल प्लेन सत्यापन के लिए एक स्थिर आधार

1. समस्या विवरण (Problem Statement)

नेटवर्क ऑपरेटर विशाल, जटिल नेटवर्क का प्रबंधन करते हैं जहाँ कंट्रोल प्लेन में कॉन्फ़िगरेशन त्रुटियां अक्सर महत्वपूर्ण आउटेज (outages) का कारण बनती हैं। ये विफलताएं अक्सर इवेंचुअली-स्टेबल प्रॉपर्टीज (eventually-stable properties) के उल्लंघन से उत्पन्न होती हैं—ऐसी स्थितियाँ जो, एक बार समय $\tau$ पर स्थापित होने के बाद, तब तक बनी रहती हैं जब तक कि वातावरण अपरिवर्तित रहता है। उदाहरणों में इवेंचुअल रीचेबिलिटी (eventual reachability), एक्सेस कंट्रोल, और पाथ लेंथ कंस्ट्रेंट्स शामिल हैं।

मौजूदा सत्यापन उपकरण सीमाओं का सामना करते हैं:

मोनोलिथिक दृष्टिकोण (Monolithic approaches) (जैसे Minesweeper) नेटवर्क के आकार और जटिल नीतियों के साथ स्केल करने में संघर्ष करते हैं।
मॉड्यूलर दृष्टिकोण (Modular approaches) (जैसे Timepiece, Lightyear) अक्सर सिंक्रोनस नेटवर्क मॉडल, मैनुअल पाथ स्पेसिफिकेशन की मांग करते हैं, या लिवनेस प्रॉपर्टीज (liveness properties) और फॉल्ट टॉलरेंस विश्लेषण का समर्थन करने में विफल रहते हैं।
ऐसे टूल्स की कमी है जो इन गुणों को सिद्ध करने के लिए आवश्यक एब्स्ट्रैक्शन (interfaces) को स्वचालित रूप से सिंथेसाइज कर सकें या सत्यापन संरचना के आधार पर फॉल्ट टॉलरेंस का विश्लेषण कर सकें।

2. कार्यप्रणाली: एब्स्ट्रैक्ट कन्वर्जेंस और CB-ग्राफ्स (Methodology: Abstract Convergence and CB-Graphs)

लेखक CB-VER प्रस्तावित करते हैं, जो एब्स्ट्रैक्ट कन्वर्जेंस के एक नए सिद्धांत पर आधारित एक मॉड्यूलर वेरिफिकेशन फ्रेमवर्क है। मुख्य कार्यप्रणाली में तीन मुख्य घटक शामिल हैं:

A. नेटवर्क मॉडल और सिमेंटिक्स (Network Model and Semantics)

कंट्रोल प्लेन को एक एसिंक्रोनस मैसेज-पासिंग सिस्टम के रूप में मॉडल किया गया है जहाँ राउटर (जैसे BGP, OSPF, या RIP प्रोटोकॉल का उपयोग करके) रूट्स (संदेशों) का आदान-प्रदान करते हैं। मॉडल रूट्स, मर्ज फंक्शन्स (रूट चयन), और ट्रांसफर फंक्शन्स (पॉलिसी अनुप्रयोग) को दर्शाने के लिए एक मल्टी-सॉर्टेड फर्स्ट-ऑर्डर थ्योरी (SMT में एनकोडेड) का उपयोग करता है। सिमेंटिक्स 'फेयर शेड्यूल्स' को मानते हैं जहाँ संदेश अंततः डिलीवर हो जाते हैं।

B. मॉड्यूलर इंटरफेस ( $I$ और $Q$ )

मॉड्यूलर वेरिफिकेशन को सक्षम करने के लिए, प्रत्येक नेटवर्क डिवाइस $v$ को दो इंटरफेस के साथ जोड़ा जाता है:

$I(v)$ (इनवेरिएंट इंटरफेस): उन सभी स्टेट्स (रूट्स) का ओवर-एप्रोक्सिमेशन जो डिवाइस निष्पादन के दौरान किसी भी समय में प्रवेश कर सकता है।
$Q(v)$ (कन्वर्जेंस इंटरफेस): उन इवेंचुअली-स्टेबल स्टेट्स का ओवर-एप्रोक्सिमेशन जहाँ डिवाइस अभिसरित (converge) होता है।

सत्यापन रणनीति दोहरी है:

यह सिद्ध करना कि सभी नोड्स अंततः $Q(v)$ के भीतर की स्टेट्स में अभिसरित होते हैं।
यह सिद्ध करना कि $Q(v)$ की प्रत्येक स्टेट उपयोगकर्ता के करेक्टनेस प्रॉपर्टी $Y(v)$ को संतुष्ट करती है (अर्थात $Q(v) \implies Y(v)$ )।

C. द कन्वर्जेस-बिफोर (CB) ग्राफ

नेटवर्क $Q$ की ओर अभिसरित होता है, यह सिद्ध करने के लिए, फ्रेमवर्क CB-ग्राफ पेश करता है, जो कन्वर्जेंस प्रक्रिया का एक विटनेस (witness) है।

CB-Roots: वे नोड्स जो $t=0$ पर तुरंत $Q(v)$ की ओर अभिसरित होते हैं (जैसे बॉर्डर नोड्स जो रूट्स उत्पन्न करते हैं)।
CB-Edges: निर्देशित किनारे (directed edges) $(u, v)$ जहाँ $u \in Q(u)$ से $v$ को रूट का स्थानांतरण यह गारंटी देता है कि $v$ अपनी $I(v)$ में पूर्व स्थिति की परवाह किए बिना $Q(v)$ में एक रूट चुनेगा।

थ्योरम 1: यदि एक CB-ग्राफ कनेक्टेड है (प्रत्येक नोड CB-एज के माध्यम से एक CB-रूट से जुड़ा हुआ है) और सभी लोकल वेरिफिकेशन कंडीशंस लागू होती हैं, तो पूरा नेटवर्क अमूर्त रूप से $Q$ की ओर अभिसरित होता है।

3. मुख्य योगदान (Key Contributions)

1. CB-VER वेरिफिकेशन एल्गोरिदम

CB-VER निम्नलिखित चरणों के माध्यम से सत्यापन प्रक्रिया को स्वचालित करता है:

लोकल वेरिफिकेशन कंडीशंस (VCs): यह निम्नलिखित के लिए SMT-आधारित VCs बनाता है और जाँचता है:
- इनवेरिएंट मेंटेनेंस: यह सुनिश्चित करना कि $I$ एक इंडक्टिव इनवेरिएंट है ( $VC_{Init}$ , $VC_{Inv}$ )।
- प्रॉपर्टी इम्प्लिकेशन: यह सुनिश्चित करना कि $Q$ , वांछित प्रॉपर्टी $Y$ को दर्शाता है ( $VC_{Prop}$ )।
- CB-ग्राफ निर्माण: वैध CB-roots ( $VC_{CBroot}$ ) और CB-edges ( $VC_{CBedge}$ ) की पहचान करना।
पैरेलल सिंथेसिस: टूल सभी नोड्स और एडजेस को समानांतर में चेक करके एक मैक्सिमल CB-ग्राफ को स्वचालित रूप से सिंथेसाइज करता है।
कनेक्टिविटी चेक: यह सत्यापित करने के लिए ग्राफ ट्रैवर्सल करता है कि क्या सिंथेसाइज किया गया CB-ग्राफ सभी नोड्स को जोड़ता है। यदि कनेक्टेड है, तो प्रॉपर्टी को सत्यापित माना जाता है।

2. फॉल्ट टॉलरेंस विश्लेषण (Fault Tolerance Analysis)

सिंथेसाइज किया गया CB-ग्राफ दिए गए इंटरफेसेस के लिए मैक्सिमल कनेक्टिविटी का प्रतिनिधित्व करता है। इस ग्राफ की कनेक्टिविटी का विश्लेषण करके, CB-VER $k$ -फॉल्ट टॉलरेंस निर्धारित कर सकता है: यदि $k$ एड्स हटाने के बाद भी CB-ग्राफ कनेक्टेड रहता है, तो नेटवर्क किसी भी $k$ एज फेलियर के संयोजन के तहत सही रहता है। इसे डिनिट्ज़ (Dinitz) एल्गोरिथ्म के एक वेरिएंट का उपयोग करके लागू किया गया है।

3. ऑटोमेटेड इंटरफेस सिंथेसिस (CB-2IQ)

पेपर "उलटे प्रश्न" को संबोधित करता है: दिए गए CB-ग्राफ और प्रॉपर्टी $Y$ को देखते हुए, क्या हम इंटरफेस $I$ और $Q$ को सिंथेसाइज कर सकते हैं?

लेखक इसे एक कॉन्स्ट्रेंड हॉर्न क्लॉज (CHC) समस्या के रूप में फॉर्म्युलेट करते हैं।
उन्होंने एक प्रोटोटाइप टूल, CB-2IQ विकसित किया है, जो ऑफ-द-शेल्फ CHC सॉल्वर (जैसे Spacer/Z3) का उपयोग करके वैध इंटरफेस $I$ और $Q$ को स्वचालित रूप से जेनरेट करता है जो वेरिफिकेशन कंडीशंस को संतुष्ट करते हैं।

4. फॉर्मल साउंडनेस (Formal Soundness)

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

4. मूल्यांकन परिणाम (Evaluation Results)

लेखकों ने तीन बेंचमार्क सेट्स पर CB-VER और CB-2IQ का मूल्यांकन किया: सिंथेटिक फैट-ट्री नेटवर्क (20–2000 नोड्स), वास्तविक दुनिया का इंटरनेट2 नेटवर्क (~300 नोड्स), और बैटफिश (Batfish) ट्यूटोरियल नेटवर्क।

एक्सप्रेसिवनेस (RQ1): CB-VER ने सभी नेटवर्क आकारों और टोपोलॉजी में विविध प्रॉपर्टीज (रीचेबिलिटी, पाथ लेंथ, वैली-फ्री, हाइजैक प्रिवेंशन) को सफलतापूर्वक सत्यापित किया।
परफॉरमेंस (RQ2):
- CB-VER प्रभावी ढंग से स्केल करता है, 2000-नोड वाले फैट-ट्री नेटवर्क पर प्रॉपर्टीज को 20 मिनट के भीतर सत्यापित करता है।
- यह मोनोलिथिक वेरीफायर (Minesweepers-स्टाइल) की तुलना में काफी बेहतर प्रदर्शन करता है, जो बड़े इंस्टेंस पर अक्सर टाइम-आउट हो जाता था या मेमोरी की कमी का सामना करता था।
- प्रदर्शन आम तौर पर मॉड्यूलर वेरीफायर Timepiece के तुलनीय है, जिसमें CB-VER जटिल पॉलिसी बेंचमार्क (वैली-फ्री) में मामूली सुधार और सरल रीचेबिलिटी चेक में थोड़ा ओवरहेड दिखाता है।
फॉल्ट टॉलरेंस (RQ3): टूल ने सफलतापूर्वक पुश-बटन फॉल्ट टॉलरेंस विश्लेषण किया। उदाहरण के लिए, इसने निर्धारित किया कि एक 2000-नोड वाला फैट-ट्री रीचेबिलिटी के लिए 19 एज फेलियर को सहन कर सकता है।
इंटरफेस सिंथेसिस: CB-2IQ ने फैट-ट्री नेटवर्क के लिए इंटरफेस सफलतापूर्वक सिंथेसाइज किए। अधिकांश मामलों में, यह मोनोलिथिक वेरिफिकेशन की तुलना में तेज़ था (रीचेबिलिटी के लिए 27 गुना तक तेज़), जो दर्शाता है कि ऑटोमेटेड सिंथेसिस मैनुअल इंटरफेस स्पेसिफिकेशन का एक व्यवहार्य विकल्प है।

5. महत्व और दावे (Significance and Claims)

पेपर का दावा है कि CB-VER मॉड्यूलर कंट्रोल प्लेन वेरिफिकेशन के लिए एक स्थिर आधार प्रदान करता है क्योंकि यह:

मॉड्यूलर वेरिफिकेशन का सामान्यीकरण करता है: यह पिछले मॉड्यूलर टूल्स की तुलना में एसिंक्रोनस नेटवर्क और अधिक व्यापक क्लास की इवेंचुअली-स्टेबल प्रॉपर्टीज का समर्थन करता है।
"विटनेस" को स्वचालित करता है: मैनुअल पाथ स्पेसिफिकेशन की आवश्यकता वाले टूल्स के विपरीत, CB-VER स्वचालित रूप से CB-ग्राफ को सिंथेसाइज करता है, जो कन्वर्जेंस विटनेस के रूप में कार्य करता है।
फॉल्ट टॉलरेंस को सक्षम बनाता है: यह अद्वितीय रूप से वेरिफिकेशन स्ट्रक्चर (CB-ग्राफ) को सीधे फॉल्ट टॉलरेंस विश्लेषण से जोड़ता है, जिससे इंजीनियर लचीलेपन (resilience) को माप सकते हैं।
लूप को बंद करता है: CB-2IQ के माध्यम से, यह प्रदर्शित करता है कि वांछित कन्वर्जेंस स्ट्रक्चर से इंटरफेस को स्वचालित रूप से सिंथेसाइज किया जा सकता है, जिससे नेटवर्क ऑपरेटरों पर मैनुअल बोझ कम होता है।

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