Experiment of a Freight Management System with the Multiple Ambient Calculus

We are developing a freight management system that confirms the correctness of container handling during shipping. The system determines the correctness by comparing container handling, which is sensed by UHF RFID tags, with formal models (formulae) written in the Multiple Ambient Calculus(MAC). MAC is a formal description language extended from the Ambient Calculus(AC) in order to express freight systems with 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 container while, using AC, 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. This paper shows the implementation of the freight management system and the results of several experiments.