**********************************************************************
セッションS4-b ワーク 
テーマ：実践形式手法 Event-B
講師：小川清（名古屋市工業研究所）
日時：2010/09/03 13:00〜14:30
参加人数：7名
**********************************************************************

WEB上にテキストが公開されており，ツールも含めてフリーで利用することがで
きる．UPPAALについても取り組んでいるが，商用は有償なため，Event-Bを取り
上げる．

当日配布資料
1
http://wiki.event-b.org/index.php/ASCII_Representations_of_the_Mathemati
cal_Symbols_%28Rodin_User_Manual%29

PDF版
http://deploy-eprints.ecs.soton.ac.uk/11/1/manual-2.3.pdf

2
http://wiki.event-b.org/index.php/UML-B_Tutorial

Event-BはBメソッドがベースとなっている．BメソッドのツールAterier-Bで作成
したものをEvent-BのツールRodinで利用できる．記述は，ダイナミックな区分と
スタティックな部分に区分される．ツール導入については別配布の資料にも掲載
した．proverbをチェックする必要がある．

Atelier B : http://www.atelierb.eu/index-en.php

予稿集に掲載したチュートリアルに従って，実際にやってみる．まず，プロジェ
クト，コンテキストを作る必要がある．

ローカル変数としてp,dを入れ，それぞれPERSON, DATEの要素とする．birthday 
に，pからdへの対応付けを入れる．記号がうまく入力できないときは，symbols
ウィンドウから入力することもできる．

保存すると syntax のチェックし，エラーがなければ証明まで行ってくれる．ヘ
ッダファイル相当のものを読み込まないとエラーになる．SEESでcarrier setを
選択する必要がある．初期化として，試しにbirthdayに0を入れた．しかし，
PERSONからDATEへの関係の集合の要素なので，空集合で初期化しなければならな
い．

内部の証明器だけでなく，外部の証明器を入れてみる．guardで，pはbirthdayの
ドメインの要素ではないというのを追加する．

このチュートリアル程度の小さいものなら7,8割は内部の証明器で証明できる．
その他は外部から入力する．

パースペクティブでUML-Bを選択する．これで，UMLをBメソッドで検証できる．
まだUML-Bは開発が進んでいる状況で，UMLの2割程度しか使えない．UMLで書いて
形式検証するという流れがあり開発は期待できる．VDMでも同様の動きがある．

次に，UML-Bを利用してみる．personクラスを作成する．attributeやeventを入
力する．UML-Bを使うことでUMLからEvent-Bへ変換することができ，それを証明
することができる．

他にも状態機械についてもいろいろ記述している．

形式手法のAterier-Bの基本的なツールがUML-Bで利用できる．また，UMLから
Event-Bへの変換が（一部）可能となっている．Bメソッドを使いやすくなってい
る．テキストは最初に具体例が載っているので，プログラマには取り組みやすい
と思う．論理式は難しいが，ツールを使っているうちにだんだん理解できるよう
になる．

北海道ではOSの検証に使おうとする動きがある．

テキストは10日くらいで学習可能である．言語ごとに10日もかけられない，とい
う相談も頂いているのでより良い方法について取り組んでいる．

富士ゼロックスがExecutable UMLからPromelaへの変換について取り組んでいる．
既存のツールを新たにいろいろ持ってきて新しいことに取組むより，今使ってる
もの，今の環境に適したツールを使うなり変換して使うと良いのではないか．

富士ゼロックスの例
http://www.jasst.jp/archives/jasst07e/pdf/D2-3.pdf

メーリングリストには，講師自身もいろいろ質問していた．質問しやすい雰囲気
になっていると思うので，是非質問があればメーリングリストへ．

■まとめ
UMLからBへ落とし込む手順について紹介した．
モデルを作る人も検証をできるようになっているのではないか．

以上．