■日 程：2011年6月6日(月)
■会 場：国立情報学研究所 20階ミーティングルーム(2009, 2010)
■講 師：（株）東芝 長谷川 哲夫、イーソル(株) 宇佐美 雅紀
セミナー概要
| 日 時 | 2011年6月6日(月) 10:00-17:00(9:30受付開始) |
|---|---|
| 会 場 | 国立情報学研究所 20階 ミーティングルーム１・２(2009, 2010) |
| 概 要 | ソフトウェア開発の上流工程で信頼性を向上させる技術として，形式手法の一つであるモデル検査による設計検証が注目されています。モデル検査は、システ ムが取り得る全状態を網羅的に検査し、システムが要求された性質や挙動を満たさない状態に到達する場合は、その状態に至るまでのパスを発見することができ ます。これにより、微妙なタイミングや多くの条件が重なることで発生する不具合の発見・解析に有効です。 本チュートリアルでは，特に時間制約を扱えるモデル検査ツールUPPAALを使って検証する方法について解説します。前半では、時間に関する情報を UPPAALでモデル化し、時間制約を検証する手法の概要を説明します。後半では、LEGO Mindstorm製のブロックソーター（LEGOブロックを色分けする機械）を例題に、実世界の時間制約をモデル化し検証する実習を行います。さらに、実際の開発におけるUMLによる設計モデルと、UPPAALによる検査モデル、ソースコードとの関係を考えていきます。 下記がチュートリアルの内容になります。 ・モデル検査ツールUPPAAL概論 ※トップエスイーチュートリアルは、GRACEセンターが実施しているトップエスイーの科目の内容を分りやすく1日で学べるチュートリアルです。本チュートリアルの詳細は、トップエスイーの開講科目「性能モデル検証」で学べます。詳細は事務局までお問い合わせください。 |
| 内容のレベル | 応用 |
| 講 師 | （株）東芝 長谷川 哲夫、イーソル(株) 宇佐美 雅紀 |
| 対 象 | 一般 ※ 定員 36 名（先着順） |
| 参加費 | 一般会員 10,000円（税込み）、一般非会員 23,000円（税込み） 学生会員 3,000円（税込み）、学生非会員 8,000円（税込み） ※NPO法人 トップエスイー教育センター会員、日本ソフトウェア科学会、に所属されている方は会員としてお申込ください。 ※キャッツ株式会社からの割引券をお持ちの方は、会員割引の対象となります。 ※参加費の一部（10%）を、東日本大震災の義援金として寄付いたします。 |
| 主 催 | NPO法人 トップエスイー教育センター |
| 協 力 | 国立情報学研究所 GRACEセンター |
| 協 賛 | 日本ソフトウェア科学会 ソフトウェア工学の基礎研究会、キャッツ株式会社 |
| お問合せ先 | セミナーに関するご質問などは、下記アドレスにて承ります。 seminar@topse.or.jp |