多重Ambient CalculusとUHF帯RFID機器を用いた海上物流監視システム

我々は，多重Ambient Calculus（MAC）による物流システムの記述方法の研究および，実際の物流が正しく行われているかを監視するシステムの開発を行っている．物流システムは，より小さなパッケージをより大きなパッケージに収容する階層構造を持っている．これに対し，プロセス代数の一種であるMACは，階層構造を持ち動的に構造が変化するシステムを形式的に記述できる．MACは，通常のAmbient Calculus（AC）と異なり，個々の貨物の取扱いを個別のプロセス式として記述し，それらの集合により物流システム全体をモデル化するものである．この特徴により，通常のACと比較して物流システムの持つ対称性，並行性をより適切に表現でき，貨物が追加，削除される際のプロセス式の変更も容易となる．本稿では，MACとUHF帯RFID機器を用いた物流監視システムを提案する．本システムは，実際のコンテナ輸送で使われる数種類の書類をもとに，各コンテナの搬送経路を表現するMAC式を自動生成するシステム，MACの個別式を適切な端末へと分散するシステム，およびRFIDを用いて検知した貨物の動きや，船の乗り換えがMAC式の遷移に沿ったものであるかを監視するシステムからなる．また，本システムの有用性を示すために，車をコンテナと見立てて行った屋外実験についても述べる．

We are investigating a way of modeling freight system in the Multiple Ambient Calculus (MAC) and the management systems ensuring the correctness of container handling during shipping using the model. Freight systems have nested structures, i.e., packages (e.g. containers) containing smaller packages (e.g. luggage) that are accommodated by a larger entity such as a container ship. MAC is a formal description language that is suitable for modeling such systems with the nested structures that dynamically change. Using MAC, whole the freight system is modeled by a set of formulae each of which represents the handling of each containers while, using the Ambient Calculus, the freight systems are modeled by a large formula. Thanks to this feature of MAC, we can express symmetric and concurrent property of freight systems more appropriately and adding or retracting formulae (representing adding or canceling containers for a voyage) becomes easier than using AC. The management system propsesed in this paper consists of three sub systems. The first generates formulae that represent freight systems based on several trading documents, the second deploys the formulae to each devices (PCs and RFID tags), the last senses the handling of containers by using UHF RFID devices and checks their consistency with the transitions of corresponding formulae. We also show the results of preliminary experiments in which a car is used as a container.