レベッカ（プログラミング言語）

Rebeca (Reactive Objects Language の略) は、形式的な基盤を持つアクターベースのモデリング言語であり、形式的な検証アプローチと実際のアプリケーションの間のギャップを埋めるために設計されています。アクター モデルの操作的解釈に基づく、並行計算の参照モデルとして考えることができます。また、実際にオブジェクト ベースの並行システムを開発するためのプラットフォームでもあります。

並行システムや分散システムをモデル化するための適切かつ効率的な方法に加えて、それらの正確性を保証するための形式検証アプローチが必要です。Rebeca は、一連の検証ツールによってサポートされています。以前のツールは、Rebeca コードを操作するフロントエンドを提供し、Rebeca コードを有名で成熟したモデル チェッカー (SPIN や NuSMV など) の入力言語に変換して、それらのプロパティを検証できました。2005 年以降、Rebeca は Modere (Rebeca のモデル チェック エンジン) に基づく直接モデル チェッカーによってサポートされています。モジュラー検証および抽象化技術を使用して状態空間を削減し、複雑なリアクティブ システムを検証できるようにします。これらの技術に加えて、Modere は部分順序削減と対称性削減をサポートしています。

• 形式手法
• モデルチェック
• SPIN モデルチェッカー

• M. Sirjani. 並行システムとリアクティブ システムの形式仕様と検証、博士論文、コンピュータ エンジニアリング学部、シャリフ工科大学、2004 年 12 月。
• M. Sirjani、A. Movaghar。エージェントのためのオブジェクトベース モデル、情報管理のためのエージェントに関するワークショップの議事録、オーストリア コンピュータ協会、2002 年 10 月。

• レベッカホームページ
• テヘラン大学形式手法研究所