情報処理学会 第77回全国大会講演要旨

複数機器による組み込みシステムは、各機器が協調して目的を達成している。目的を達成するためのシステムの振る舞いをUMLアクティビティ図で表したワークフローにより表現できる。しかし、ワークフローが各機器の通信、時間などの設計制約を満たすかを確認する事は難しく、下流工程での手戻りの原因になっている。そこでワークフローに設計制約を表現するステレオタイプやタグ付き値を与え、モデル検査ツールUPPAALのモデルに変換して安全性、活性を検査し、検査結果をワークフローにフィードバックする方法を提案する。本稿では複数ロボットが協調する荷物の自動搬送システムへの適応事例により、その有効性を示す。