(sigemb-info 375) [参加募集] UPPAALを使った時間制約の検証(3/27)

["N. Yoshioka" <nobukazu@xxxxxxxxx>]

組込みシステム研究会の皆様

本MLをお借りして、UPPAALを使った時間制約の検証のチュートリアルの
参加募集の案内をお送りさせていただきます。
皆様の参加をお待ちしております。
-- 吉岡信和(NII)

************************************************************************
　　　　　　 トップエスイーチュートリアルシリーズ
　　　　「モデル検査ツールUPPAALを使った時間制約の検証」
　　　　　　　　　　　　参加募集のご案内
　　　http://www.topse.jp/tutorial/UPPAAL-tutorial-20090327.html

■ チュートリアルの趣旨と概要:

本チュートリアルでは、システムの時間制約をモデル検査ツールUPPAALによっ
て検証する方法について講演します。

ソフトウェア開発の上流工程で信頼性を向上させる技術として，形式手法の一
つであるモデル検査に基づく設計検証が注目されています。従来，形式手法は，
宇宙探査機や原子力発電所の制御など高い信頼性を必要とするシステムの検証
に用いられていましたが，組み込みシステムの分野においてもソフトウェアの
複雑化に伴い，もはや，人手によるレビューが困難になりつつあり，モデル検
査の活用が望まれています。また，モデル検査を行うためのツールの開発・公
開により，一般のソフトウェア技術者もその技術を利用可能になってきました。

モデル検査を行うツールとしては，SPINが有名ですが，本チュートリアルでは，
特に時間制約をモデル検査ツール UPPAALで検証する方法をお話します。時間制
約は，応答時間が重要となる組込みシステなどでは，重要な要素です。しかしな
がら，SPINなどのモデル検査ツールでは，時間を直接的に扱えないためシステム
の時間制約が成り立つかを網羅的に調べ，それを保証するのが困難でした。

本チュートリアルでは，時間制約を考慮した設計の概論からはじめ，UPPAALのモ
デルで表現し，それを検証する手順を，具体的な設計例をもちいて実践的に解説
していただきます。具体的には，出力である反例を分析する際の留意点について
説明した後，実際のアプリケーション事例を使いながら，時間制約をUPPAALでど
のように検証するかを解説していただきます。

講師には，国立情報学研究所で行われている先端ソフトウェア技術者育成プログ
ラムでも講師をされている長谷川哲夫氏と石川冬樹氏をお招きしました。

受講対象は，ソフトウェア開発に携わる技術者や技術管理者の方，大学院生でプ
ログラムの形式検証に興味のある方，これからこの分野の研究をはじめようとさ
れる方などです。多数の皆様のご参加をお願いいたします。

[プログラム]

1)形式手法とモデル検査
　・形式手法とは何か？
　・モデル検査で何ができるのか？

2)モデル検査ツールUPPAAL
  ・UPPAALの紹介
　・例題を使ってUPPAALを操作

3)時間制約の検証
　・時間が扱えると何がうれしいか
　・モデルに表現すべき時間の種類とモデル化
　・事例によるモデル化と検証

(1)では，まず，最近注目されている形式手法について概論した後，ソフトウェ
アの設計工程においてモデル検査がどう使えるのか，何ができるのか，モデル
検査を行うために通常の設計工程に比べてどのような情報を用意しなくてはな
らないのかを整理します。(2)では，UPPAALがどのようなツール化を体験・理解
してもらいます。そして，(3)では，事例を基に時間制約の扱い方を学び，理解
を深めてもらいます。

講演中，UPPAAL の簡単な使用方法もご説明する予定です。可能な方は UPPAAL 
システムをノート PC などにインストールして当日お持ちください。
UPPAAL システムのインストール方法に関しては，以下の URL を御覧下さい:

  http://topse.jp/tutorial/UPPAAL-install.html

※時間の関係でプログラムが若干変更になる場合がありますことを，ご了承下
  さい。なお、本チュートリアルは、2007年11月に行われたソフトウェア科学
  会主催の同タイトルのチュートリアルのツール情報などを更新した内容にな
  ります。

■ 講師
　長谷川哲夫氏 (東芝 ソフトウェア技術センター)
　石川冬樹氏 (国立情報学研究所)

■ 日時:
・2009年3月27日(金)
・午前10時00分〜午後5時（受付開始：午前9時半） 

■ 会場
・国立情報学研究所 ２０階ミーティングルーム１・２
　〒101-8430 東京都千代田区一ツ橋２−１−２ 
　Web: http://www.nii.ac.jp/introduce/access1-j.shtml 
　最寄り駅: 東京メトロ半蔵門線／都営地下鉄三田線・新宿線「神保町」A8出口、
　もしくは、 東京メトロ東西線「竹橋」1b出口から徒歩3〜5分 

■ 募集定員
　30名(先着順)

■ 参加費
　一般会員　　7,000円 
　一般非会員 20,000円 
　学生会員　　2,000円 
　学生非会員　4,000円 

　※NPO法人 トップエスイー教育センター、日本ソフトウェア科学会、情報処理学会
　　ソフトウェア工学研究会の会員が割引の対象となります。
　※GRACEセンター協賛企業の方は別途お問い合わせ下さい。

■ 申込み方法

・本ご案内の最後についている参加申込みフォーマットに必要事項を記入し，お問
　い合わせ先宛，"UPPAAL Tutorial"というタイトルで電子メールでお送り下さい。
・参加費は当日，会場受付でお支払い下さい．領収書をお渡しします。
・定員に達し次第, 申し込みを締め切らせていただきます。
・空席状況については定員が一杯になりしだい，

　　http://www.topse.jp/tutorial/UPPAAL-tutorial-20090327.html

　に掲示しますので，こちらもご参照ください。

■ お問い合わせ先
　GRACEセンター トップエスイーチュートリアル事務局:
  E-mail: uppaal-tutorial(atmark)grace-center.jp

■ 参加申込みフォーマット

ふりがな  :
氏名      :
所属      :
電子メール:
会員区分  : 会員・非会員 (該当するものを残してください)
学生区分  : 学生・一般  (該当するものを残してください)
会員種別  : トップエスイー教育センター・日本ソフトウェア科学会・
　　　　　　情報処理学会 ソフトウェア工学研究会
　　(該当するものを残してください,日本ソフトウェア科学会、情報処理学会
　　 ソフトウェア工学研究会の場合は、会員番号を記載してください)
備考      :

　※NPO法人 トップエスイー教育センター(入会費:12,000円)には、当日入会い
　ただけます。　参加と同時に入会をご希望される方は、備考欄に「NPO法人入
　希望」と　ご記入ください。会費は会場受付でお支払いいただきます。

■ 主催：
・NPO法人 トップエスイー教育センター
■ 協力：
・国立情報学研究所 GRACEセンター
■ 協賛：
・日本ソフトウェア科学会 ソフトウェア工学基礎研究会
・情報処理学会 ソフトウェア工学研究会
・キャッツ株式会社