物流システムに対するAmbient Logicモデル検査システム

• Item type: Trans(1)
• 公開日: 2009-07-10
• タイトル: 物流システムに対するAmbient Logicモデル検査システム
• タイトル / 言語: en
• タイトル: An Ambient Logic Model Checking System for Freight Systems
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 発表概要
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 近畿大学大学院総合理工学研究科
• 著者所属: 近畿大学理工学部情報学科
• 著者所属: 近畿大学大学院総合理工学研究科
• 著者所属(英): en
• 著者所属(英): Interdisciplinary Graduate School of Science and Engineering, Kinki University
• 著者所属(英): en
• 著者所属(英): School of Science and Engineering, Department of Informatics, Kinki University
• 著者所属(英): en
• 著者所属(英): Interdisciplinary Graduate School of Science and Engineering, Kinki University
• 著者名: 植田, 直人; 加藤, 暢; 樋口, 昌宏
• 著者名(英): Naoto, Ueda; Toru, Kato; Masahiro, Higuchi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本発表では物流システムの満たすべき性質の形式的な記述体系とそのモデル検査について述べる．物流の世界では，貨物の流通量の増加にともないコンテナ管理の重要性が高まっている．我々は Ambient Calculus による物流システムの記述と，実際の物流がその記述どおりに行われているかを検査するシステムを開発した．この検査システムによる物流管理の正しさを確認するためには，書類から生成されたプロセス式そのものの正当性を確認する必要がある．しかし，プロセス式生成システムで生成されるプロセス式は一般に複雑なものになり，さらに非決定的な動作も多くこの確認作業を人手で行うのは困難であると考えられる．本発表では，この課題を解決するために，物流システムに要求される，“いつか必ず貨物は目的地に輸送される” というような性質を Ambient Logic の論理式で表現し，その性質をプロセス式がすべて満たしていることを形式的に検査する手法を提案する．遷移グラフの各経路が論理式を満たしていることを調べることで検査を行う．提案手法に基づくモデル検査システムの構築し検証実験を行った結果についても述べる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: We present a variant of Ambient Logic to describe desired properties of freight systems and a model checking algorithm for the logic. In the field of freight distribution, the cargo handling fault problem becomes serious while the amount of circulation of the freights increases. We study a freight inspection system based on Ambient Calculus and we have already built a prototype system. The system can derive process formulas from several freight documents. The System also checks that the actual freight movement conforms the derived formula. To show the correctness of freights transportation, we have to ensure the validity of process formula. We provide an Ambient Logic to present desired properties of freight systems, such as "every cargo will be eventually transported to its destination". We also present an algorithm to show process formula satisfy Ambient Logic formula by exploring state transition graph. We conducted a verification experiment using the model checking system.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 2, 号 3, p. 59-59, 発行日 2009-07-10
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会