WEKO3
アイテム
物流システムに対するAmbient Logicモデル検査システム
https://ipsj.ixsq.nii.ac.jp/records/67625
https://ipsj.ixsq.nii.ac.jp/records/676254e097f38-a4f4-4195-916c-967f75341563
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TOM0301008.pdf (542.5 kB)
|
Copyright (c) 2010 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2010-01-26 | |||||||
| タイトル | ||||||||
| タイトル | 物流システムに対する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 | |||||||
| 著者所属 | ||||||||
| 近畿大学理工学部情報学科 | ||||||||
| 著者所属 | ||||||||
| 近畿大学理工学部情報学科 | ||||||||
| 著者所属 | ||||||||
| 株式会社JSOL | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| School of Science and Engineering Department of Informatics, Kinki University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| School of Science and Engineering Department of Informatics, Kinki University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| JSOL Corporation | ||||||||
| 著者名 |
加藤, 暢
× 加藤, 暢
|
|||||||
| 著者名(英) |
Toru, Kato
× Toru, Kato
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | 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 distribution, the increase in cargo handling errors is a serious problem as the amount of freight circulation 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 | |||||||
| 収録物識別子 | AA11464803 | |||||||
| 書誌情報 |
情報処理学会論文誌数理モデル化と応用（TOM） 巻 3, 号 1, p. 73-86, 発行日 2010-01-26 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7780 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
