抄録
B-006
並列制御システム設計のUMLアクティビティ図に対するペトリネットによる正当性検証
關屋貴詞・和崎克己(信州大)
モデル駆動開発は,生産性・再利用性の向上といった点で有用である. UMLを用いた上位設計は,レビュー工程に適している反面, 記述規則が曖昧で,構造・振る舞い両面での検査が別途必要である. 他方,ペトリネットに代表される形式記述法は並列動作を伴う制御システムの 検証能力が高いが,抽象度の問題により記述性が低い. 本研究では,設計と検証系との中継手段として,UMLアクティビティ図の記述規則と 構造条件を定義し,あるクラスのペトリネットへの自動変換と解析を提案する. 具体的には,構造誤りの設計者側へのフィードバックを目的とし, UMLアクティビティ図の構造的正当性を,変換後のネット構造の制約の下で確かめる.