(sigemb-info 297) 参加募集：「Bメソッドを用いた形式仕様記述と検証」(9/4)

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

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

この場をお借りして、下記のチュートリアルの参加募集の案内を送付させて
いただきます。

「Bメソッドを用いた形式仕様記述と検証」
 日時：2008年9月4日　10:00 - 17:00
 会場：国立情報学研究所

重複して受け取られる方にはお詫びいたします
フォーマルメソッドにご興味をお持ちの方は奮ってご参加ください。
--
吉岡信和(NII)


-----------------------------------------------------------------------
　　　　　　日本ソフトウェア科学会 チュートリアル 
　　　　　　 トップエスイーチュートリアルシリーズ
　　　　　　「Bメソッドを用いた形式仕様記述と検証」
　　　　　　　　　　　　参加募集のご案内
　　　http://www.topse.jp/tutorial/B-tutorial-20080904.html

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

本チュートリアルは，データ構造の記述／検証手法の一つであるBメソッドの講
演となります。

ソフトウェアの信頼性を向上させる基礎技術として，ソフトウェアの仕様を数学
的な基礎のもとに記述し検証する，形式手法が注目されています．形式手法は，
厳密な仕様記述を核とするソフトウェア開発手法として1960年代から研究が続け
られてきましたが，近年では仕様記述／検証を支援するツールの性能が飛躍的に
高まったことと，実適用のためのノウハウが蓄積されてきたことにより，適用範
囲を急速に広げつつあります．形式手法には，システムの振る舞いの記述と検証
に適した手法と，システムが扱うデータ構造の記述と検証に適した手法がありま
す．これまでソフトウェア科学会ではSPINやUPPAALのチュートリアルを開催し，
振る舞いの記述／検証手法を紹介してきました．本チュートリアルでは，データ
構造の記述／検証手法の一つであるBメソッドを紹介します．

BメソッドはJean-Raymond Abrial氏を中心として考案された形式手法で，仕様記
述からプログラム作成までの開発過程をカバーしていることと，その全過程を支
援する商用のツールが提供されていることが特徴です．実システム開発への適用
を志向した実践的な手法であり，パリ地下鉄や空港シャトルなどの適用事例が知
られていますが，ツールの支援がなくては手法を理解し使いこなすのが難しいこ
ともあり，日本の産業界ではあまり知られていませんでした．しかし近年，商用
ツールをベースとする無償のツールB4free（http://www.b4free.com）が，大学;
研究機関だけでなくWebから登録すれば誰でも利用できるようになり，試用する
ための環境が整ってきました．

このような背景から本チュートリアルでは，形式手法の入門者を対象に，簡単な
例に基づいて，Bメソッドを使った仕様記述と段階的詳細化の流れを，ツールを
使った検証の実演を交えて解説します．

講師は，国立情報学研究所で行われている先端ソフトウェア技術者育成プログラ
ムでも講師をされている，石川冬樹氏（国立情報学研究所）と来間啓伸氏（日立
製作所／国立情報学研究所）となります．

本チュートリアルはソフトウェア技術者にBメソッドを紹介することを目的とし，
形式仕様記述と検証の理論的側面ではなく，ソフトウェア開発の道具としての側
面に重点を置いて進めてゆきます．形式仕様記述言語を使ったソフトウェアの仕
様記述と検証に関心を持つ技術者の方，形式手法に興味のある学部や大学院の学
生，高い信頼性を持つソフトウェアの開発過程に関心のある技術者や技術管理者
の方など，多数の皆様のご参加をお願い申し上げます．

なお，本チュートリアルではツールを使った実演も行う予定です．参加される方
は，ツールをインストールしたノートPCを当日持参されることをお薦めいたしま
す．参加者へのPC貸与はございません．例題アーカイブは，ツールをインストー
ルしたディレクトリにコピーしてください．リストア方法は，当日説明いたしま
す．

例題アーカイブ：
　http://topse.jp/tutorial/B-examples.tgz
B4freeインストール手順:
　http://topse.jp/tutorial/B4Free-InstallGuide.pdf

［プログラム］
10:00 - 11:00 ... 形式仕様記述導入・Bメソッド概要, 簡単な記述例
11:00 - 11:15 ... 休憩
11:15 - 12:15 ... B言語を使った仕様記述, 仕様の整合性の検証

13:30 - 15:00 ... 仕様の段階的詳細化, 詳細化の正しさの検証
15:00 - 15:30 ... 休憩
15:30 - 17:00 ... 今後の動向

［テキスト］
主催者が用意した資料を，テキストとして使います．資料は当日配布します．

［参考書］
次の本が参考になります（必須ではありません）．
会場での配布／販売はいたしませんので，必要な方は各自ご用意ください．

　中島震監修，来間啓伸著：Bメソッドによる形式仕様記述，近代科学社
　ISBN978-4-7649-0347-0

■ 講師
　石川冬樹氏（国立情報学研究所）
　来間啓伸氏（日立製作所／国立情報学研究所）

■ 日時
　2008年9月4日　10:00 - 17:00
　受付開始：午前9:30

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

■ 募集定員
　３５名
　定員に達した時点で，申し込みを締め切ります．

■ 参加費

　一般会員　　7,000円 
　一般非会員 20,000円 
　学生会員　　2,000円 
　学生非会員　4,000円 

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

　　http://www.topse.jp/tutorial/B-tutorial-20080904.html

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

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

ふりがな  :
氏名      :
所属      :
電子メール:
会員区分  : 会員・非会員 (該当するものを残してください)
学生区分  : 学生・一般  (該当するものを残してください)
会員番号  : (入会手続き中，および当日申し込みの場合は“手続き中”とご記入ください)
会員種別  : 日本ソフトウェア科学会・情報処理学会 ソフトウェア工学研究会 (該当するものを残してください)

　※日本ソフトウェア科学会への入会は、当日申し込み頂けます。

■ 主催：
・日本ソフトウェア科学会 

■ 協賛：
・国立情報学研究所 ＧＲＡＣＥセンター
・情報処理学会 ソフトウェア工学研究会