(sigemb-info 602) 参加募集：MindStormで学ぶ、UPPAALによる時間制約の検証(6/6)

[Nobukazu Yoshioka <nobukazu@xxxxxxxxx>]

組込研究会の皆様

本MLをお借りして、6/6にNIIにて開催する「UPPAALによる時間制約の検証」
の案内をお送りいたします。皆様のご参加をお待ちいたしております。
--吉岡(NII)

━━セミナー開催のご案内━━━━━━━━━━━━━━━━━━
 【トップエスイーチュートリアル】
　　MindStormで学ぶ、UPPAALによる時間制約の検証
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
■日　程：2011年 6月6日(月)　10:00〜17:00（受付開始：9:30）
■会　場：国立情報学研究所 20階　ミーティングルーム1・2（2009・2010）
　　　　　〒101-8430 東京都千代田区一ツ橋２−１−２
　　　　　http://www.nii.ac.jp/introduce/access1-j.shtml
■概　要：
　ソフトウェア開発の上流工程で信頼性を向上させる技術として，形式手法の
一つであるモデル検査による設計検証が注目されています。モデル検査は、シ
ステムが取り得る全状態を網羅的に検査し、システムが要求された性質や挙動
を満たさない状態に到達する場合は、その状態に至るまでのパスを発見するこ
とができます。これにより、微妙なタイミングや多くの条件が重なることで発
生する不具合の発見・解析に有効です。
　本チュートリアルでは，特に時間制約を扱えるモデル検査ツールUPPAALを使っ
て検証する方法について解説します。前半では、時間に関する情報をUPPAALで
モデル化し、時間制約を検証する手法の概要を説明します。後半では、LEGO
Mindstorm製のブロックソーター（LEGOブロックを色分けする機械）を例題に、
実世界の時間制約をモデル化し検証する実習を行います。さらに、実際の開発
におけるUMLによる設計モデルと、UPPAALによる検査モデル、ソースコードとの
関係を考えていきます。

下記がチュートリアルの内容になります。

1.モデル検査ツールUPPAAL概論
　・UPPAALの紹介
　・UPPAALのモデル
2.時間制約の検証
　・時間が扱えると何がうれしいか
　・モデルに表現すべき時間の種類とモデル化に際しての留意点など
3.例題を基に、UPPAALによる検証を実習
　・LEGO Mindstorm製ブロックソーターを用いて
　　UPPAALを使った時間制約の検証を実習する

※トップエスイーチュートリアルは、GRACEセンターが実施しているトップ
　エスイーの講義の内容を分りやすく1日で学べるチュートリアルです。
　本チュートリアルの詳細は、「性能モデル検証講座」で学べます。
　詳細は事務局までお問い合わせください。

■講　師：
　（株）東芝 長谷川 哲夫、イーソル(株) 宇佐美 雅紀

■定　員：36名(先着順)

■受講料金：
　一般会員　 10,000円（税込み）
　一般非会員 23,000円（税込み）
　学生会員　  3,000円（税込み）
　学生非会員  8,000円（税込み）

※当日会場にて現金でお支払い下さい。領収書を発行します。
※参加費の一部(10%)を、東日本大震災の義援金として寄付いたします。
※「会員」：NPO法人 トップエスイー教育センター会員、日本ソフトウェア科学会、
　に所属されている方、キャッツ株式会社からの優待券がある方は会員割引の対象と
　なります。

■申込み方法

　下記サイトをご覧ください。
　　 http://www.topse.or.jp/docs/?q=node/23

※定員に達し次第，申し込みを締め切らせていただきます。

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

■お問い合わせ先
NPO 法人　トップエスイー教育センター　事務局:
　　E-mail: seminar@xxxxxxxxxxx

━ 今後のセミナー予定 ━━━━━━━━━━━━━━━━━
今後も、下記のように多数のセミナーを予定しております。

 6月下旬 13:00-17:00: （調整中）：edubaseで学ぶクラウド入門
 7月 10:00-17:00: （調整中）：Coqで学ぶ定理証明入門(仮)
    講師： (有)ITプランニング　今井宜洋

最新情報はウェブページ(http://topse.or.jp/)をご確認ください。