[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

(sigemb-info 23) 「モデル検査を用いたソフトウェアの形式検証」チュートリアル参加募集のご案内

組込みシステム研究グループの皆様

＊＊同じ案内を複数受け取られた場合には，ご容赦ください＊＊

日本ソフトウェア科学会チュートリアル「モデル検査を用いたソフトウェアの
形式検証」参加募集をご案内いたします．

参加をご検討いただければ幸いです．

来間　啓伸　（（株）日立製作所　システム開発研究所）
----------------------------------------------------------------------------
-

日本ソフトウェア科学会チュートリアル
「モデル検査を用いたソフトウェアの形式検証」開催のご案内

コンピュータ・システムの信頼性に対する社会的要求の高まりとともに，シス
テムを数学的基盤のもとに記述し検証する，形式手法が注目されています．
形式手法は，形式言語を使った厳密な仕様記述を中核とするソフトウェア開発
手法として，1970年代より研究が続けられて来ました．近年では支援ツールの
性能が飛躍的に高まったことと，実適用のためのノウハウの蓄積が進んだこと
により，適用範囲を急速に広げつつあります．

モデル検査は，有効な検証ツールが登場したこともあり，形式手法の中でも注
目を集めている手法の一つです．日本ソフトウェア科学会では，関西企画委員
会によって2004年12月に大阪でチュートリアル「モデル検査を用いたソフト
ウェアの形式検証」を開催しましたが，この度その内容を一部改訂し，下記の
要領で東京を会場として再度開催いたします．

このチュートリアルでは，モデル検査を使ったソフトウェアの検証に関心を持
つ学生，研究者，技術者を対象として，形式手法やモデル検査の入門からツー
ルを用いた検証の方法までを，具体例に基づく実演を交えて実践的に解説しま
す．検証ツールには，定評のあるSPINを採り上げます．SPINはBell Labsで開
発され，現在はフリーのツールとして一般の研究者や技術者が容易に入手し利
用することができます．講師は，国立情報学研究所／科学技術振興機構の中島
震氏です．中島氏はソフトウェア工学の第一線で活躍され，特にモデル検査を
使ったソフトウェアの検証では，Webサービスや組込みシステムなどにおける
検証事例を含め，数多くの業績を挙げておられます．

形式言語を使ったソフトウェアの仕様記述と検証に関心を持つ研究者や技術者
の方，形式手法に興味のある学部や大学院の学生，高い安全性が要求されるシ
ステムの開発に携わる技術者や技術管理者の方など，多数の皆様のご参加をお
願い申し上げます．

[日時] 2005 年 9 月 28 日（水曜日） 10:00 - 17:00

[会場] 東京工業大学　西８号館３階Ｗ８３４号室
　　　　東急目黒線あるいは大井町線　大岡山駅より徒歩５分
　http://www.titech.ac.jp/access-and-campusmap/j/o-okayamaO-j.html

[講師] 中島震氏（国立情報学研究所／科学技術振興機構）

[プログラム]

　10:00 - 11:30  デザインと形式手法
  　               形式手法を使う目的は？
    　             形式手法の技術分野の概要

　12:30 - 14:00  モデル検査ツールSPINの基礎
  　               SPINを使ってみる
    　             具体的な例題を用いて

　14:15 - 15:45  SPINの応用
  　               SPINが用いている「検証」の方法
    　             検証性質の表現方法

　16:00 - 17:00  事例からの経験，今後の動向
  　               検証モデリングの重要性
    　             参考書のガイド
      　           関連する研究

　講演では，モデル検査ツールSPINの簡単な例題を使った操作実習も行われる
　予定です．聴講される方はSPINをインストールしたノートPCを当日持参され
　ることを，お勧めいたします．学会からのPCの貸与はございません．
　SPINは，UNIX，Solaris，Linux，Windows，MacOS Xで動作します．詳細は次
　のURLをご覧ください．多くの場合，インストールは容易です．
　http://spinroot.com/spin/whatispin.html

　・このチュートリアルではグラフィカルユーザインタフェースは使いません
　　ので，Xspin と Tcl/Tk の追加インストールは不要です．
　・SPINを使ってモデル検査する際には，CコンパイラとCプリプロセッサが必
　　要になります．
　　Windowsでは，SPIN に加えて，Cygwin（Cコンパイラパッケージを含めて）
　　をインストールすることをお勧めします．
　　http://www.cygwin.com/

　ご参考のため，Windows上でのインストール方法の概要を
　http://www.il.is.s.u-tokyo.ac.jp/~ishikawa/mcheck/installation.html
　にまとめてあります．

[テキスト] テキストは，学会で用意する資料を配布します．

[定員] 30 名
　　　（実習の都合上，定員になり次第締め切らせていただきます）

[参加費] 会　員: 学生 3,000 円  一般 15,000 円
         非会員: 学生 5,000 円  一般 20,000 円
　　　（注: 入会申し込み中の方は会員の費用で参加できます）
　　　参加費用には学会側で用意する配布資料の代金が含まれます．

[申し込み方法]
　聴講を希望される方は，下記の[開催案内／申し込み]ページで最新情報をご
　確認の上，案内にしたがってお申し込みください．
　電子メール，FAX，電話での申し込みはできませんので，ご了承願います．

　聴講申し込みは，定員に達した時点で締め切らせていただきます．定員に達
　しない場合は，2005年9月23日まで受け付けます．

　なお，このチュートリアルは2004年12月に大阪で開催された日本ソフトウェ
　ア科学会チュートリアル「モデル検査を用いたソフトウェアの形式検証」の
　一部改訂版であり，大部分の内容が共通することをあらかじめご了承願いま
　す．

[開催案内／申し込み]
　　　http://www.il.is.s.u-tokyo.ac.jp/~ishikawa/mcheck/

[問い合わせ先]
　　来間　啓伸　（くるま　ひろのぶ）
　　（株）日立製作所　システム開発研究所
　　電子メール: kuruma@xxxxxxxxxxxxxxxxx

----------------------------------------------------------------------------
-