うぃんつり3.1

情報系研究所准教授(32)のブログです。Twitter/Facebookができてからは、海外出張時における仕事外の話を書くだけの場になってしまっています。

VDM

形式手法系イベントのお知らせ: 入門セミナー

いまだにやっぱり「形式手法とは?(きちんと聞きたい)」というくらいのニーズをぶつけて下さる産業界の方々が多いのと,かといってこういうWebサイトで読み物を提供するだけだと何とも言えないことが多いので,「実際に触ってみる」入門セミナーをやらせていただくことになりました.

詳しくはこちら

ありきたりな入門だけではなく,ついに和訳本が出たAlloyも含めて様々な手法を俯瞰するとか,最近よく整理されているガイダンスや応用事例集を俯瞰するとか,そういうことも要望が多いのでこの機会に整理する予定です.


なお,VDM++本は明日が発売日です.Amazonで買うと数日前にフライングゲットできたとの報告を受けています.そういう方がいらっしゃったことがありがたいです.

自分は出版社から先週もらっていたので,早速秋葉原のキンコーズに持ち込んで105円できれいにばらばらにしてもらいました.初めての自炊です.最後の方の校正何往復かはずっと紙ベースだったので,完成版はファイルとしては持っていないのですよね.もちろん個人的な利用のため(ぱっと内容確認したり検索したりするため)ということで.

ご報告1: 本が出ます

近代科学社からVDMの本を出させていただくことになりました.監修者の九大荒木先生には本当にお世話になりました.27日発売です.


本という媒体では厳しいところ,例えば最新のツールの具体的なことや記述例のバリエーションについては,関連してWebサイトも簡単に作りました.Eclipseベースの新しいツールであるOverture IDEの利用法説明も含め,細かいマニュアルを見る段階に行く前に必要になるところと実際によく聞かれる(はまりやすい)ところは一通り書きたいと思っています.まぁこの辺は単に,どうせ年に何度も,そして毎年聞かれるから(かといって全部予め話すことは到底できないから)なんですけどね.


こういうところは,トップエスイー日科技連SQiPなどで,多くの産業界の方々と関わるいろいろな機会をいただき,楽しくやらせていただいております.現場の実態とニーズ(あと偉そうですがレベル)が実感できるというのは本当に重要なことだと思います.

一方,こうやってその分野に浅くて国際的にImpact Factorの高いようなことを成し遂げたわけでもないぽっと出の人が,歴史ある当たり前のもの(コンピュータ科学がわかっていれば&英語でアンテナを張れば何てことはないもの)を日本語で解説し直すようなことで,こんなに目立ってしまうというのはどうなの?とも正直思っています(「日本のレベルが」という偉そうなことではなくて,自分自身の価値と位置づけについて).

もちろんサービスコンピューティング関連の研究は,今はやはりメインとして,方向性修正も含め進めています.一方,(関連したソフトウェア工学周りの方の)研究にも遅まきながら手を出し始めましたが,やっぱり片手間になってしまっているので,もっともっと時間をかけて世界に通じる結果を出さなければならない,ということが明らか.まぁがんばります.

アイルランド出張2回目の2: Overture/VDM

追記: Overture IDEの情報を求めて検索で来た方はこちらのページへどうぞ



たまにはお仕事の話も.

FM 2011に来ています.形式手法のトップ国際会議です.形式手法分野は,助教になって産業界向け教育活動を任されるようになってからちゃんと取り組むようになったのですが,さすがに研究でもそれなりの結果を出さなければなりません.研究のメインはサービスコンピューティングなのでかなりの片手間なのですが,ようやく「一流国際会議に論文を通す!」というところまで何とか来たくらい.FM 2011には全然間に合ってなかったですが...

今回は併設のOverture・VDMのワークショップで発表.今日一日の中で一番目新しいチャレンジングな話をしたはず(勝手にそう思っている).終了後に大御所が寄ってきて「これについて諸々話したい」と言ってもらえたのでまずはOKでしょうか.質疑で手抜き過ぎるひどい回答をしてしまいましたが...

VDMのコミュニティもちょっとclosedな感じでまずいかな,とずっと思っていましたが,怒濤のOverture IDEリリース,裏で進めている証明系や意味論定義の話,FP7でやっているリアルタイム性(離散系と連続系のハイブリッド)を扱う組み込み向けの話,聞くたびに大きく進んでいておもしろいですね.日本(だけ)で妙に流行っている感もありますがこれからどうなるやら.


夜はそのコミュニティの人たちとお食事.特にアイリッシュというわけではない普通の食事ですが,先々週来たときは食事の写真を載せてなかったので載せてみます.

traditionalだというクラムチャウダー.前菜ってレベルじゃない量.おいしかったです.
IMG_1121

北の方に来たから,と安易にサーモン.意外に小さい(それでも日本人には多いですしジャガイモ4個付いてますが).普通においしかったですが,クラムチャウダーの中にクラムよりサーモンがたくさん入っていてかぶりました.
IMG_1122

Puddingと呼ばれる何か.欧米のデザートの甘さには慣れていたつもりでしたが,こんなに甘いものは初めて.スポンジケーキをハチミツ+カラメルソースにどっぷり3時間付けておきました,って感じ.3分の1くらいでギブ.ヨーロッパの人もアイス部分しか食べてませんでしたし.
IMG_1123

形式手法系イベントのお知らせ

年度末&投稿シーズンにさしかかる時期ですが,下記のイベントを担当させていただきます.いずれも入門レベルです.


1/25(火): 日本ソフトウェア科学会 VDMチュートリアル
内容はVDM++言語・VDM++ Toolboxの入門です.Overture IDEについても紹介します.

3/23(水): NPO法人トップエスイー教育センターにおけるソフトウェア工学入門4日間(リンクは後日更新します)
4晩にわたり開催されるセミナーですが,この最終回に形式手法入門を担当します.モデル検査と形式仕様記述について,例題+ツールの要点をさらいながら紹介します.


最近サービスコンピューティング側のイベントが多かったのですが,水面下では形式手法系の話(上のような入門の話ではなくて)もいろいろ動いています.

[お仕事] ロンドン+α生活 23 VDM Workshop

追記: Overture IDEの情報を求めて検索で来た方はこちらのページへどうぞ


今日はFM 2009(形式手法の国際会議)併設のVDM-Overture Workshopに参加.

いろいろなご縁があってトップエスイーという場にて企業の方々にVDMを教えているわけですが,産業界でVDMがそれなりに盛り上がっているのは日本だけです.まぁ,
・ VDM Toolboxというツールの保有,保守管理元がCSKさん.
・ Felicaという世界的にも代表的な適用事例がある.
ですからね.海外の人なんかと話していると,けっこう「え,なんで今さらVDMなの?」というコメントをもらうこともあります.

もちろん形式手法については,「使うべきところが使っている」「知っている人はよく知っている」のは海外でももちろんそうなのですが,最近の日本では,それ以外の人々の「何だろう」「知らなきゃ」的な興味も引いているところがあります.変な期待を持たず,「何のためにどういうアプローチをとっていて,何ができて何ができないのか」という原則を「なるほど」と実感してもらって,視点を広げるのに効いているならよいことだと思いますが.


それはともかく,せっかくやることになっていていろいろな労力をかけたからには,研究にも絡めたいし,コミュニティの動向も追いたいし,そもそももっともっと誇れるものになってくれないと困るので,2件発表を持っていって参加してきました.

去年このワークショップに出たときは,大丈夫かなぁ(内輪気味,「イノベーション」「科学的な基盤」「研究」が少ない)と思ったのですが,それでもトップ陣はさすがという感じですね.いろいろ聞いたり話したりできたし,こっちの話もだいぶインパクトを与えられたようでよかったです.なかなかお会いできない方々(日本人含む)といろいろお話しできましたし.


とりあえず「(CSKさんの)VDM Toolboxは3年ほどで駆逐」ということになるかどうかはともかく,Overture(EclipseベースのVDMツール)は思ったより進んでいたという印象です.個人的には,リソースの問題はありますが,科学的・技術的進化のポテンシャルは間違いなくOvertureの方にあると思っています.
ようこそ!
  • 累計:

中の人(石川 冬樹)

情報系研究所の准教授(32歳)
神田・神保町付近

記事内容における意見・見解等は,所属機関によるものではありません.リンクはご自由にどうぞ.

記事検索
最新コメント
カテゴリ別
昔の記事へ
  • ライブドアブログ