Rodin tool
रॉडिन टूल इवेंट-बी में औपचारिक मॉडलिंग के लिए एक सॉफ्टवेयर टूल है। इसे कई सहयोगी यूरोपीय संघ परियोजनाओं के हिस्से के रूप में विकसित किया गया था, जिसमें शुरू में आरओडीआईएन परियोजना (2004-2007) शामिल थी। अवलोकन घटना-बी बी-विधि से विकसित एक संकेतन और विधि है और इसका उपयोग मॉडलिंग की एक वृद्धिशील शैली के साथ किया जाना है। वृद्धिशील मॉडलिंग का विचार प्रोग्रामिंग से लिया गया हैः आधुनिक प्रोग्रामिंग भाषाएं एकीकृत विकास वातावरण के साथ आती हैं जो कार्यक्रमों को संशोधित करने और सुधारने में आसान बनाती हैं। रॉडिन उपकरण इवेंट-बी के लिए ऐसा वातावरण प्रदान करता है। रॉडिन उपकरण की दो विशेषताएँ इसके उपयोग में आसानी और इसकी विस्तार क्षमता हैं। यह उपकरण मॉडलिंग पर केंद्रित है। यह उपयोगकर्ता को मॉडल को संशोधित करने और मॉडल की विविधताओं को आजमाने की अनुमति देता है। उपकरण भी विस्तार योग्य है। इससे उपकरण को विशिष्ट आवश्यकताओं के अनुकूल बनाना संभव हो जाता है, इसलिए उपकरण को विपरीत की मांग करने के बजाय मौजूदा विकास प्रक्रियाओं में फिट होने के लिए अनुकूलित किया जा सकता है। एक संबद्ध इवेंट-बी विकी है। रॉडिन ("जटिल प्रणालियों के लिए कठोर मुक्त विकास वातावरण") एक्लिप्स आईडीई (जावा-आधारित) का एक विस्तार है। रॉडिन एक्लिप्स बिल्डर निम्नलिखित का प्रबंधन करता हैः अच्छी तरह से गठित और प्रकार परीक्षक प्रूफ ऑब्लिगेशन (पी. ओ.) जनरेटर प्रूफ मैनेजर (पी. एम.) परिवर्तनों का प्रसार रॉडिन प्रूफ मैनेजर (पी. एम.) पी. एम. प्रत्येक पी. ओ. स्वचालित और संवादात्मक तरीकों के लिए एक प्रूफ ट्री का निर्माण करता है पी. एम. उपयोग की गई परिकल्पनाओं का प्रबंधन करता है पी. एम. तर्ककर्ताओं को बुलाता हैः निर्वहन लक्ष्य, या लक्ष्य को उप-लक्ष्यों में विभाजित करता है तर्ककर्ताओं का संग्रहः सरलीकरण, नियम-आधारित, निर्णय प्रक्रियाएं, पी. एम. को परिभाषित करने के लिए बुनियादी रणनीति भाषा और तर्ककर्ता औद्योगिक अनुप्रयोग और केस स्टडी रॉडिन परियोजना में पांच औद्योगिक केस अध्ययन शामिल थे जो टूलसेट को मान्य करने में काम करते थे और उपकरणों का उपयोग करने के लिए एक उपयुक्त पद्धति के विस्तार में मदद करते थे। केस स्टडीज का नेतृत्व रॉडिन परियोजना के औद्योगिक भागीदारों द्वारा किया गया था, जिसे अन्य भागीदारों द्वारा समर्थित किया गया था। केस स्टडी इस प्रकार थीः एक इंजन नियंत्रक के लिए एक विफलता प्रबंधन प्रणाली; मोबाइल इंटरनेट प्रौद्योगिकी के लिए एक मंच का हिस्सा; संचार प्रोटोकॉल की इंजीनियरिंग; एक वायु-यातायात प्रदर्शन प्रणाली; एक परिवेशी परिसर अनुप्रयोग। रॉडिन बी4 फ्री प्रोवर्स प्रोवाइडर के लिए कुछ उपलब्ध प्लग-इनः क्लियरसी फंक्शनः प्रमेय प्रोवर्स यूएमएल-बी प्रोवाइडरः यूनिवर्सिटी ऑफ साउथेम्प्टन फंक्शनः इवेंट-बी के लिए यूएमएल जैसे ग्राफिकल फ्रंट-एंड जो क्लास डायग्राम और स्टेट चार्ट का समर्थन करता है प्रोबी प्रोवाइडरः यूनिवर्सिटी ऑफ डसेलडोर्फ फंक्शनः इवेंट-बी मॉडल का एनिमेशन और मॉडल-चेकिंग; गलत प्रूफ लक्ष्यों के लिए काउंटर-उदाहरण, विशेष रूप से, प्रूफ दायित्व ब्रामा प्रोवाइडरः क्लियरसी फंक्शनः बी मॉडल का एनिमेशन। उद्देश्य दो गुना हैः अवस्थाओं का निरीक्षण करने के लिए एक मॉडल के साथ प्रयोग और इवेंट-बी मॉडल के परिवर्तन फ्लैश एनीमेशन मॉड्यूलराइजेशन प्रदाताः न्यूकैसल विश्वविद्यालय कार्यः मॉडलिंग की तार्किक इकाइयों में इवेंट-बी विकास की संरचना, जिसे मॉड्यूल कहा जाता है; मॉडल रचना; मॉडल का पुनः उपयोग संदर्भ आगे पढ़ने के लिए जीन-रेमंड एब्रियल। बी-बुकः कार्यक्रमों को अर्थों के लिए निर्दिष्ट करना। कैम्ब्रिज यूनिवर्सिटी प्रेस, 1996 ()। जीन-रेमंड एब्रियल, माइकल बटलर, स्टीफन हॉलरस्टेड और लॉरेंट वोइसिन। इवेंट-बी के लिए एक खुला विस्तार योग्य उपकरण वातावरण। जेड. लियू और जे. वह, संपादक, आईसीएफईएम 2006, एलएनसीएस, खंड 4260, पृष्ठ 588-605। स्प्रिंगर, 2006। अब्दोलबागी रेज़ाज़ादेह, नील इवांस और माइकल बटलर। इवेंट-बी और रॉडिन का उपयोग करके एक औद्योगिक, केस स्टडी का पुनर्विकास। बी. सी. एस-एफ. ए. सी. एस. क्रिसमस 2007 बैठक, 2007 में। रॉडिन। डिलीवरेबल डी18: केस स्टडी विकास पर मध्यवर्ती रिपोर्ट। माइकल बटलर और स्टीफन हॉलरस्टेड, द रॉडिन फॉर्मल मॉडलिंग टूल, ईयू रिसर्च प्रोजेक्ट आईएसटी 511599 रॉडिन। एक्लिप्स प्लेटफॉर्म होमपेज। बाहरी लिंक इवेंट-बी और रॉडिन प्लेटफॉर्म इवेंट-बी और रॉडिन प्रलेखन विकी रॉडिन सोर्सफोर्ज 2007 सॉफ्टवेयर पर औपचारिक विधियों के उपकरण औपचारिक विनिर्देशन भाषाएँ