本チュートリアルでは，システムの時間制約をモデル検査ツールUPPAALによっ て検証する方法について講演します。
ソフトウェア開発の上流工程で信頼性を向上させる技術として，形式手法の一 つであるモデル検査に基づく設計検証が注目されています。従来，形式手法は， 宇宙探査機や原子力発電所の制御など高い信頼性を必要とするシステムの検証 に用いられていましたが，組み込みシステムの分野においてもソフトウェアの 複雑化に伴い，もはや，人手によるレビューが困難になりつつあり，モデル検 査の活用が望まれています。また，モデル検査を行うためのツールの開発・公 開により，一般のソフトウェア技術者もその技術を利用可能になってきました。
モデル検査を行うツールとしては，SPINが有名ですが，本チュートリアルでは， 特に時間制約をモデル検査ツール UPPAALで検証する方法をお話します。時間制 約は，応答時間が重要となる組込みシステなどでは，重要な要素です。しかしな がら，SPINなどのモデル検査ツールでは，時間を直接的に扱えないためシステム の時間制約が成り立つかを網羅的に調べ，それを保証するのが困難でした。
本チュートリアルでは，時間制約を考慮した設計の概論からはじめ，UPPAALのモ デルで表現し，それを検証する手順を，具体的な設計例をもちいて実践的に解説 していただきます。具体的には，出力である反例を分析する際の留意点について 説明した後，実際のアプリケーション事例を使いながら，時間制約をUPPAALでど のように検証するかを解説していただきます。
講師には，国立情報学研究所で行われている先端ソフトウェア技術者育成プログ ラムでも講師をされている長谷川哲夫氏と石川冬樹氏をお招きしました。
受講対象は，ソフトウェア開発に携わる技術者や技術管理者の方，大学院生でプ ログラムの形式検証に興味のある方，これからこの分野の研究をはじめようとさ れる方などです．多数の皆様のご参加をお願いいたします．
【プログラム】(1)では，まず，最近注目されている形式手法について概論した後，ソフトウェ アの設計工程においてモデル検査がどう使えるのか，何ができるのか，モデル 検査を行うために通常の設計工程に比べてどのような情報を用意しなくてはな らないのかを整理します。(2)では，UPPAALがどのようなツール化を体験・理解 してもらいます。そして，(3)では，事例を基に時間制約の扱い方を学び， 理解を深めてもらいます。
講演中，UPPAAL の簡単な使用方法もご説明する予定です．可能な方は UPPAAL システムをノート PC などにインストールして当日お持ちください。 UPPAAL システムのインストール方法に関しては，下記、インストール手順を御覧下さい: なお，時間の関係でプログラムが若干変更になる場合がありますことを，ご了 承下さい. また、本チュートリアルは、2007年11月に行われたソフトウェア科学 会主催の同タイトルのチュートリアルのツール情報などを更新した内容にな ります。長谷川哲夫氏 (東芝 ソフトウェア技術センター)
石川冬樹氏 (国立情報学研究所)
国立情報学研究所 20階階講義室１・２室(2004,2005)(会場が変更になりました！)
30名(先着順)
| 一般会員 | 7,000円（税込み） |
| 一般非会員 | 20,000円（税込み） |
| 学生会員 | 2,000円（税込み） |
| 学生非会員 | 4,000円（税込み） |
GRACEセンター トップエスイーチュートリアル事務局: E-mail: uppaal-tutorial(atmark)grace-center.jp
ふりがな : 氏名 : 所属 : 電子メール: 会員区分 : 会員・非会員 (該当するものを残してください) 学生区分 : 学生・一般 (該当するものを残してください) 会員種別 : トップエスイー教育センター・日本ソフトウェア科学会・ 情報処理学会 ソフトウェア工学研究会 (該当するものを残してください,日本ソフトウェア科学会、情報処理学会 ソフトウェア工学研究会の場合は、会員番号を記載してください) 備考 :※NPO法人 トップエスイー教育センター(入会費:12,000円)には、 当日入会いただけます。 参加と同時に入会をご希望される方は、備考欄に「NPO法人入会希望」と ご記入ください。会費は会場受付でお支払いいただきます。