多数の貨物を扱う時間制約を含む物流計画の形式記述のための枠組みという観点から、Ambient Calculus の拡張について検討を行った。時間制約記述のため、ケーパビリティに有効期限付きのものを導入し、時間経過遷移を導入することにより、タイムアウト動作などが記述できる時間付きAmbient Calculus を提案した。一方、多数の類似する貨物を扱う物流を適切に表現するため、プロセス式の組により物流システムを記述する多重Ambient Calculus を提案した。また、それらの拡張を施したAmbient Calculus におけるモデル検査、および記述に基づいて物流管理を行う物流監視システムの構築について検討した。
|