เครื่องมือRodinเป็นเครื่องมือซอฟต์แวร์สำหรับการสร้างแบบจำลองอย่างเป็นทางการในEvent-B [ ^{1 ] [ 2 ] ได้}รับการพัฒนาขึ้นเป็นส่วนหนึ่งของโครงการความร่วมมือของสหภาพยุโรป หลาย โครงการ รวมถึงโครงการ RODIN ในช่วงเริ่มต้น (2004–2007) ^{[ 3 ]}

Event-B เป็นสัญกรณ์และวิธีการที่พัฒนามาจากB-Methodและมีจุดประสงค์เพื่อใช้กับรูปแบบการสร้างแบบจำลอง แบบเพิ่มขึ้น แนวคิดของการสร้างแบบจำลองแบบเพิ่มขึ้นนั้นมาจากการเขียนโปรแกรม: ภาษาโปรแกรมสมัยใหม่มาพร้อมกับสภาพแวดล้อมการพัฒนาแบบบูรณาการที่ทำให้ง่ายต่อการแก้ไขและปรับปรุงโปรแกรม เครื่องมือ Rodin ให้สภาพแวดล้อมดังกล่าวสำหรับ Event-B คุณลักษณะสองประการของเครื่องมือ Rodin คือใช้งานง่ายและขยายได้^{[ 2 ]}

เครื่องมือนี้เน้นการสร้างแบบจำลอง ช่วยให้ผู้ใช้สามารถแก้ไขแบบจำลองและทดลองใช้รูปแบบต่างๆ ของแบบจำลองได้ นอกจากนี้ เครื่องมือนี้ยังสามารถขยายได้ ทำให้สามารถปรับเครื่องมือให้เข้ากับความต้องการเฉพาะได้ ดังนั้น เครื่องมือจึงสามารถปรับให้เข้ากับกระบวนการพัฒนาที่มีอยู่ได้ แทนที่จะต้องเปลี่ยนแปลงไปในทางตรงกันข้าม มีวิกิ Event-B ที่เกี่ยวข้อง^{[ 4 ]}

Rodin ("สภาพแวดล้อมการพัฒนาแบบเปิดที่เข้มงวดสำหรับระบบที่ซับซ้อน") เป็นส่วนขยายของEclipse IDE ( ที่ใช้ Java ) Rodin Eclipse Builder จัดการสิ่งต่อไปนี้: ^{[ 5 ]}

• ตัวตรวจสอบ รูปแบบและประเภท
• เครื่องสร้างหลักฐานภาระผูกพัน (PO)
• ผู้จัดการหลักฐาน (PM)
• การแพร่กระจายของการเปลี่ยนแปลง

Rodin Proof Manager (PM)

• PM สร้างแผนผังพิสูจน์สำหรับ PO แต่ละรายการ
• โหมดอัตโนมัติและโหมดโต้ตอบ
• PM บริหารจัดการสมมติฐานที่ใช้
• นายกรัฐมนตรีเรียกร้องให้ผู้ที่มีเหตุผลพิจารณาเรื่องต่อไปนี้:
  • เป้าหมายการจำหน่าย หรือ
  • แบ่งเป้าหมายออกเป็นเป้าหมายย่อย
• กลุ่มของตัวให้เหตุผล:
  • ตัวทำให้ง่ายขึ้น, ขั้นตอนการตัดสินใจตามกฎเกณฑ์
• ภาษาเชิงกลยุทธ์พื้นฐานเพื่อกำหนด PM และเหตุผล

โครงการ Rodin ประกอบด้วยกรณีศึกษาเชิงอุตสาหกรรม 5 กรณี ซึ่งทำหน้าที่ตรวจสอบความถูกต้องของชุดเครื่องมือและช่วยในการกำหนดวิธีการที่เหมาะสมสำหรับการใช้เครื่องมือ^{[ 6 ]}กรณีศึกษาเหล่านี้ดำเนินการโดยพันธมิตรทางอุตสาหกรรมของโครงการ Rodin โดยได้รับการสนับสนุนจากพันธมิตรอื่นๆ กรณีศึกษามีดังต่อไปนี้:

• ระบบจัดการความผิดพลาดสำหรับตัวควบคุมเครื่องยนต์;
• เป็นส่วนหนึ่งของแพลตฟอร์มเทคโนโลยีอินเทอร์เน็ตบนมือถือ;
• การออกแบบทางวิศวกรรมของโปรโตคอลการสื่อสาร;
• ระบบแสดงผลการจราจรทางอากาศ;
• แอปพลิเคชันสำหรับใช้งานในวิทยาเขต

• ผู้พิสูจน์ B4free ^{[ 7 ]}
  • ผู้ให้บริการ: ClearSy
  • ฟังก์ชัน: โปรแกรมพิสูจน์ทฤษฎีบท
• UML-B ^{[ 8 ]}
  • ผู้ให้บริการ: มหาวิทยาลัยเซาแธมป์ตัน
  • ฟังก์ชัน: ส่วนติดต่อผู้ใช้แบบกราฟิกคล้าย UML สำหรับ Event-B ที่รองรับไดอะแกรมคลาสและแผนภูมิสถานะ
• ProB ^{[ 9 ] [ 10 ]}
  • ผู้จัดหา: มหาวิทยาลัยดุสเซลดอร์ฟ
  • หน้าที่: การสร้างภาพเคลื่อนไหวและการตรวจสอบแบบจำลองของแบบจำลอง Event-B; ตัวอย่างค้านสำหรับเป้าหมายการพิสูจน์ที่ผิดพลาด โดยเฉพาะอย่างยิ่ง ข้อผูกพันในการพิสูจน์
• บรามา^{[ 11 ]}
  • ผู้ให้บริการ: ClearSy
  • ฟังก์ชัน: การสร้างภาพเคลื่อนไหวของโมเดล B วัตถุประสงค์มีสองประการ:
    • การทดลองกับแบบจำลองเพื่อสังเกตสถานะและการเปลี่ยนแปลง
    • ภาพเคลื่อนไหวแฟลชของโมเดล Event-B
• การแบ่งส่วนย่อย^{[ 12 ]}
  • ผู้จัดหา: มหาวิทยาลัยนิวคาสเซิล
  • หน้าที่: จัดโครงสร้างการพัฒนา Event-B ให้เป็นหน่วยเชิงตรรกะของการสร้างแบบจำลอง เรียกว่า โมดูล; การประกอบแบบจำลอง; การนำแบบจำลองกลับมาใช้ใหม่

• ฌอง-เรย์มอนด์ อับเรียล . หนังสือ บี: การกำหนดโปรแกรมให้กับความหมาย . สำนักพิมพ์มหาวิทยาลัยเคมบริดจ์ , 1996, ( ISBN) 0-521-49619-5)
• Jean-Raymond Abrial , Michael Butler , Stefan Hallerstede และ Laurent Voisin. สภาพแวดล้อมเครื่องมือแบบเปิดที่ขยายได้สำหรับ Event-B ในZ. LiuและJ. Heบรรณาธิการ, ICFEM 2006 , LNCS, เล่มที่ 4260, หน้า 588–605. Springer, 2006.
• Abdolbaghi ​​Rezazadeh, Neil Evans และ Michael Butler. การพัฒนาพื้นที่อุตสาหกรรมใหม่ กรณีศึกษาโดยใช้ Event-B และ Rodin ใน การประชุม BCS-FACS Christmas 2007 , 2007
• RODIN. ผลลัพธ์ D18: รายงานความคืบหน้าเบื้องต้นเกี่ยวกับกรณีศึกษา
• Michael Butler และ Stefan Hallerstede, เครื่องมือสร้างแบบจำลองเชิงรูปธรรมของ Rodin , โครงการวิจัยของสหภาพยุโรป IST 511599 RODIN
• หน้าแรกของแพลตฟอร์มEclipse

• กิจกรรม B และแท่นโรดิน
• วิกิเอกสารประกอบ Event-B และ Rodin
• RodinบนSourceForge