インタビュー

第2回「形式仕様記述手法の導入」(倉員桂一 氏 / フェリカネットワークス株式会社 取締役副社長)

2007.12.25

倉員桂一 氏 / フェリカネットワークス株式会社 取締役副社長

「日本発の技術 進化するICカードと携帯の融合」

倉員桂一 氏
倉員桂一 氏

非接触ICカードを組み込んだ携帯端末が、交通、通信に限らず買い物その他、日常生活のありようを大きく変えようとしている。何枚もの各種カードのみならず、小銭すら持ち歩かなくても済む。そんな時代を可能にした基本技術である携帯端末向け非接触ICカード技術方式「モバイルFeliCa」の開発とその応用に取り組んでいる倉員桂一・フェリカネットワークス株式会社取締役副社長に、モバイルFeliCa技術開発の経緯、応用の現状、さらにはICカードと携帯機能の融合がどこまで進化するかの見通しなどについて聞いた。

―モバイル FeliCa IC チップファームウェアの開発にあたり、どのような工夫をしていますか?

ソフトウェアの開発において、いわゆる「銀の弾丸」はありません。社外の協力を得ながら、要件獲得、仕様開発、設計、実装、テストなどの各開発工程においてさまざまな工学的工夫をするとともに、公的第三者評価の依頼やプロジェクトマネジメント、チームビルディングといった取り組みも行っています。文字通り「産官学連携」して開発に取り組んでいます。例えば、仕様開発工程では、形式仕様記述手法の適用、テスト工程では、ブラックボックステスト項目を効率的に列挙するためにAll Pair 法の適用などを行っています。

ソフトウェアの開発現場では、あいまいな仕様に起因するトラブルが多いのです。また、一般に下流工程の修正コストは、上流工程よりも大きくなります。近年、ソフトウェア開発の上流工程における、要件や仕様の品質を確保するための形式手法が注目されています。

形式手法は、システム、特にソフトウェア開発の手法で、数理論理学に基づく科学的な裏付けを持つ言語を用いて設計対象を表現することで、ある側面の仕様を厳密に記述し、開発工程で利用する手段の総称です。手法の利用により、設計対象を表現し、設計記述の正しさを系統的に示すことが可能になります。形式的な記述を行うことであいまいさが取り除かれ、機械処理が可能になり、さまざまな可能性が開けるのです。

形式手法の中で、モバイル FeliCa IC チップファームウェアの仕様開発に適用したのは、モデル規範型の形式仕様記述と、一部仕様の振る舞い仕様のモデル検査です。モデル規範型の形式仕様記述とは、集合論や命題論理、述語論理を基礎として、不変条件、事前条件、事後条件を仕様として記述することで、情報の構造や、ある状態から他の状態への変化をモデル化する手法のことです。専用言語の利用によるコンパクトな仕様記述、あいまいさの除去、仕様の実行、テスト、回帰テスト、定理証明などの可能性が広がります。一方のモデル検査とは、振る舞い仕様を、状態遷移モデルと、モデルが満たす条件として記述することで、全状態空間を生成し自動検査することです。これにより従来のテストでは見つからない障害を発見できる可能性が広がります。

国内では多くの適用事例がありませんでしたが、今回、モバイル FeliCa ICチップファームウェアの品質確保に対する社会的責任をかんがみ、導入に踏み切りました。

―形式仕様記述手法の導入により、どのような効果があったのでしょう?

上流工程、特に仕様策定工程における成果物の品質向上に効果がありました。今回のプロジェクトの場合、仕様のデバッグ工程における不具合はほとんどありませんでした。また、要件獲得、仕様開発、実装、テストのイテレーションを多数回しても、変更によるノイズが増幅されず、仕様を洗練することができました。さらに、形式手法はプロジェクト内のコミュニケーションの活性化にも寄与します。しかし、先程述べたようにソフトウェアの開発において「銀の弾丸」はありません。開発ドメインに応じて、他の手法を組み合わせることが肝要です。形式手法も、他の工夫と組み合わせることにより効果を発揮するのです。

―教訓や反省点といったものはありますか?

仕様を形式的に記述・検証できることと、要件が定まっていることを混同しないことが重要です。また、形式仕様記述手法の適用に際しては、開発のプロセス全体を見直す必要があります。厳密な仕様記述・検証には時間がかかります。トップマネジメントの理解が不可欠です。

さらに、導入には経験豊富な専門家の助言が必要です。私たちの場合、九州大学の荒木啓二郎教授にお世話になりました荒木教授の指導がなければ、私たちの手法適用は実現できませんでした。さらに、教授に社外発表の機会も数多くいただき、社外から有益なフィードバックも得られました。

モバイルFeliCaが関心を集めた世界最大のカードショー「CARTES 2007」
(11月、パリ)
モバイルFeliCaが関心を集めた世界最大のカードショー「CARTES 2007」
(11月、パリ)
「CARTES 2007」のモバイルFeliCa講演会場風景
「CARTES 2007」のモバイルFeliCa講演会場風景

(続く)

倉員桂一 氏
(くらかず けいいち)
倉員桂一 氏
(くらかず けいいち)

倉員桂一(くらかず けいいち)氏のプロフィール
1957年茨城生まれ、81年東京大学工学部卒、日立製作所入社、94年半導体事業部マイコン設計部 SH マイコン第一 Grリーダ、02年半導体グループマイコンビジネスユニットIC カード本部長、03年 IT 戦略統括部エグゼクティブ、04年から現職。91年プリンストン大学電子工学研究科修士課程修了、07年先端技術ベースの経営戦略に関する研究で高千穂大学から博士(経営学)を取得。

ページトップへ