池田 彩恵 さん(電子情報システム学科4年)が情報処理学会第80回全国大会において学生奨励賞を受賞しました

【受賞者】池田 彩恵 さん(電子情報システム学科4年)
【指導教員】松浦 佐江子 教授(電子情報システム学科)
【発表題目】要求分析段階におけるモデル検査技術を用いた設計制約検証の自動化
Automatic Verification of Design Constraints on Requirements Analysis Model using Model Checking

複数の機器が通信を行うことでサービスを提供する複合システムは、各機器が連携して正しくデータをやり取りする必要があります。システム開発において、各機器の連携はUMLモデルで定義できますが、UMLには通信発生のタイミングや通信時間といった設計制約の明示的な記述要素が無いため、各機器が取り得る膨大な状態から機器が同期しない状態を人の目で確認することが困難であるという問題点があります。本研究では、システムの状態を網羅的に検査できるモデル検査技術を用いて、各機器が設計制約を満たし同期を取るかを自動的に検証することを目的としています。

UMLモデルをモデル検査ツールUPPAALのモデルに自動変換し、並列動作をシミュレートして設計制約を満たすことを検証する手法を提案しました。本研究では、モデリングツールastahで記述したUMLモデルをXMLファイル形式のUPPAALモデルに自動変換するツールを開発しました。

UMLモデルからUPPAALモデルに変換するツールの基礎を作成できたため、今後はシステムの事前条件、事後条件の定義を変換できるようにするなど、より実際のシステムに則した状態を検証できるようにすることが本研究の課題です。