Java分散オブジェクトからπ計算プロセスへの変換系
スポンサーリンク
概要
- 論文の詳細を見る
本発表では,Java RMIを用いた分散アプリケーションからπ計算プロセスへの変換系について述べる.この変換により,様々な実用的な分散アプリケーションをMWBやPi-ETなどのモデル検査を利用して形式的に取り扱えるようになる.Java RMIを使用したアプリケーションには,分散オブジェクトの参照を受け渡すことで参照先を動的に切り替えられるという特徴がある.π計算もまた,ポート名の送受信によりプロセス間の接続を動的に切り替える機能を持つ.我々はこの類似性に注目し,Java RMIを用いた分散アプリケーションの計算モデルとしてπ計算が適当であると考えた.構築した変換系では,Javaのメソッドやコンストラクタの呼び出しをメッセージパッシングによる操作と見なし,これらをπ計算プロセスの入出力アクションに変換する.また,この変換系は,Javaの制御構造をπ計算のMatchとMismatchの操作に変換し,繰返しやmapなどのデータ構造もプロセスの再帰的定義に変換する.この変換の有用性を示すため,チャットシステムを変換系に適用する実験を行った.作成したチャットシステムは1台のサーバと複数台のクライアントからなり,Java RMIを使用して書かれている.各クライアントはサーバに問い合わせることにより他クライアントの参照を得ることができる.
- 2008-06-26
著者
関連論文
- 分散オブジェクト技術によるプログラムのπ計算への変換
- D-1-12 時間オートマトンからタイマ付き有限状態機械への変換における状態数簡単化について(D-1. コンピュテーション,一般セッション)
- M-014 タイマを用いる分散システムにおける時間因果順序違反を保存した障害復旧方法(M分野:ユビキタス・モバイルコンピューティング)
- 研究室配属プログラムの開発と運用
- RA-005 Ambient Calculusによる物流システム記述に対するモデル検査(モデル・アルゴリズム・プログラミング,査読付き論文)
- 時間オートマトンによるフェースディスプレイの上位設計と形式的検証
- 時間オートマトンによるフェースディスプレイの上位設計と形式的検証
- Ambient計算に基づく動的な海上物流の監視システム
- A_014 時間オートマトンのタイマ付き有限状態機械への変換法(A分野:モデル・アルゴリズム・プログラミング)
- 物流システムに対するAmbient Logicモデル検査システム
- 物流システムに対する Ambient Logic モデル検査システム
- 物流システムに対するAmbient Logicモデル検査システム
- 物流システムに対するAmbient Logicモデル検査システム
- 3M-7 Ambient Calculusを用いる物流検査システムの実装(数理モデルと問題解決,学生セッション,ソフトウェア科学・工学)
- A-032 分散オブジェクトからπ計算プロセスへの変換系(A分野:モデル・アルゴリズム・プログラミング)
- Ambient Calculusを用いた物流検査システム
- A-015 動的な接続関係を持つJavaプログラムの一記述法とπ計算への変換(A分野:モデル・アルゴリズム・プログラミング)
- D-1-12 Javaオブジェクトからπ計算プロセスへの変換について(D-1. コンピュテーション, 情報・システム1)
- Java分散オブジェクトからπ計算プロセスへの変換系
- 3P-9 モバイルアドホックネットワークのための低トラヒックコーラムによるオブジェクト配布方式の評価(ソフトウェアアーキテクチャ・設計,学生セッション,ソフトウェア科学・工学,情報処理学会創立50周年記念)
- Ambient CalculusのJavaによる処理系の実装
- 物流システム記述のための多重Ambient Calculus (プログラミング Vol.5 No.2)
- 多重Ambient Calculusによる物流記述に対する弱双模倣等価性を用いたモデル検査 (プログラミング Vol.5 No.3)
- 時間付きAmbient Calculus