物流システムに対するAmbient Logicモデル検査システム
スポンサーリンク
概要
- 論文の詳細を見る
本稿では物流システムの満たすべき性質の形式的な記述体系とそのモデル検査について述べる.物流の世界では,貨物の流通量の増加に伴いコンテナ管理の重要性が高まっている.我々は Ambient Calculus による物流システムの記述と,実際の物流がその記述どおりに行われているかを監視するシステムを開発した.この監視システムによる物流管理の正しさを確認するためには,書類から生成されたプロセス式そのものの正当性を確認する必要がある.しかし,プロセス式生成システムで生成されるプロセス式は一般に複雑なものになり,さらに非決定的な動作も多くこの確認作業を人手で行うのは困難であると考えられる.本稿では,この課題を解決するために,物流システムに要求される,"いつか必ず貨物は目的地に輸送される"というような性質を Ambient Logic の論理式で表現し,その性質をプロセス式がすべて満たしていることを形式的に検査する手法を提案する.遷移グラフの各経路が論理式を満たしていることを調べることで検査を行う.提案手法に基づくモデル検査システムを構築し検証実験を行った結果についても述べる.
- 一般社団法人情報処理学会の論文
- 2009-09-03
著者
-
樋口 昌宏
近畿大学理工学部
-
樋口 昌宏
近畿大学大学院総合理工学研究科
-
加藤 暢
近畿大学理工学部
-
樋口 昌宏
近畿大学理工学部情報学科
-
植田 直人
株式会社JSOL
-
加藤 暢
近畿大学理工学部情報学科
関連論文
- 分散オブジェクト技術によるプログラムのπ計算への変換
- D-1-12 時間オートマトンからタイマ付き有限状態機械への変換における状態数簡単化について(D-1. コンピュテーション,一般セッション)
- M-014 タイマを用いる分散システムにおける時間因果順序違反を保存した障害復旧方法(M分野:ユビキタス・モバイルコンピューティング)
- 研究室配属プログラムの開発と運用
- RA-005 Ambient Calculusによる物流システム記述に対するモデル検査(モデル・アルゴリズム・プログラミング,査読付き論文)
- 時間オートマトンによるフェースディスプレイの上位設計と形式的検証
- 時間オートマトンによるフェースディスプレイの上位設計と形式的検証
- Ambient計算に基づく動的な海上物流の監視システム
- 階層的キーワードベースの名前管理におけるキーワード管理手法
- 非階層型名前空間のファイルシステムへの適用に関する実験的評価
- 分散計算における制御フローに基づいたイベントアブストラクション手法(マルチメディアネットワークシステム)
- 階層的キーワードに基づく名前管理手法とそれに基づくファイル共有手法
- 階層的キーワードに基づく名前管理手法とそれに基づくファイル共有手法
- 分散環境における透過的なプログラム記述法とD'Agentを用いた実行環境
- 分散環境における透過的なプログラム記述法とD'Agentを用いた実行環境
- 分散データベースにおける通信量を考慮した動的データ配置法
- 逐次化グラフを用いた複合トランザクションの並行制御
- 待ち時間を考慮したΔ因果順序配送アルゴリズムの提案
- 待ち時間を考慮したΔ因果順序配送アルゴリズムの提案
- 配送時間を考慮した因果関係を保存するメッセージ配送
- 部分トランザクションの独立性を考慮した入れ子トランザクションモデル
- 多重化データベースにおけるsite equorumを用いたデータの一貫性制御
- 多重化データベースにおけるsite quorumを用いたデータの一貫性制御
- 多重化データベースにおける仮想分割と再生成を用いた一貫性制御
- 書き込み保留を用いた逐次化グラフスケジューリング
- 分散システムにおける因果関係を保存するメッセージ 配送プロトコル
- 分散型データベースにおける逐次化グラフ検査を用いたスケジューラの実現と評価
- 分散型データベースにおける逐次化グラフを用いたスケジューリングアルゴリズム
- 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周年記念)
- タイマを用いる有限状態機械でモデル化されたシステムの検証手続き
- 観測不可能な非決定動作を含む並行DFSM群としてモデル化される通信プロトコルの適合性試験法(マルチメディアコミュニケーションシステム)
- タイマシステムコールを用いるDFSMプロトコルに対する試験系列生成手法(マルチメディアコミュニケーションシステム)
- タイマを用いる有限状態機械でモデル化されたシステムの検証手続き
- タイマシステムコールを用いるFSMプロトコルの適合性試験について
- タイマシステムコールを用いるFSMプロトコルの適合性試験について
- 拡張有限状態機械モデルで書かれた通信プロトコルの適合性試験系列の自動生成の一手法
- 拡張有限状態機械モデルにおける通信プロトコルのテスト系列の自動生成の一手法
- Ambient CalculusのJavaによる処理系の実装
- 物流システム記述のための多重Ambient Calculus (プログラミング Vol.5 No.2)
- 多重Ambient Calculusによる物流記述に対する弱双模倣等価性を用いたモデル検査 (プログラミング Vol.5 No.3)
- 時間付きAmbient Calculus