Rebeca (аббревиатура от Reactive Objects Language) — это язык моделирования на основе актеров с формальной основой, разработанный с целью преодолеть разрыв между формальными подходами к проверке и реальными приложениями. Ее можно рассматривать как эталонную модель для параллельных вычислений , основанную на оперативной интерпретации модели актера. Это также платформа для практической разработки объектно-ориентированных параллельных систем.
Помимо наличия подходящего и эффективного способа моделирования параллельных и распределенных систем, необходим формальный подход к проверке, чтобы гарантировать их корректность. Rebeca поддерживается набором инструментов проверки. Более ранние инструменты предоставляли интерфейс для работы с кодом Rebeca и для перевода кода Rebeca на языки ввода известных и зрелых средств проверки моделей (таких как SPIN и NuSMV) и, таким образом, могли проверять их свойства. Rebeca с 2005 года поддерживается средством прямой проверки моделей на основе Modere (механизм проверки моделей Rebeca). Модульные методы верификации и абстракции используются для уменьшения пространства состояний и позволяют проверять сложные реактивные системы. Помимо этих методов, Modere поддерживает частичное понижение порядка и уменьшение симметрии.