#etrobo 「VDMで戦うETロボコン2011～Project VDM 2年目の挑戦～」を読んで

オブジェクトの広場2011年11月号にProjectVDMさんのETロボコン2011参戦記が掲載されました。

著者の植木さんは、私が2011年4月から6月にかけてロボコンのモデルに関する記事を連載したときに、Twitterに記事の感想をつぶやいていたのをきっかけに知り合った方です。

今回は、2011年の東京地区大会が終わった直後に参加しての感想をつぶやいていたので、参戦記を書いてみませんか？と誘ったところ、快く了承していただいて立派な記事を書いてくださりました。ありがたいです。

実は直接お会いして話した経験はありません・・・。

■Project VDMさんの取り組みについて

ProjectVDMさんがやっていることは、ロボコンの制御プログラムを実装してしまう前に、アーキテクチャ（全体的な構成）の実現性を形式手法という手法で検証したというものです。形式手法の実装言語としてはVDM++、ツールとしてはVDMToolsやVDMUnitというものを使っています。

また、2010年参加時に検証に使ったコードをそのままモデルシートに載せても審査委員に伝わらなかったという反省を生かして、2011年はUMLモデルとの対応付けを分かりやすくしたとのことです。

■ETロボコンでも形式手法は使えそうだ

この形式手法というのは、私は業務で見た経験はないですが、航空業界などミッションクリティカルな分野で活用されているようですね。仕様の間違いによって発生する不具合で、大きな損害（人命、金銭）が出てしまう場合に、ものを作る前に仕様が正しいことを保証しようという目的で使われるようです。

複雑な状態遷移や、並行処理の微妙なタイミングによって不具合がおきやすいところは使いどころだと感じます。ETロボコンで言えば、以下のようなところに使えるのではないでしょうか？

• 各難所の走行制御の仕様化
• マルチタスクにした場合に時間制約を守れることの確認
• 走行体内の各ハードウェア制御や、Bluetooth通信を活用する場合の走行と通信応答の兼ね合いなど

実際に、ほぼ組さんはBluetoothを使って制御パラメタをPCに送信する仕組みを作っているようですが、その際にマルチタスク処理の仕様はLTSA（Labelled Transition System Analyser）という形式手法のツールで検証されていたようです。

■Project VDMさんのVDM活用について

一方で、Project VDMさんが活用しているのは、よくある区間切り替え部分の検証です。記事に書いている範囲では、UMLのクラス図やコミュニケーション図（もしくはシーケンス図）で確認できる範囲かな？という印象を受けました。「マルチタスクやらハードの制御が複雑に絡み合って、UMLでは確認できない」というものではない印象を受けました。

ただ、まとめの部分に制御アルゴリズムへの適用を匂わせている記述があるので、本当にVDMが生きてくるところは来年以降出てくるのかな？と期待しています。

■開発プロセスとの絡みが知りたい

読んでいて疑問に思ったのは開発プロセスとどう関係してくるのか？というところです。

実開発では、仕様が固まっていない状態で大規模に人員を投入するわけにもいかないので、実開発が始まる前に仕様を固める段階で形式手法によるモデル検証を行うのでは？と予想しています。

一方、ETロボコンでは、時間的にも人手的にも、そう悠長なことを言っていられないはずなので、開発のプロセスとモデル検証のプロセスが平行して、フィードバックをまわしていくのではないかと思います。

• 開発のプロセスでは、UMLでアーキテクチャとサブシステムを設計し、実装に落として、コースでの走行テストを行う。
• モデル検証のプロセスでは、仕様化が難しそうなところをピックアップして、モデルで検証した仕様を開発のプロセスに展開する。

両者は完全に分離しているわけではなく、開発のプロセスの中で走らせて分かったことはモデル検証のプロセスにインプットされるし、モデル検証のプロセスで検証したことは開発のプロセスへのインプットになります。

実際にやったわけじゃないので、妄想ですがｗ どなたかノウハウ持っていたら、ブログ記事にでも挙げてくれるとうれしいです。ワークショップに行って聞けば教えてもらえるかもしれないけど、ネットを補完的に使えたらいいなー＾＾；

■参戦記募集！

地区大会の参戦記では1本のみでしたが、希望者いれば他にも参戦記を書いてもらいたいと思っています。もし希望者いたら、私までご連絡ください。「地区大会敗退したけど書いてみたい」という人でも歓迎しますよ。