4K-5
Ambient Logic モデル検査におけるプロセス式のグループ化による検証の効率化
○森田哲平,加藤 暢,樋口昌宏(近畿大)
物流システムの満たすべき性質の形式的な記述体系に対するモデル検査の
新たな手法を提案する。我々は Ambient Calculus による物流システムの
記述と、実際の物流がその記述どおりに行われているかを監視するシステム
を開発した。また、この監視システムによる物流管理の正しさを形式的に
確認するための手法と、その手法に基づいた検査システムも構築した。
しかし、書類から生成されたプロセス式の検証は多大なメモリと検証時間
が必要となる。そこで、これらの問題、特に使用メモリを軽減する手法と
して同一の輸送経路を持つ貨物を表すプロセス式を一つのグループとして
扱う手法を提案し検証実験を行った。