Rebeca (lenguaje de programación)

Rebeca (acrónimo de Reactive Objects Language) es un lenguaje de modelado basado en actores con una base formal, diseñado para tender un puente entre los enfoques de verificación formal y las aplicaciones reales. Puede considerarse un modelo de referencia para la computación concurrente , basado en una interpretación operacional del modelo de actores. Además, constituye una plataforma para el desarrollo práctico de sistemas concurrentes basados ​​en objetos.

Además de contar con un método adecuado y eficiente para modelar sistemas concurrentes y distribuidos, se requiere un enfoque de verificación formal para garantizar su corrección. Rebeca cuenta con el respaldo de un conjunto de herramientas de verificación. Las herramientas anteriores proporcionaban una interfaz para trabajar con el código de Rebeca y traducirlo a lenguajes de entrada de verificadores de modelos conocidos y consolidados (como SPIN y NuSMV), lo que permitía verificar sus propiedades. Desde 2005, Rebeca cuenta con el respaldo de un verificador de modelos directo basado en Modere (el motor de verificación de modelos de Rebeca). Se utilizan técnicas de verificación modular y abstracción para reducir el espacio de estados y permitir la verificación de sistemas reactivos complejos. Además de estas técnicas, Modere admite la reducción de orden parcial y la reducción de simetría.

• Métodos formales
• Verificación de modelos
• Verificador de modelos SPIN

• M. Sirjani. Especificación formal y verificación de sistemas concurrentes y reactivos, tesis doctoral , Departamento de Ingeniería Informática, Universidad Tecnológica Sharif, diciembre de 2004.
• M. Sirjani, A. Movaghar. Un modelo basado en objetos para agentes, en Actas del Taller sobre Agentes para la Gestión de la Información, Sociedad Austriaca de Informática, octubre de 2002.

• Página principal de Rebeca
• Laboratorio de Métodos Formales, Universidad de Teherán