@article{oai:ipsj.ixsq.nii.ac.jp:00192961,
 author = {加藤, 暢 and 高岡, 久裕 and 樋口, 昌宏 and 大山, 博史 and Toru, Kato and Hisahiro, Takaoka and Masahiro, Higuchi and Hiroshi, Ohyama},
 issue = {3},
 journal = {情報処理学会論文誌数理モデル化と応用（TOM）},
 month = {Dec},
 note = {海上コンテナ輸送では，気象や貨物量の急激な変化など様々な要因を考慮し，使用する船や中継港などは輸送の途中で動的に決定される．我々は，このような動的な物流計画を対象とし，コンテナ取扱の妥当性を自動的に判定する監視システムを開発している．これは，物流計画をプロセス代数の一種である多重Ambient Calculusでモデル化し，RFID機器を用いてとらえたコンテナの挙動とモデルを比較することでコンテナ取扱の妥当性を判定するものである．本稿ではまず本監視システムの実装について述べる．ところで，自動的に生成されるモデルが物流計画の内容を正確に反映していない場合，この監視活動は無意味なものとなってしまう．そこで本稿では，このモデルが，動的に変化する物流システムの所期の性質を満たすことを自動的に確認するモデル検査システムを提案する．, Vessels and hub ports used in maritime logistics of container are dynamically determined depending on various factors such as weather condition or the sudden increase of amount of containers. Aiming supervising such dynamically changing freight plans, we are developing a freight management system that can not only monitor the handling of containers with RFID devices but also confirms the correctness of it by modeling whole the freight plans with Multiple Ambient Calculus that is a kind of process algebra. This paper shows the implementation of the system. If the model includes wrong information, however, the system would be useless. Thus, this paper also proposes a model checking system that confirms the model satisfies the properties expected to the freight plan that dynamically changes.},
 pages = {84--99},
 title = {多重Ambient Calculusを用いた動的な海上物流計画に対するモデル検査},
 volume = {11},
 year = {2018}
}