Ребека (язык программирования)

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

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

См. также

• Формальные методы
• Проверка модели
• Проверка модели SPIN

Ссылки

• М. Сирджани. Формальная спецификация и верификация параллельных и реактивных систем, докторская диссертация , факультет компьютерной инженерии, Технологический университет Шарифа, декабрь 2004 г.
• М. Сирджани, А. Мовагар. Объектно-ориентированная модель для агентов, в материалах семинара по агентам для управления информацией, Австрийское компьютерное общество, октябрь 2002 г.

Внешние ссылки

• Домашняя страница Ребеки
• Лаборатория формальных методов Тегеранского университета