長谷川 哲夫

【担当講義】
性能モデル検証

【所属・役職】
株式会社 東芝 ソフトウェア技術センター 先端ソフトウェア開発担当 グループ長

【研究分野】
モデル検査、自律分散システム、エージェントシステム、サービス指向アーキテクチャ

【ひとこと】
モデル検査ツール「UPPAAL」を使用して時間に関する制約の検証方法を学びます。UPPAALは時間制約を扱えるのが特徴ですが、システムモデルの定義や反例のトレースが行えるGUIを持ち、システム動作が理解しやすいためモデル検査の入門としてもお薦めです。