UMLのEvent-B（要求の形式仕様言語）変換、SAPによるBPMNのEvent－B変換

シリーズTOPSEのEvent-B/RODIN集中セミナーに行ってきた！
前回は全体的な話だったけど、今回から内容。
今回は、Session1(１日目午前中）の話のメモメモ

なお、石川先生以外は、英語なので、それを日本語にしてメモメモしているため、
テキトーに間違っていると思います。その点よろしく・・

---

■石川先生
・プログラムを作るための検証
　　　→VDM／仕様のテストも

・仕様を作っていくための検証も
　　EventB：Bメソッドの発展
　　　eclipse上→プラグインも
　　　RODIN,DEPLOY
　産業界のケーススタディ
　　ロマノフスキー先生、エレナ先生

---

■ロマノフスキー先生

・複雑→バグ見つけるの大変→フォーマルメソッド

・サクセスストーリー
　　Bメソッド
　　　１９８９～
　　　１９９８～　パリ、メトロ
　　　２００７～　パリ、エアポート

　VDM
　　　２００８（？うちの席から良く見えん）　フェリカ　

　フォーマルメソッド：クオリティ向上
　　　→どうやって適用？

・フォーマルメソッドの開発
　　まだ広まっていない
　　なぜ難しい
　　セイフティケース→フォーマルメソッド

・Event-B
　　Bメソッド（J.R.Abrial 1990年代）
　　　抽象化
　　　モデル分析、証明、モデルチェック、アニメーション
　　　コレクトネス　バイ　コンストラクション
　　　Atelier B
　　　ソフト開発
　　Event-Bメソッド（J.R.Abrial 2003～）
　　　システムの振る舞いの推論
　　　抽象化サポート
　　　全システムのコンポーネントに対する抽象化サポート

・産業界のドメイン
　　輸送（鉄道・メトロ・シャトル）
　　自動車
　　情報システム
　　航空
　　通信
　　チップ設計
　　スマートグリッド
　　ヘルスケア／医療
　　防衛（UK/フランス）
　　ディペンダブル・ソフトウェア・フォーラム（DSF)

　FP6　EC　RODIN　Project
　FP7　EC　DEPLOY Project(2008-2012)
　after DEPLOY
FP7 EC ADVANCE Project(2011-2014)

具体的に
　RODIN Project：Nokia
　　　フォーマルアプローチ：テレコムにSOA
　　　Lyra
　RODIN Project：ATEC（という会社）
　　　Engine failure management systems
　RODIN Project：Praxis
　　　CCF　Display and Information system
　DEPLOY：ボッシュ
　　　RSML→問題フレームからEvent-B
　DEPLOY：siemens
　　　communication-based train control(CBTC)
　　　　ProB,RATPの検証
　DEPLOY:フィンランドの宇宙システム
　　　Bepi Colombo(ESA's first mission to Mercury)
　　　Attitude and orbit control system(AOCS)
　DEPLOY:SAP
　　　BPMNをEvent-Bへ変換
　DEPLOY associates
　　　クリティカルソフトウェアテクノロジー
　　　スマートグリッド
　Xcare マイクロプロセッサー　インストラクション　セット(ISA)
　　　XMOS XSI アーキテクチャ
　QNX ソフトウェアシステム(2011-12）
　　　セイフティケース、QNXニュートリノ、RTOS上
　Battle and clear sy(2011-12)

OUTSIDE and AFTER DEPLOY
　　Clear Sy(2012-2013)
　　防衛システム（UKとフランス）（2010-2013)
　　STマイクロエレクトロニクス
　　　モデリング、VHDLコード生成
　　　スマートカードのマイクロサーキット
　　Systeral(2010-2013)
　　　CBTCシステム（communication-based train control)
　　ディペンダブル・ソフトウェア・フォーラム（DSF)
　　　日本の会社：NTTデータ、富士通、日立、東芝など

　Advance(今活動中）
　　alstom
　　　ダイナミックな信頼性の有る電車のインターロッキング
　　　　　Interloking Dynamic Control(IDC)
　　スマートエナジーグリッド
　RODIN　エコシステム

　NPO Rodin Tool Ltd:ツールはOpen

　出版物
　RODIN User handbook
　　http://handbook.event-b.org/

　J.R.Abrial
　Modeling in Event-B : System and Software Engineering
　Cambridge Uni. Press 2010

Alexander Romanovsky
Martyn Thomas Editors
Industrial Deployment of System Engineering Method
Springerebook版

産業界のフォーマルメソッド利用
http://www.fm4industry.org

---

■エレナ先生

Event-B
　　マシン→コンテキスト

イベントの一般的な形
　　WHERE ガード THEN ボディ END

Lyra Design Method
　　UML2ベースのサービスオリエンティッドな方法論
　　UMLモデルをACCパターンへトランスレートする方法
　　

---

ちなみに、
UMLからEvent-B変換のLyraの話とかは、

Project IST-511599　RODIN
“Rigorous Open Development Environment for Complex Systems”
http://rodin.cs.ncl.ac.uk/D27FinalC.pdf

に出ているみたい。

ふなっしーYahoo２倍募金？

ふなっしーといえば、最近、まゆゆを助けたことで、絶賛有名中だが、
ふなっしーのYahoo２倍募金というのを

本紙記事「日本ユニセフ、寄付金の流れ透明化へ」についてご報告
http://kyoko-np.net/kenkai1311.html

で見た。

ふなっしーはさておき、２倍募金というのは、上記サイトのリンク先

【寄付が2倍】フィリピン台風支援募金
http://donation.yahoo.co.jp/detail/1630008/

でやっているらしい（自分の募金学分、YAHOOが上乗せしてくれる）。

ソフトウェア業界は、アベノミクスの恩恵を受けていない。その証拠

儲かってます？みなさん？？どう？？

まず、アベノミクスってのは、どんなものか見てみよう。
アベノミクスで、景気が良くなったそうだ。
たしかに、景気動向指数を見ると、

景気動向指数 平成25 年９月分（速報）の概要より引用

２４年１２月ごろからの伸びをアベノミクスというようなので、
１００から１１０くらい上がってる？
つまり、１０％くらい上がっていると、アベノミクスというようだ・・・

---

　一方、情報処理産業、SIはどうか？

　これは、特定サービス産業動態統計調査というのを見ると判る。
２０１３年９月確報値における、情報サービス業は、こんなかんじ。

平成２４年１２月からを見ると、受注ソフトウェア、システムインテグレーションは１００％前後で大きく動いていない。

　１０％程度動くのが、アベノミクスの成果だとすると、情報処理産業はぜんぜん恩恵を受けていない。

---

　では、最近はやりのネットワークではどうか。
　これは、インターネット付随サービス業を見ると判る。


　２４年１２月からみると、
　サーバー・ハウジング・ホスティングは１００％を超えたり、超えなかったり
　ASP(今で言うSaaS)も、１００％をかなり下回っている。

　セキュリティは絶好調なのかな・・・？
　セキュリティはアベノミクスの恩恵を受けている？

　かなり絶好調なのは、課金・決済代行とサイト運営。
　しかし、ここで考えたいのは、「課金・決済代行」が儲かるのは、それを利用したとき、つまり、ソフトウェア産業が儲かるときというより、他の小売などが儲かっているときにもうかる。サイト運営も、他の産業の業績にかなり依存しそう。
　つまり、これらは、他産業の影響を受けやすいものといえる。

---

　一致指数が１０％くらい上がり、
　他産業の影響を受けやすい課金・決済代行とサイト運営も１０％くらい上がっているのに、
　他の情報産業は、１００％（アベノミクス前と同じ）くらい

　ということは、情報産業はアベノミクスの恩恵を受けていないといえ、特定サービス産業動態統計調査の結果がその証拠といえる。