3J-01
要求分析段階におけるモデル検査技術を用いた設計制約検証の自動化
○池田彩恵，松浦佐江子（芝浦工大）
複数機器間での通信によりサービスを提供する複合システムのワークフローは,UMLモデルで定義することができる.しかし,UMLは,通信発生のタイミングや通信時間という設計制約の明示的な記述要素が無い.サブシステムは並列動作するため,設計制約により各サブシステムが取り得る膨大な数の状態から機器が同期しない状態を人の目で確認することは困難である.そこで,UMLモデルのフロー,シグナル送受信をモデル検査UPPAALモデルのプロセス,チャネルに対応付けて自動変換し,並列動作をシミュレートして,設計制約を満たすことを検証する手法を提案する.本稿では,大学のPBL課題である荷物自動搬送システムを事例として本手法の有効性を議論する.
footer 著作権について 倫理綱領 プライバシーポリシー セキュリティ 情報処理学会