文献

J-GLOBAL ID：201002284044482232   整理番号：10A0440805

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

An Ambient Logic Model Checking System for Freight Systems

著者 (3件)： 加藤暢 (近畿大 理工) ,  樋口昌宏 (近畿大 理工) ,  植田直人 (JSOL)
資料名： 情報処理学会論文誌トランザクション(CD-ROM)  (情報処理学会論文誌 Computer Vision and Applications(CD-ROM))
巻： 2009  号： 2  ページ： SURIMODERU.VOL.3,NO.1,73-86  発行年： 2010年04月15日 
JST資料番号： L7379A  ISSN： 1882-7772  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本論文では物流システムの満たすべき性質の形式的な記述体系とそのモデル検査について述べる。物流の世界では,貨物の流通量の増加にともないコンテナ管理の重要性が高まっている。我々はAmbient Calculusによる物流システムの記述と,実際の物流がその記述どおりに行われているかを監視するシステムを開発した。この監視システムによる物流管理の正しさを確認するためには,書類から生成されたプロセス式そのものの正当性を確認する必要がある。しかし,プロセス式生成システムで生成されるプロセス式は一般に複雑なものになり,さらに非決定的な動作も多くこの確認作業を人手で行うのは困難であると考えられる。本論文では,この課題を解決するために,物流システムに要求される,“いつか必ず貨物は目的地に輸送される”というような性質をAmbient Logicの論理式で表現し,その性質をプロセス式がすべて満たしていることを形式的に検査する手法を提案する。また,提案手法に基づくモデル検査システムを構築し検証実験を行った結果についても述べる。(著者抄録)

シソーラス用語： *物流システム ,  *モデル検査 ,  形式的手法【計算機】 ,  計算モデル ,  監視制御システム ,  非決定性 ,  貨物 ,  論理 ,  実証実験
準シソーラス用語： Ambient Calculus ,  Ambient Logic

分類 (2件)： 物的流通  (KA08000O) ,  計算理論  (JB02000A)

引用文献 (11件)：

• Affeldt, R. and Kobayashi, N.: Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes, Proc.11th International Workshop on Expressiveness in Concurrency (EXPRESS 2004)(2004).
• Cardelli, L. and Gordon, A. D.: Mobile Ambients, LNCS, Vol.1378, pp. 140-155(1998).
• Cardelli, L. and Gordon, A. D.: Anytime Anywhere Modal Logics for Mobile Ambients, POPL’00, Proc.2000 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 365-377(2000).
• Cardelli, L. and Gordon, A. D.: Mobile Ambients, Theoretical Computer Science, Vol.240, pp. 177-213(2000).
• Clarke, E., Grumberg, O. and Peled, D.: Model Checking, MIT Press (2000).

タイトルに関連する用語 (3件)： 物流システム ,  モデル ,  検査システム