うぃんつり3.1

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

形式手法

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

いまだにやっぱり「形式手法とは?(きちんと聞きたい)」というくらいのニーズをぶつけて下さる産業界の方々が多いのと,かといってこういう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晩にわたり開催されるセミナーですが,この最終回に形式手法入門を担当します.モデル検査と形式仕様記述について,例題+ツールの要点をさらいながら紹介します.


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

[お仕事] ロンドン+α生活 25 Turing Award Winner Talk @ FM 2009

今日も,たまにはまじめにお仕事の話.

今日からFM 2009の本会議.細かい話は書きませんが,さすがに面白い話ばかり.


夜はTuring Award 2007(コンピュータの世界のノーベル賞みたいな)のE. Allen Emerson氏の講演.もちろん1980年代の彼らのModel Checkingに関する取り組みを振り返って,という話.Temporal Logicの導入について.そしてLTLのモデル検査の,オートマトン積Non-Emptyness判定問題への還元について.数百名の参加者の誰もが当たり前のように知っている話.だからこそすごい.

Computer Scienceに関わっていない人でも,IntelプロセッサなりIEEEプロトコルなりを通して,何らかの恩恵は受けているのではないでしょうか.

Emerson氏はそれなりにご高齢なわけですが,「テキサスからはるばる来て,乗ったタクシーの運転手がオランダ語しか話せなかったショックで声が出なくなってしまった」そうです.確かに最初はガラガラ声でしたが,のってきたら全く問題ないように見えました.そういった方でも1.5Lペットボトルのコーラを持ち歩いてがぶがぶ飲んでいるのがアメリカらしいというか何というか.


続いては若手のやり手,Joost-Pieter Katoen氏によるモデル検査はどこにでも(ubiquitous),という話.エンザイムの化学反応系の確率計算や,「複数電池のどれをいつ充電するのが最もライフタイムを長くするか」という最適化を,モデル検査で解くという話.後者の話なんかは,自分のところの学生さんなんかも関係ある話ですが,複雑な電池の消費・充電モデルを扱い,そしてまさかのUPPAALによる解法.


やっぱりComputer Scienceは面白いなぁと実感.ちなみに自分はComputer Science出身ですが,もっとComputer Scienceをきちんとやってくればよかったという後悔というか引け目があります.もちろんこれからの方向性は考えていて,まぁそれは書いてみるよりも実行ですね.


ちなみにFM 2011は2011年6月(FMは1年半ごと).アイルランド,つまりLEROです.今回はサブイベントで計3件発表ですが,次回はもっとインパクトのあることを持ってこなければですね.

[お仕事] ロンドン+α生活 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の方にあると思っています.

北九州出張(後): 形式手法系の会議の話

北九州では形式手法系の国際会議に1日だけ参加.この分野は教育・普及的なこともやろうとしているので,メインの目的はいろんな人と話してくることだったりします.とりあえず午前のブレイクのうちに,今書いている本にとって重要な方々とお話し.

今日は検証系のセッション.モデル検査におけるfairness検証の効率化から始まり,仕様検証を行った後の実装検証の対応付けなどなど.明日以降もBPMNの意味論とか自分的にぴったりな発表もあるのですが,諸事情により参加は今日だけです.

サービス指向系・エージェント系の会議だと何年もサーベイしてきたのでどの発表もだいたいぱっとわかるのですが,こっちは助教になってから本格的に踏み込み始めたところがあるので,まだまだ勉強不足ですね.

夜はバンケット.北九州なんだからフグが出る,そんな風に考えていた時期もありました.自分の泊まっていたホテルにフグ屋がありましたし.まぁ普通にいろいろおいしかったです.全く知らなかったのですが,小倉と言えば焼うどんなんですね.何かいつも食べてるのとは違う感じのが出てきました.小倉は焼きうどん発祥の地で,小倉発祥焼うどんっていうのがあるんですね.


明日からは滋賀でやっている別の国内会議に移動.こっちは2002年から皆勤賞.今年はついに論文を出しませんでしたが,運営にも関わってるので参加します.

CEDEC 2008(前): お仕事の部


昨日はCEDEC 2008に参加.ゲーム開発者系の一大イベント.


トップエスイー(企業開発者向け教育コース)関連のつてで,モデル検査の話をさせてもらいました.おおざっぱには「賢い総当たりテスト」であるモデル検査という技術が,他の複雑なソフトウェア開発と同じようにゲーム開発にも使えないかという話です.単に「同じように」というだけではなく,ゲーム固有のフラグ・シナリオ管理にばっちり役だったりしないか,というところもあります.

大学院の同期がそういう研究をやっていたのですが,偶然にも今回の話を持ってきてくれた方とも知り合いでした.世界は狭いですね!昨日はその彼が急きょ関西からかけつけてくれて話してくれたので,助かりました.自分はゲーム開発の実態(言語,プロセス,規模などなど)について何の実感もないですから.

商業イベントということで,セッションの開始10分前くらいまで聴講者を部屋には入れず並ばせていたのが印象的でした.もちろん講演中にPCを開くような人はゼロ.いつもよりもプレッシャーが大きかったです.

時間めいっぱい話してしまったのでじっくり議論という感じにはできなかったのですが,自分の話から何かしら得てもらったなら幸いです.とりあえず終わった後に,自分の問題にどう使えるか相談してくださった方もいたのでよかったです.

Bメソッドチュートリアル


今日はBメソッドという形式手法の1日チュートリアル.といっても自分が話したのは少しだけれども.無料版のツールはXEmacs上で動く前時代的なものなので,トラブル対応でぐったり.今年の12月に今の商用版が無料になればもっとよくなるはず.

いくらパリの地下鉄だの空港シャトルだので使われてようが,日本ではほとんど知られていないのでどうかなぁと思ったのだけど,まさかの満員御礼.今年度はろくに研究の時間もとれずに,形式手法の教育・実践に力を注いでいたけれども,それに見合うくらい,ほんとにブームが来ているのかもしれない.


そして来週はゲーム開発者会議で,今度はモデル検査についての講演.モデル検査なら他にもっと専門家がいるので申し訳ない感じもするのだけど,「ゲームが少しはわかる」「形式手法なんて,っていう人の感覚も残っている」というところの適性はあるのかもしれない.

ゲームに詳しい人にプログラム見せたらひどく興奮していたので,他の講演者はやっぱりそうそうたるメンツみたい.確かに自分は開発者やデザイナーの名前まではわからないけど,タイトルとしては自分にもわかるくらいのすごいのが並んでるし.講演者限定のレセプションとか実はすごい場なのではなかろうか.

バーゲンとBメソッド


バーゲンに行こうかと思ったものの,お目当てのお店は明日からだったので今日も実家に引きこもり.TVで混み具合を見ているともういいかなという気もしてきている.「セールに行くと,セール対象外のものでいいものを見つける」という法則があるし.

そんなわけで今日ものんびりと副業の論文調査.バーゲンに行っていたら使っていたであろう額の倍以上に相当する分の作業が進んだ.これはおいしい.


以下同業者向け.

論文調査でB method関連の論文を読みまくったのだが,特にヨーロッパにおける企業での活用が多くてものすごく有望な技術のように思えてきた.ところが日本語のページを検索すると,情報のなさがなかなかひどい.特に「Bメソッド」での検索だと,ほとんどうちのプロジェクトで数日前に出した本に関するページ.圧倒的じゃないか.

これはうまくやれば国内第一人者.もちろん普及させてなんぼだけど.とりあえず合間を縫ってもっと勉強しないと.
ようこそ!
  • 累計:

中の人(石川 冬樹)

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

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

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