UMLと形式手法のハイブリッド仕様が鍵となるか

新しい設計技術とその解説
〜適用技術の紹介〜

　本部審査員の中嶋 栄治氏と鄭 顕志氏からは、「方法論」「メカ制御モデリング」「UML以外のモデリング技術」という3つの視点で注目したというモデルが紹介された。

　まず方法論の観点では、ETロボコンでも数年前から出てきたSPL（Software Product Line）を用い、部品化による再利用を適用したチームとしてプッシュ☆スタート2（デンソー）、BricRobot09（富士通コンピュータテクノロジーズ）、BERMUDA（富士通コンピュータテクノロジーズ）、くろしお（個人）のモデルが紹介された。上記3チームはRCXとNXTという制御方法が異なる2つのロボットで共通可能な部品を個別部品で構成し、くろしおについては、RCXからNXTへ移行する過程で、SPLを適用していたという。

プッシュ☆スタート2のモデル 共通部分と差分を表記し、制御方式に違いを表している	SPLについて プロダクトライン・フレームワークとは、基本的な活動と、プロティクスのエリアがあり、図ではコア資産を作ってベースとなるコンポーネントを作るものと、商品（対象）となるもの（今回であれば、RCX用、NXT用を作ること）を示している。両製品の差分になる部分、共通部分をどちらで作るかをマネジメントする

　中嶋氏は「今回、SPLを用いたチームはすべてが上図のような考え方に基づいているわけではなく、良いところを使って、効率的かつ品質良く作って、ロボコンで勝ち抜こうという意図があると読み取れた」とコメントした。

　メカ制御システムのモデリングの観点では、サヌックのモデルが紹介された。サヌックのモデルからは「メカトロニクスはアナログの世界、ソフトウェアはデジタルの世界。メカ制御というのは、その両方をつないでいかなければならない。我われはそれを表現した」という意図が一貫して読み取れたという。

サヌックのモデル アナログを連続系、デジタルを離散系とし、それらを組み合わせたシステムを作成

　「基本的にメカは物理法則に沿って動いているため、それをソフトウェアでどう制御するかは、非常に大切。知らない人からすれば、結構はっとする内容になのでは」（中嶋氏）

　UML以外のモデリング技術としては、SysMLを適用したひものエンベダーズ（沼津工業高等専門学校）、サヌック、田町レーシング（オージス総研）、そしてVDMを適用したVienna Line Tracer Club（個人、関西地区大会特別賞チーム）、O・I・SA（福岡CSK、九州地区大会チーム）、s-Spot（国立情報学研究所 、東京地区大会チーム）のモデルが紹介された。SysMLに関してはひものエンべダースとサヌックが要求図で、田町レーシングがパラメトリック図でそれぞれ適用している。

田町レーシングのモデル コード変化の検知をするためにどういうパラメータがあり、演算をすると、その結果が範囲が出せるかというのを記載している	SysMLの概要 SysMLは、できるだけUMLを流用して、定義されている

モデリング言語 SysMLを概観する（1/2） − ＠IT MONOist via kwout

　鄭氏からはVDM（形式手法）について、次のように解説された。

　「VDMとは、数理論理学などに基づいて品質の高いソフトウェアを効率良く開発するための科学的・系統的アプローチのこと。何をするかというと、システムの注目する側面を正確かつ、あいまいさのない言語で表現する。UMLは確かにソフトウェアのある側面をモデリングする言語で、人と人とがコミュニケーションする際に向いている。ただし、UMLでモデルを書いたときに、書いたモデルが正しく書けているか、仕様に準拠しているモデルが書けているかをチェックするときはどうなるか。おそらくはモデルを見てみんなで議論をする。そこでモデルが間違ってそうだ、とか、合ってそうだ、というのを判断する」（鄭氏）

　「うまくいった／いかなかったかは実際にコーディングしてプログラムを走らせてみて分かる。そこでもし設計に間違いがあれば、その段階からまた設計をし直す。つまり実装段階にあるため、設計が正しかったかどうかを厳密に判断できない。その問題を解決するための1つの手法が、形式手法と呼ばれるもの。モデル化した段階で、特定の論理数理学という学術的背景を元に作られた言語でモデル化している。どんなメリットがあるかというと、仕様の段階で仕様の性質を定義し、その性質を仕様が満たしているかどうかをチェックできる」（鄭氏）

　「形式手法は、仕様の正しさを厳密にチェックするには良いが、書いてある仕様の可読性の問題や、あるいはUMLと比べてはどうか。モデル審査員の観点からすると、正しいモデルを書いていることも大事だが、それに対する分かりやすさ、理解性の観点から見ると、形式手法だけを使ってモデル化したとしてもだめで、うまくUMLで作られている分かりやすい・見やすいポイントを組み合わせると、より良いモデルになるのではないだろうか。そういう意味で、UMLと形式手法。両方の良さをハブリッドで使うのも1つの考え方ではないかと見ている」（鄭氏）

いまさら聞けない 形式手法入門（1/3）− ＠IT MONOist via kwout

関連記事：
	連載記事「誰でも使える形式手法」 http://monoist.atmarkit.co.jp/fembedded/index/formalmethod.html

　最後に中嶋氏と鄭氏は、「モデリング技術は本日紹介した以外にも複数ある。何が課題なのかを見極め、その課題を解決するために適した技法／手法を選び、モデリング技術を楽しみながら挑戦してほしい」と述べた。

◇

　次回は性能面での今年のトレンド、必勝法を紹介します。

ETロボコン2009公式ホームページはこちらへ