|
|
[2011 年 11 月号] |
［レポート]
私たち「Project VDM」チームは、ETロボコン2011の東京地区大会に出場しました。残念ながらチャンピオンシップ大会には出場できませんでしたが、昨年より東京地区内の順位も上がり、来年への手応えを感じています。
今回は、地区大会終了後、このオブジェクトの広場への記事執筆の機会をいただき、私たちのETロボコン参戦記を書かせていただくことになりました。そこで、私たちの取り組みを、チームの特色である形式手法VDMを中心に紹介します。
なお、本記事では2011年の東京地区大会提出モデルシートの内容を引用します。ぜひ実際のモデルシートも参照しながらお読みください。
まずは、私たちのチームをご紹介します。
私たち「Project VDM」は、2010年からETロボコンに参加し始め、2011年は参加2年目になります。今年のメンバーは、入社5年目から20年目までの幅広い年代から8人で構成されています。最も若くても入社5年目なので、メンバーそれぞれ様々な開発経験を持っています。ただ、今回のETロボコンのような「組込みシステム」を業務としているメンバーは1人しかいません。残りは組込み経験があるメンバーもいますが、現在はエンタープライズ系の業務を担当しています。これは、社内でETロボコンに参加したい人を自由応募で集めた結果なので、初めからこのような構成にしようとしたわけではありません。
そんなチームを作り、走り始めた私たちは、チーム名の通り形式手法である「VDM」をモデリング手法として、ETロボコンに参加した2年共採用しています。今年もVDMを使ったのには4つ理由があります。
私たちが使った形式手法VDMをご存じない方もいらっしゃると思いますので、ここで簡単に形式手法とVDMについて説明します。
形式手法とは、形式仕様記述言語という、プログラミング言語のように厳密に定義された文法を持った言語を用いて仕様や設計を記述し、その記述された仕様や設計をテストや網羅的検証、数学的証明によって確認するソフトウェア開発手法の1つです。
みなさんは普段ソフトウェアの仕様や設計をする時、ExcelやWordを用いて日本語で書いていると思います。ETロボコンであれば、UMLがメインでしょうか。日本語のような自然言語は、誰しもが読むことができ、書くことができます。しかし、みなさんが書いた仕様や設計の意図は、その読み手に正確に伝わっているでしょうか？また、UMLで書かれたモデルが正しいことは、どのようにして確認しているでしょうか？
一般的に、自然言語で記述された仕様や設計には曖昧さがあり、開発者の間で解釈違いを起こす可能性があります。これらを排除するために、形式手法は2つのアプローチをします。
形式手法は文法を持った言語で記述するため、曖昧さが排除され、誰が読んでも一意に仕様や設計を伝えることができます。それに加え、厳密に定義された文法の上で記述されることから、レビューだけでない検証手段を用いることができるのです。
私たちが使ったVDMは、形式手法の1つです。VDMには、VDM-SLとVDM++という形式仕様記述言語があり、主にテストによって仕様や設計の正しさを検証します。ちなみに、私たちは今回VDM++を使いました。これは、VDM++がオブジェクト指向言語であるため、実装のC++へ繋げやすく、モデルを説明するためのUMLも書きやすいことが理由です。
次節以降では、具体的に私たちがこのVDMをどのように使い、どのようなメリットや課題があり、どのような評価をされたかを解説します。
なお、形式手法やVDMについてより詳しく知りたい方は、以下の解説を読んでみてください。
@IT monoist "誰でも使える形式手法" - https://monoist.atmarkit.co.jp/mn/kw/embe_fm.html
さて、私たちがVDMを使った理由と、VDM自体をご説明しましたので、ここからは「ETロボコンにおいてVDMをどのように使ったか？」をご説明します。
端的に私たちの使い方を説明すると、「アーキテクチャの実現性と正しさを実装前に事前検証すること」です。この使い方の中で、私たちはETロボコンのシステム全体にVDMを使ってはいません。使った箇所は、後述のモデルシートにも出てくる、コースを区間とランドマークという独自に定義した単位に分割して、その区間と機能を切り替える部分です。これは、私たちのアーキテクチャ上特に重要な意味を持ち、かつ複雑な処理であることから適用箇所としました。
適用方法については、以下のようなステップでVDMを使いました。
まずは、「区間切替」というアーキテクチャを発想したメンバーに、UMLを用いてモデルのラフスケッチを書いてもらいました。ここでのUMLは、後々VDMモデル構築のインプットとなりますので、以下のようにUMLの記法に忠実であることよりも、イメージが通じやすいように書いてもらっています。
そのUMLを受け取った私は、そこからVDMを書いていきます。その際、スクラッチでVDMを記述するのではなく、VDMToolsのUMLリンクという機能を用い、クラス図からVDMモデルのスケルトンを生成し、モデル記述の省力化も図りました。
下の図のように、生成されたスケルトンのVDMモデルは、クラス構造やインスタンス変数、定数や関数/操作のシグネチャまでは書かれていますが、関数/操作の中身、つまり振る舞いの中身については書かれていません。VDMでは、このような概念レベルのモデルを「陰仕様」と呼びます。
その後、UMLのシーケンス図やオブジェクト図を元に、下図のようなモデルの動的側面を記述していきます。この時、UMLに現れていない事前条件・事後条件・不変条件といった制約条件も意識しながら書き進めます。このようなモデルを、VDMでは「陽仕様」と呼びます。先ほどの陰仕様で「is not yet specified」になっていた部分に、アルゴリズムが書かれています。
このVDMモデルで振る舞いを記述していく過程でも、UMLを書いてレビューしただけでは見過す可能性のある以下のような点に気づき、それをアーキテクチャ発想者にフィードバックすることができます。例えば、
上記のような点をフィードバックしつつ、VDMモデルを書き進め、ある程度動作する所まで記述ができたら、続いてVDMのテストケースをユースケース図やオブジェクト図から導出します。
今回の適用箇所の場合は、区間が条件により動的に切り替わり、その際に機能切り替えも起こることを確認したいので、その点を考慮したテストケースをVDMで記述します。
以下では、2つのテストケースが定義されており、それぞれテスト環境をセットした上でロジックを動かし、想定通りの結果になっているかを「assertTrue」にて判定をしています。
VDM++には、CPPUnitやJUnitと同様の構造や機能を持つVDMUnitというテストフレームワークが存在します。VDMにおけるテストを記述し、実行するのに便利であるため、日常的に使っているフレームワークです。今回も使いました。
こうして記述したVDMモデルとVDMUnitのテストケースを、VDMToolsを用いてテスト実行します。これにより、発想したアーキテクチャの実現性と、アーキテクチャ上のロジックが想定通り正しく動作することを、事前に検証することができます。
副産物として、最初にクラス図からVDMを生成しましたが、逆にVDMからクラス図を生成することもできます。ですので私たちは、ここまで検証したVDMモデルから生成したクラス図をモデルシートに掲載しています。
前節で、VDMの使い方と実際の記述を見ていただきました。ETロボコンでは、モデルを記述するだけでは終わらず、そのモデルを審査員に説明するモデルシートを提出する必要があります。本節では、記述したVDMモデルをどのようにモデルシートに表現したかを見ていただきます。
まずは、私たちのモデルシートのうち、構造と振る舞いを説明したページを以下に掲載します。
ご覧いただいて分かると思いますが、VDMの記述が一切出てきません。これが、今年私たちがモデルシートについてこだわったポイントです。VDMのようなテキスト形式の表現を効果的に見せるには、テキスト表現をそのまま見せるだけでは伝わらない、ということです。昨年は、せっかくVDMを使っているので、それを実際に見せるべきであると考え、VDMの記述とUMLのシーケンス図をオーバーラップさせた、以下のようなモデルシートを提出していました。
しかし、審査員に審査をしてもらうというETロボコンの特性上、審査員にどれだけモデルの意図が伝わるかを意識する必要があります。去年の振り返りをしている中でその点が議論になり、部分的なVDMモデルの提示だけでは、モデルの意図が伝わりきらないと考えました。
そのため、今年はVDMの記述は掲載せず、機能や構造や振る舞いの検討を支える背景の技術としてVDMを位置づけました。この方針の元、構造や振る舞いのページにはクラス図・アクティビティ図・シーケンス図といったUML図を掲載しています。ただ、クラス図はVDMのツールであるVDMToolsから自動生成したものを活用したり、テスト済であるVDMモデルの振る舞いからシーケンス図を書いたりすることで、正しさを検証した上でのUML図を記述、生成することを重視しました。
ここまで、私たちがVDMをどのように使ったかをご説明してきました。ここでは、前述のようにVDMを使ったことで、どのようなメリットがあったかをご説明します。
ETロボコンにおいてVDMを使うことのメリットは3つあると考えます。
(1) モデルの早期検証による手戻りの防止
モデルをVDMで記述し、早期に検証することで、実装してみて初めてモデルの不備に気づき、モデルへ手戻りすることを防ぐということです。ETロボコンのロボットは、非常にデバッグし辛いため、実装前に不具合の元を取り除けるのは大きな効果があります。
(2) 単一メディアでの記述によるトレーサビリティの取りやすさ
VDMの場合、VDMという1つの記述メディアで一貫した動的振る舞いを記述することができます。UMLであればシーケンス図やアクティビティ図等を用いて様々なビューで複数の図を記述することになると思います。記述メディアが増えると、その間のトレーサビリティを取るのが難しくなってくるため、単一メディアで記述できることはメリットになります。
(3) モデルシートにおけるモデルの記法正確性向上
クラス図を自動生成することにより、手作業でクラス図を記述することによるクラス図の記法間違いを削減することができます。ETロボコンでは、UMLの記法に対するチェックがかなり厳しいため、単純な記法ミスによる減点を避ける効果は大きいです。
VDMを使うことは、決してメリットだけではなく、課題もあります。ETロボコンにおいてVDMを使う時の課題は2つあると考えます。
(1) チームでVDMを理解する学習コスト
チームでVDMを理解することは、その初期学習コストで課題になると思っていました。しかし、実際にやってみると、そうでもありませんでした。前述した、VDMだけではモデルの全体像がつかみにくい点を、VDMから生成したクラス図を使うことで、全体像を把握することができるようになりました。そして、全体像を把握した上で、VDMの基本的な文法を教えることで、まずは書かれたVDMモデルを読むことは問題なくできるようになりました。ですので、書かれたモデルを見て実装をすることには障壁がなく、少しの初期学習コストを越えてしまえば問題ありませんでした。初期学習コストについても、考えようによってはせっかくETロボコンという技術を試す場において、新しい技術を覚えることは必要な投資だと思います。
(2) モデルシートへの表現が難しい
昨年も今年も、モデルシートを書く時に最も悩むのがVDMの表現の仕方でした。VDMは、モデルを記述する面としては優れていますし、それを検証することもできます。しかし、VDMはテキスト表現であるため、モデルの全体像を簡単に把握することが難しいです。そのため、モデルシートに部分的なVDMコードを掲載したとしても、それが審査員に伝わるのだろうか？という不安がつきまといます。
今年は前述したように、「UMLによってモデルを表現し、その背景としてVDMを使ってモデル記述と検証をしており、またUMLはVDMから自動生成しているため正確である。」ということから、記述と検証の面でVDMを使うことのうれしさを伝えるというシナリオにしました。今年のモデルで、このシナリオ通りに審査員に伝わったかはわかりませんが、現時点でのベストプラクティスだと思っています。
しかし、今年の表現方法で満足しているわけではありませんので、この辺りのどう表現するか？は来年もまた悩むことになるでしょう。
では、このように書いた私たちのモデルシートは、地区大会でどのような審査結果になったのでしょうか。以下が、VDM関連でいただいた審査コメントになります。
良かった点としては、VDMを使ったことの新規性とVDMによって検証されていることから要求が実現されていそうだ、との評価をいただいています。気になった点は、VDM関連ではありませんでした。
この評価をとても素直に捉えると、VDMを用いていることが独自性の評価に繋がっていると読めます。しかし、もう少し冷静かつ客観的に見てみると、VDMを使っていることの良さが審査員に伝わらず、どのように評価したら良いかを迷った末に出した評価のようにも読めます。これは、実際に地区大会の懇親会において、スタッフの方にも同じようなことをご指摘いただいたので、おおよそ合ってる気がします。
最後に、VDMは今回説明した以外にも色々な使い方ができます。そのため、ここで説明した使い方がVDM自体の最適な使い方とは限りません。形式手法と言うと、不具合のないソフトウェアを開発するための魔法の道具のように思われる方もいらっしゃいます。しかし、形式手法もソフトウェア開発する上での道具の一つにすぎませんので、その道具を何を目的にどう使うかが重要だと思っています。
とはいえ、今回ご紹介したVDMの使い方は、課題は色々ありますが、ETロボコンでVDMを使う現時点でのベストプラクティスだと思っています。来年への課題という意味では、今年アーキテクチャの事前検証にVDMを適用しましたが、ロボットの制御部分には使っていません。制御アルゴリズムにVDMを適用した場合、VDMでモデル記述・検証をし、そのモデルから実装、そして走行させて取ったログをモデルにフィードバックするというサイクルを回すことが可能となります。これにより、制御アルゴリズムの構築にリズムが生まれ、効率的かつトレーサビリティを持った開発ができるようになります。
また、今回ご紹介した使い方を発展させて「形式手法をETロボコンで使う」というのであれば、VDMのような記述の手法と、Spinのようなモデル検査の手法を組み合わせると、VDMが持つ記述力に加えて、Spinを用いた状態遷移モデルの網羅的検証が可能となり、より強力な検証をしたモデルを作成することができます。このSpinを使うことに関しては、来年以降PCとBluetooth通信によるやり取りが増えていくであろうこともあり、よりタイミングや割り込みに気をつける必要があることからも言えると思います。
何はともあれ、ETロボコンは「技術の砂場」という側面を持っていますので、形式手法のような普段使わない手法を使ってみると、その手法を小規模で試せて、業務への展開もしやすいと思いますので、ぜひ来年から挑戦してみてはいかがでしょうか？
| © 2011 OGIS-RI Co., Ltd. |
|
