TOPSEのEvent-B/RODIN集中セミナーに行ってきた！それについて、何回かに分けてメモメモ！
するけど、今回は、全体的な話。
Event-Bというと、普通の印象は、要求仕様の検証。
Rodinなんかが有名なわけなんだけど、このRodinがかなり進化したみたい。
検証だけでなく、モデル検査やシミュレーションもできる上、
記述に関しても、かなりの支援が付くようになった。
その結果、もしかすると、他の形式仕様、例えばVDMなんかよりも、
書きやすくなったかもしれない。
そのへんを、今日はご紹介してみる。
なお、以降紹介することは、このセミナー用のRodinだとできることで、普通にダウンロードしただけでは、ここまではできず、プラグインを入れまくると、こうなるらしい。
■書きやすくなったエディタ
昔のRodinは、たしか
みたいな、ふつうの感じのエディタと
のEbent-B用エディタしか、なかったんじゃなかったっけ？
ちがったっけ？
今は、Rodinエディタっていうのがあって、
な感じの画面になる。
そして、入力は、
のように、右クリックから、いろいろな要素を選んで行うことも出るし
上にウィザードがあって、そこをクリックすると、
のように、入力支援ダイアログがでてくる。
■自動的に検証しているみたい
で、書き終わると、
なんか、検証してくれているみたい（POのところに並ぶ）
■証明に何が足りないかがわかる。
いま、この記述は、
不変条件 nは０より大きい
初期値 n=5のとき
イベント n=n+1
になっている。ここで、
イベント n=n-1
にかえる。当然そうすると、証明できなくなる。
（イベントが６回起きると、nはマイナスになり、不変条件を満たさなくなる）
で、ここからがすごい。
その茶色の証明できないPOをダブルクリック！
証明できないところが出てくる。
ここで、Goalに注目！
n-1が０より大きいと出ている！
これが証明できない・・・そうそう、この条件がイベント１にないと、
確かに不変条件を満たさない。
ということで、この足りない条件を、ガードに入れると、
（ここ、コピーできる）
証明できた。
■さらに、シミュレーション？
右ボタンクリックで、Start Animation/Model Checking
を選択すると、
な感じになる。左上のINITIALIZATIONをクリックすると、
evt1が今度緑になってクリックでき、
緑の三角形（ここでは、evt1しかならないけど）
をクリックしていくと・・・
真ん中に値の変化、右側に履歴（クリックして実行したもの）
が出ている。
■モデル検査
ここで、Checksをクリックすると、Model Checkingとでてくるので、
これを選択。
デフォルトだと、デッドロックと不変条件のチェックを
してくれるらしい。真ん中下のボタンをクリック
なんかやらかしたらしい・・・Detailsをクリック
下に説明が出てくる。
なお、ここで言っている「デッドロック」とは、
いわゆる排他制御でおこるデッドロックだけでなく、
どのイベントにもいけなくなることをさしている
（排他制御のデッドロックもどこにもいけなくなるが、
それ以外の理由も含む）
ｎが２になったとき、evt1に入るとn=1となる。
しかし、n=1となると、次に実行できるイベントがない
そのため、デッドロックになる。
なんか、知らぬ間にEvent-Bが進化して、シミュレーションまで出来るように
なってきた。これ、通信プロトコルのチェックとかにいいかも？
するけど、今回は、全体的な話。
Event-Bというと、普通の印象は、要求仕様の検証。
Rodinなんかが有名なわけなんだけど、このRodinがかなり進化したみたい。
検証だけでなく、モデル検査やシミュレーションもできる上、
記述に関しても、かなりの支援が付くようになった。
その結果、もしかすると、他の形式仕様、例えばVDMなんかよりも、
書きやすくなったかもしれない。
そのへんを、今日はご紹介してみる。
なお、以降紹介することは、このセミナー用のRodinだとできることで、普通にダウンロードしただけでは、ここまではできず、プラグインを入れまくると、こうなるらしい。
■書きやすくなったエディタ
昔のRodinは、たしか
みたいな、ふつうの感じのエディタと
のEbent-B用エディタしか、なかったんじゃなかったっけ？
ちがったっけ？
今は、Rodinエディタっていうのがあって、
な感じの画面になる。
そして、入力は、
のように、右クリックから、いろいろな要素を選んで行うことも出るし
上にウィザードがあって、そこをクリックすると、
のように、入力支援ダイアログがでてくる。
■自動的に検証しているみたい
で、書き終わると、
なんか、検証してくれているみたい（POのところに並ぶ）
■証明に何が足りないかがわかる。
いま、この記述は、
不変条件 nは０より大きい
初期値 n=5のとき
イベント n=n+1
になっている。ここで、
イベント n=n-1
にかえる。当然そうすると、証明できなくなる。
（イベントが６回起きると、nはマイナスになり、不変条件を満たさなくなる）
で、ここからがすごい。
その茶色の証明できないPOをダブルクリック！
証明できないところが出てくる。
ここで、Goalに注目！
n-1が０より大きいと出ている！
これが証明できない・・・そうそう、この条件がイベント１にないと、
確かに不変条件を満たさない。
ということで、この足りない条件を、ガードに入れると、
（ここ、コピーできる）
証明できた。
■さらに、シミュレーション？
右ボタンクリックで、Start Animation/Model Checking
を選択すると、
な感じになる。左上のINITIALIZATIONをクリックすると、
evt1が今度緑になってクリックでき、
緑の三角形（ここでは、evt1しかならないけど）
をクリックしていくと・・・
真ん中に値の変化、右側に履歴（クリックして実行したもの）
が出ている。
■モデル検査
ここで、Checksをクリックすると、Model Checkingとでてくるので、
これを選択。
デフォルトだと、デッドロックと不変条件のチェックを
してくれるらしい。真ん中下のボタンをクリック
なんかやらかしたらしい・・・Detailsをクリック
下に説明が出てくる。
なお、ここで言っている「デッドロック」とは、
いわゆる排他制御でおこるデッドロックだけでなく、
どのイベントにもいけなくなることをさしている
（排他制御のデッドロックもどこにもいけなくなるが、
それ以外の理由も含む）
ｎが２になったとき、evt1に入るとn=1となる。
しかし、n=1となると、次に実行できるイベントがない
そのため、デッドロックになる。
なんか、知らぬ間にEvent-Bが進化して、シミュレーションまで出来るように
なってきた。これ、通信プロトコルのチェックとかにいいかも？
アクセス
トータル
ランキング
