2025-11-24T00:55:25.034139

PolyVer: A Compositional Approach for Polyglot System Modeling and Verification

Chen, Lin, Godbole et al.
Several software systems are polyglot; that is, they comprise programs implemented in a combination of programming languages. Verifiers that directly run on mainstream programming languages are currently customized for single languages. Thus, to verify polyglot systems, one usually translates them into a common verification language or formalism on which the verifier runs. In this paper, we present an alternative approach, PolyVer, which employs abstraction, compositional reasoning, and synthesis to directly perform polyglot verification. PolyVer constructs a formal model of the original polyglot system as a transition system where the update functions associated with transitions are implemented in target languages such as C or Rust. To perform verification, PolyVer then connects a model checker for transition systems with language-specific verifiers (e.g., for C or Rust) using pre/post-condition contracts for the update functions. These contracts are automatically generated by synthesis oracles based on syntax-guided synthesis or large language models (LLMs), and checked by the language-specific verifiers. The contracts form abstractions of the update functions using which the model checker verifies the overall system-level property on the polyglot system model. PolyVer iterates between counterexample-guided abstraction-refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS) until the property is verified or a true system-level counterexample is found. We demonstrate the utility of PolyVer for verifying programs in the Lingua Franca polyglot language using the UCLID5 model checker connected with the CBMC and Kani verifiers for C and Rust respectively.
academic

PolyVer: बहुभाषी प्रणाली मॉडलिंग और सत्यापन के लिए एक संयोजन दृष्टिकोण

मूल जानकारी

  • पेपर ID: 2503.03207
  • शीर्षक: PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
  • लेखक: Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, Sanjit A. Seshia
  • वर्गीकरण: cs.PL (प्रोग्रामिंग भाषाएं)
  • प्रकाशन समय/सम्मेलन: Formal Methods in Computer-Aided Design 2025
  • पेपर लिंक: https://arxiv.org/abs/2503.03207

सारांश

बहुभाषी सॉफ्टवेयर प्रणालियां (polyglot systems) कई प्रोग्रामिंग भाषाओं में लागू किए गए प्रोग्राम के संयोजन से बनी होती हैं, लेकिन मौजूदा प्रोग्राम सत्यापक आमतौर पर केवल एकल भाषा के लिए अनुकूलित होते हैं। बहुभाषी प्रणालियों को सत्यापित करने के लिए, आमतौर पर उन्हें एक सामान्य सत्यापन भाषा या औपचारिक प्रतिनिधित्व में अनुवाद करने की आवश्यकता होती है। यह पेपर PolyVer प्रस्तुत करता है, जो सीधे बहुभाषी सत्यापन करने के लिए अमूर्तता, संयोजन तर्क और संश्लेषण तकनीकों का उपयोग करने का एक वैकल्पिक तरीका है। PolyVer बहुभाषी प्रणालियों को संक्रमण प्रणालियों के औपचारिक मॉडल के रूप में निर्मित करता है, जहां संक्रमण-संबंधित अपडेट फ़ंक्शन लक्ष्य भाषा (जैसे C या Rust) में लागू किए जाते हैं। सत्यापन को निष्पादित करने के लिए, PolyVer अपडेट फ़ंक्शन के पूर्व/पश्च शर्त अनुबंधों के माध्यम से संक्रमण प्रणाली के मॉडल चेकर को भाषा-विशिष्ट सत्यापक से जोड़ता है। ये अनुबंध स्वचालित रूप से वाक्य-विन्यास-निर्देशित संश्लेषण या बड़े भाषा मॉडल के आधार पर संश्लेषण ओरेकल के माध्यम से उत्पन्न होते हैं, और भाषा-विशिष्ट सत्यापक द्वारा जांचे जाते हैं।

अनुसंधान पृष्ठभूमि और प्रेरणा

समस्या परिभाषा

आधुनिक सॉफ्टवेयर प्रणालियां तेजी से बहुभाषी आर्किटेक्चर को अपना रही हैं, जैसे ROS2, Lingua Franca जैसे ढांचे डेवलपर्स को विभिन्न घटकों के लिए सबसे उपयुक्त प्रोग्रामिंग भाषा चुनने की अनुमति देते हैं। हालांकि, यह लचीलापन सत्यापन चुनौतियां लाता है:

  1. भाषा शब्दार्थ अंतर: विभिन्न प्रोग्रामिंग भाषाओं में अलग-अलग वाक्य-विन्यास और शब्दार्थ होते हैं, जैसे Rust का saturating_add फ़ंक्शन ओवरफ्लो पर अधिकतम मान तक संतृप्त होता है, जबकि C का जोड़ लपेट सकता है।
  2. मौजूदा सत्यापक सीमाएं: अधिकांश प्रोग्राम सत्यापक (जैसे C के लिए CBMC, Rust के लिए Kani) एकल भाषा के लिए विशेष रूप से डिज़ाइन किए गए हैं और बहुभाषी प्रणालियों को सीधे संभाल नहीं सकते।
  3. अनुवाद जटिलता: संपूर्ण बहुभाषी प्रणाली को एकल सत्यापन भाषा में अनुवाद करने के लिए सभी भाषाओं के पूर्ण वाक्य-विन्यास और शब्दार्थ का समर्थन करने की आवश्यकता होती है, जो आधुनिक भाषाओं के लिए निषेधात्मक है।

अनुसंधान महत्व

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

मौजूदा विधियों की सीमाएं

  • एकीकृत अनुवाद विधि: प्रत्येक भाषा के लिए संपूर्ण कंपाइलर बुनियादी ढांचा विकसित करने की आवश्यकता है
  • शब्दार्थ संरक्षण कठिनाई: लक्ष्य सत्यापन भाषा में स्रोत भाषा के सभी भाषा-विशिष्ट निर्माणों को वफादारी से कैप्चर करना मुश्किल है
  • स्केलेबिलिटी समस्याएं: उत्पन्न सत्यापन समस्या बहुत बड़ी हो सकती है

मुख्य योगदान

  1. बहुभाषी सत्यापन समस्या का औपचारिकीकरण: पहली बार बहुभाषी सत्यापन समस्या को व्यवस्थित रूप से औपचारिक बनाया गया और कई भाषा-विशिष्ट सत्यापकों को एकीकृत करने का संयोजन समाधान प्रस्तावित किया गया।
  2. स्वचालित अनुबंध संश्लेषण: मध्यवर्ती भाषा और CEGIS-CEGAR चक्र का उपयोग करके पूर्व/पश्च शर्त अनुबंधों के स्वचालित संश्लेषण और परिशोधन विधि प्रस्तावित की गई, जो वाक्य-विन्यास-निर्देशित संश्लेषण और बड़े भाषा मॉडल को संश्लेषण ओरेकल के रूप में समर्थन करती है।
  3. उपकरण कार्यान्वयन: UCLID5 के आधार पर PolyVer उपकरण लागू किया गया, जो C और Rust का समर्थन करता है, CBMC और Kani सत्यापकों के माध्यम से, यह प्रदर्शित करता है कि LLM-आधारित संश्लेषण ओरेकल शुद्ध प्रतीकात्मक संश्लेषण विधि से बेहतर है।
  4. केस स्टडी और मूल्यांकन: Lingua Franca समन्वय भाषा के लिए सत्यापक विकसित किया गया, C और Rust प्रक्रियाओं वाली बहुभाषी प्रणालियों को सत्यापित किया गया, साथ ही C भाषा के टुकड़े जो पिछले काम द्वारा समर्थित नहीं थे।

विधि विस्तार

कार्य परिभाषा

इनपुट: बहुभाषी मॉडल M = (Q,V,I₀,T,F) और प्रणाली गुण φ आउटपुट: सत्यापन परिणाम (पास/विफल) और संभावित प्रतिउदाहरण ट्रेस उद्देश्य: यह निर्धारित करना कि M ⊨ φ सत्य है या नहीं

जहां:

  • Q: मोड का समुच्चय
  • V: टाइप किए गए चर का समुच्चय
  • I₀: प्रारंभिक अवस्था का समुच्चय
  • T: मोड संक्रमण का समुच्चय
  • F: प्रक्रिया का समुच्चय

मॉडल आर्किटेक्चर

1. विस्तारित अवस्था मशीन (ESM)

PolyVer बहुभाषी प्रणालियों को विस्तारित अवस्था मशीन के रूप में मॉडल करता है, जहां:

  • अवस्थाएं मोड और चर असाइनमेंट से बनी होती हैं
  • संक्रमण गार्ड शर्तों और अपडेट संबंधों से जुड़े होते हैं
  • अपडेट संबंध प्रक्रिया कॉल अनुक्रमों में विशेषज्ञता प्राप्त करते हैं

2. मध्यवर्ती अनुबंध भाषा L*

मुख्य नवाचार विभिन्न भाषाओं के बीच "गोंद" के रूप में मध्यवर्ती भाषा L* का परिचय है:

  • अनुबंध L* में लिखे जाते हैं
  • शब्दार्थ-संरक्षण संकलन compL के माध्यम से ठोस भाषाओं में रूपांतरित होते हैं
  • पूर्ण भाषा अनुवाद की जटिलता से बचा जाता है

3. CEGIS-CEGAR हाइब्रिड विधि

एल्गोरिदम कोर दो-स्तरीय पुनरावृत्ति चक्र है:

बाहरी CEGAR चक्र:

  1. वर्तमान अनुबंध का उपयोग करके अमूर्त मॉडल M' का निर्माण करें
  2. मॉडल चेकर M' ⊨ φ को सत्यापित करता है
  3. यदि विफल हो, तो जांचें कि क्या प्रतिउदाहरण झूठा है
  4. यदि झूठा है, तो अनुबंध को परिशोधित करें; अन्यथा वास्तविक प्रतिउदाहरण की रिपोर्ट करें

आंतरिक CEGIS चक्र:

  1. संश्लेषण ओरेकल उम्मीदवार अनुबंध उत्पन्न करता है
  2. सत्यापन ओरेकल अनुबंध की वैधता जांचता है
  3. यदि अमान्य है, तो सकारात्मक उदाहरण जोड़ें और पुनः संश्लेषण करें

तकनीकी नवाचार बिंदु

1. संयोजन सत्यापन रणनीति

एकीकृत अनुवाद के विपरीत, PolyVer "विभाजित और जीतो" रणनीति अपनाता है:

  • अनुबंध अमूर्तता का उपयोग करके व्यक्तिगत प्रक्रियाओं को अमूर्त करें
  • भाषा-विशिष्ट सत्यापक अनुबंध की वैधता को सत्यापित करते हैं
  • मॉडल चेकर प्रणाली-स्तरीय गुणों को सत्यापित करता है

2. स्वचालित अनुबंध पीढ़ी

कई संश्लेषण ओरेकल का समर्थन करता है:

  • LLM-आधारित संश्लेषक: विचार श्रृंखला संकेत और Python DSL का उपयोग करता है
  • SyGuS/SyMO संश्लेषक: समस्या को उदाहरण प्रोग्रामिंग समस्या के रूप में एन्कोड करता है

3. झूठापन जांच

{V = d} C {V' ≠ d'} को सत्यापित करके प्रतिउदाहरण ट्रेस की पहुंच योग्यता की जांच करता है, वास्तविक प्रतिउदाहरण और झूठे प्रतिउदाहरण के बीच अंतर करता है।

प्रयोगात्मक सेटअप

डेटासेट

  1. LFVerifier बेंचमार्क: 22 Lingua Franca प्रोग्राम, प्रतिबंधित C वाक्य-विन्यास के साथ
  2. पूर्ण LF उदाहरण: LED नियंत्रक, पर्वतारोहण रोबोट, उपग्रह मुद्रा नियंत्रक आदि एम्बेडेड प्रणालियां
  3. बहुभाषी प्रणालियां: C/Rust मिश्रित LF प्रोग्राम, ROS2 अनुप्रयोग, FFI कॉल प्रोग्राम

मूल्यांकन मेट्रिक्स

  • संश्लेषण पुनरावृत्ति संख्या (IS: CEGIS पुनरावृत्ति, AR: CEGAR पुनरावृत्ति)
  • चलने का समय (SOT: संश्लेषण ओरेकल समय, VOT: सत्यापन ओरेकल समय, UT: UCLID5 समय)
  • सत्यापन सफलता दर

तुलना विधि

LFVerifier15 के साथ तुलना, जो LF प्रोग्राम सत्यापन के लिए एकमात्र ज्ञात अंत-से-अंत स्वचालित उपकरण है।

कार्यान्वयन विवरण

  • OpenAI o1-mini को LLM संश्लेषक के रूप में उपयोग करता है, प्रति प्रक्रिया 3 समानांतर क्वेरी
  • CBMC-6.3.1, Kani-0.56.0, z3-4.8.7 सत्यापन बैकएंड के रूप में
  • 3.7GHz Intel Core i9 मशीन, 62GB RAM

प्रयोगात्मक परिणाम

मुख्य परिणाम

RQ1: मौजूदा LF सत्यापन कार्य के साथ तुलना

22 बेंचमार्क में:

  • PolyVer सभी बेंचमार्क को सफलतापूर्वक सत्यापित करता है, LFVerifier TrafficLight उदाहरण को सत्यापित नहीं कर सकता
  • 18 बेंचमार्क एकल CEGIS चक्र में सही अनुबंध संश्लेषित करते हैं, औसत 37 सेकंड
  • हालांकि कुल चलने का समय धीमा है (मुख्य रूप से अनुबंध संश्लेषण समय द्वारा प्रभावित), लेकिन महत्वपूर्ण गुणात्मक सुधार प्रदान करता है

RQ2: पूर्ण LF उदाहरणों को संभालना

पूर्ण C कोड वाली एम्बेडेड प्रणालियों को सफलतापूर्वक सत्यापित किया गया:

  • LED नियंत्रक: 1 प्रक्रिया, 123 पंक्तियां C कोड, 31.0 सेकंड संश्लेषण समय
  • पर्वतारोहण रोबोट: 12 प्रक्रियाएं, 75 पंक्तियां C/Rust कोड, 685.4 सेकंड संश्लेषण समय
  • उपग्रह नियंत्रक: 6 प्रक्रियाएं, 424 पंक्तियां C कोड, 729.0 सेकंड संश्लेषण समय

RQ3: बहुभाषी प्रणाली सत्यापन

वास्तविक बहुभाषी प्रणालियों को सत्यापित किया गया:

  • C/Rust मिश्रित LF प्रोग्राम
  • ROS2 सेवा अनुप्रयोग
  • FFI क्रॉस-भाषा कॉल प्रोग्राम

महत्वपूर्ण निष्कर्ष

  1. LLM प्रतीकात्मक विधि से बेहतर है: SyGuS/SyMO सॉल्वर को बड़ी संख्या में CEGAR पुनरावृत्तियों की आवश्यकता होती है और अक्सर समाप्त नहीं हो सकते
  2. अनुबंध संश्लेषण की चुनौतियां: जटिल नियंत्रण प्रवाह और डेटा निर्भरता वाली प्रक्रियाओं को अधिक पुनरावृत्तियों की आवश्यकता होती है
  3. व्यावहारिकता सत्यापन: खिलौना उदाहरणों के बजाय वास्तविक कार्यान्वयन कोड को संभाल सकता है

संबंधित कार्य

बहुभाषी प्रणाली सत्यापन

  • मैनुअल अनुवाद विधि: Cook आदि ने Xen हाइपरविजर को सत्यापित करने के लिए असेंबली कोड को C में अनुवाद किया
  • खंड स्वचालित अनुवाद: LFVerifier स्वचालित रूप से C खंडों को सत्यापन भाषा में अनुवाद करता है
  • ब्लैक-बॉक्स विधि: इनपुट-आउटपुट व्यवहार से सारांश का अनुमान लगाता है

संयोजन सत्यापन

  • Hoare तर्क पर आधारित संयोजन सत्यापन बड़े पैमाने पर एकल-भाषा प्रोग्राम पर व्यापक रूप से लागू होता है
  • अमूर्त व्याख्या और CEGAR का उपयोग करके स्वचालित पूर्व/पश्च शर्त सीखना

अनुबंध अनुमान

  • गुण-निर्देशित अनुबंध अनुमान विधि
  • बाधा Horn खंड सॉल्वर
  • विनिर्देश सीखने में हाल के LLM अनुप्रयोग

निष्कर्ष और चर्चा

मुख्य निष्कर्ष

  1. PolyVer बहुभाषी प्रणाली सत्यापन की मुख्य चुनौतियों को सफलतापूर्वक हल करता है
  2. संयोजन विधि पूर्ण भाषा अनुवाद की जटिलता से बचाती है
  3. स्वचालित अनुबंध संश्लेषण विधि को व्यावहारिक बनाता है
  4. LLM-आधारित संश्लेषक पारंपरिक प्रतीकात्मक विधि से बेहतर प्रदर्शन करते हैं

सीमाएं

  1. समाप्ति: एल्गोरिदम समाप्ति की गारंटी नहीं देता है, संश्लेषण ओरेकल की गुणवत्ता पर निर्भर करता है
  2. भाषा समर्थन: वर्तमान में केवल C और Rust का समर्थन करता है, अन्य भाषाओं के लिए सत्यापन ओरेकल विकसित करने की आवश्यकता है
  3. अनुबंध अभिव्यक्ति: मध्यवर्ती भाषा L* की अभिव्यक्ति क्षमता सत्यापित किए जा सकने वाले गुणों की जटिलता को सीमित करती है
  4. स्केलेबिलिटी: बड़ी प्रणालियों के लिए अनुबंध संश्लेषण समय एक बाधा बन सकता है

भविष्य की दिशाएं

  1. अन्य बहुभाषी वितरित सॉफ्टवेयर प्रणालियों और रोबोटिक सॉफ्टवेयर प्रणालियों तक विस्तार करना
  2. कोड अनुवाद के औपचारिक सत्यापन पर लागू करना (जैसे C से Rust अनुवाद)
  3. अनुबंध संश्लेषण की दक्षता और सटीकता में सुधार करना
  4. अधिक जटिल अस्थायी तर्क गुणों का समर्थन करना

गहन मूल्यांकन

शक्तियां

  1. समस्या महत्व: बहुभाषी प्रणाली सत्यापन एक व्यावहारिक और महत्वपूर्ण समस्या है
  2. विधि नवाचार: संयोजन सत्यापन + स्वचालित अनुबंध संश्लेषण का संयोजन नया है
  3. सैद्धांतिक आधार: औपचारिक परिभाषा स्पष्ट है, सही होने की गारंटी स्पष्ट है
  4. व्यावहारिक मूल्य: खिलौना उदाहरणों के बजाय वास्तविक प्रणालियों को संभाल सकता है
  5. उपकरण कार्यान्वयन: उपयोगी उपकरण कार्यान्वयन प्रदान करता है

कमियां

  1. प्रदर्शन ओवरहेड: अनुबंध संश्लेषण समय लंबा है, व्यावहारिक अनुप्रयोग को सीमित कर सकता है
  2. भाषा कवरेज: वर्तमान में केवल C और Rust का समर्थन करता है, विस्तार योग्यता सत्यापित होनी बाकी है
  3. बेंचमार्क सीमित: हालांकि वास्तविक उदाहरण शामिल हैं, लेकिन आकार अपेक्षाकृत छोटा है
  4. LLM निर्भरता: वाणिज्यिक LLM सेवा पर निर्भर है, पुनरुत्पादनशीलता को प्रभावित कर सकता है

प्रभाव

  1. शैक्षणिक योगदान: बहुभाषी प्रणाली सत्यापन के लिए नई अनुसंधान दिशा खोलता है
  2. व्यावहारिक मूल्य: सुरक्षा-महत्वपूर्ण बहुभाषी प्रणालियों के लिए सत्यापन उपकरण प्रदान करता है
  3. तकनीकी प्रेरणा: भाषा-इंटरफेस के रूप में अनुबंध का विचार सार्वभौमिक मूल्य रखता है

लागू परिदृश्य

  1. एम्बेडेड प्रणालियां: C/Rust मिश्रित वास्तविक समय प्रणालियां
  2. वितरित प्रणालियां: ROS2, gRPC आदि बहुभाषी ढांचे
  3. सुरक्षा-महत्वपूर्ण अनुप्रयोग: औपचारिक सत्यापन गारंटी की आवश्यकता वाली प्रणालियां
  4. विरासत प्रणाली एकीकरण: नए और पुराने कोड मिश्रित प्रणालियां

संदर्भ

पेपर 50 संबंधित संदर्भों का हवाला देता है, जो बहुभाषी प्रणालियों, औपचारिक सत्यापन, अनुबंध अनुमान, वाक्य-विन्यास-निर्देशित संश्लेषण आदि कई क्षेत्रों के महत्वपूर्ण कार्यों को कवर करते हैं, जो अनुसंधान के लिए एक मजबूत सैद्धांतिक आधार प्रदान करते हैं।

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