รีเบก้า (ภาษาโปรแกรม)

Rebeca (ชื่อย่อของ Reactive Objects Language) เป็นภาษาสร้างแบบจำลองตามแอคเตอร์ที่มีพื้นฐานอย่างเป็นทางการ ออกแบบมาเพื่อเชื่อมช่องว่างระหว่าง วิธี การตรวจสอบอย่างเป็นทางการและการใช้งานจริง สามารถพิจารณาได้ว่าเป็นแบบจำลองอ้างอิงสำหรับการคำนวณพร้อมกันโดยอิงจากการตีความเชิงปฏิบัติการของแบบจำลองแอคเตอร์ นอกจากนี้ยังเป็นแพลตฟอร์มสำหรับการพัฒนาระบบพร้อมกันแบบอิงวัตถุในทางปฏิบัติอีกด้วย

นอกเหนือจากการมีวิธีการที่เหมาะสมและมีประสิทธิภาพสำหรับการสร้างแบบจำลองระบบพร้อมกันและระบบกระจายแล้ว ยังจำเป็นต้องมีแนวทางการตรวจสอบอย่างเป็นทางการเพื่อให้มั่นใจในความถูกต้องของระบบเหล่านั้น Rebeca ได้รับการสนับสนุนจากชุดเครื่องมือตรวจสอบ เครื่องมือรุ่นก่อนหน้านี้มีส่วนหน้าสำหรับทำงานกับโค้ด Rebeca และแปลโค้ด Rebeca เป็นภาษาอินพุตของตัวตรวจสอบแบบจำลองที่เป็นที่รู้จักและมีประสิทธิภาพสูง (เช่น SPIN และ NuSMV) ดังนั้นจึงสามารถตรวจสอบคุณสมบัติของระบบได้ ตั้งแต่ปี 2005 Rebeca ได้รับการสนับสนุนจากตัวตรวจสอบแบบจำลองโดยตรงที่ใช้ Modere (Model checking Engine ของ Rebeca) เทคนิคการตรวจสอบแบบโมดูลาร์และการลดทอนถูกนำมาใช้เพื่อลดพื้นที่สถานะและทำให้สามารถตรวจสอบระบบปฏิกิริยาที่ซับซ้อนได้ นอกจากเทคนิคเหล่านี้แล้ว Modere ยังรองรับการลดลำดับบางส่วนและการลดความสมมาตรด้วย

• วิธีการที่เป็นทางการ
• การตรวจสอบแบบจำลอง
• ตัวตรวจสอบโมเดล SPIN

• หน้าหลักของรีเบก้า
• ห้องปฏิบัติการวิธีการเชิงรูปธรรม มหาวิทยาลัยเตหะราน

บทความเกี่ยวกับภาษาโปรแกรมนี้ ยังเป็น เพียงบทความย่อคุณสามารถช่วยวิกิพีเดียได้โดยการเพิ่มข้อมูลที่ขาดหายไป

• วี
• ที
• อี