FeliCa ファームウェア (1)

ヒアリング セッション

番号

ヒアリング対象 プロジェクト名称

ヒアリング 対象組織名

ヒアリング

対象者の役割 ヒアリング日 ヒアリング 場所

HS01 FeliCa

ファームウェア(1)

フェリカネットワークス

株式会社 開発責任者 2012/03/30 東京都

4.1.1 プロジェクト特性

工期 2004-2006

要求記述言語 日本語

仕様記述言語 VDM++, FSP, 日本語 設計言語 UML, 日本語

実装言語 C++

開発 日 フェリカネットワークス株式会社 ドメイン 組み込み

4.1.2 プロジェクト概要

FeliCaチップは首都圏のPASMOや全国のJR系各社のICカードに用いられたり、所謂お

財布ケータイの内部に埋め込まれたりして用いられている中核素子である。

本プロジェクトでは初期の IC カード型の FeliCa チップのリリースに引き続き、新たに開 発された移動機用の FeliCa チップ（所謂モバイル FeliCa チップ）の内蔵ファームウェア が開発対象となった。

図4-1に示したものがモバイルFeliCaの全体図である。本プロジェクトで開発対象となっ たモバイル FeliCa チップは、図の左下に水色で示された（モバイル FeliCa IC チップ）

部分である（参考文献17より）。

図4-1: モバイルFeliCa全体図

一種の組み込み機器であることに加えて、一度市場に出回ると回収が困難であること（事 実上不可能）、金銭を扱うため間違いが社会的に大きな責任問題を引き起こすことなどか ら、極めて高い信頼性が要求される部品である。

第一世代（カード）のFeliCaチップは旧来の手法で開発されたものの、第二世代（モバイ ル）の開発に際して、機能の増強に伴い大幅な信頼性向上が求められていた。

プロジェクト本格開始に先立ち、開発リーダーは信頼性向上に関する様々な調査を行い、

有力な手法の 1 つとして形式手法の存在に出会った。いくつか形式手法が存在する中で、

VDM++が採用されたのは以下の理由からである。

• 実機のない仕様策定段階でもアニメーションによる仕様の検証ができる

• 開発上流工程における開発者同士のコミュニケーションと相互理解向上が可能

• 文法を持った言語として記述されていることから、解析が容易で仕様を多方面から 精査できる

• 普通の開発者（特に数学的な訓練を受けていない技術者）でもある程度の努力で使 うことができる

VDM++の採用を検討する際には、大学の形式手法専門家や VDM++コンサルタントの協力

を得て、プロジェクトや開発対象の性質に対して検討が重ねられた。

4.1.3 開発プロセス概要

開発プロセスの全体像をデータフローダイアグラムで記述したものを下図に示す。

図4-2: 開発プロセスの全体像[HS01]

最初の要求は「商品企画（社内）」または「顧客（社外）」からもたらされる。この段階 では表などは用いられるものの完全に日本語のみで記述された未整理の要求記述である。

これらの記述を要求分析することにより、整理された「要求定義」へと展開する。この段 階でも要求は表の形などに整理されているものの、特に厳密な定義がされているわけでは ない。

形式仕様作成が行われるのはこの次の段階である。図中「外部仕様」と書かれた部分が

VDM++で記述された形式仕様の部分である。チップが提供するサービス（API）の仕様を

VDM++で記述し、更に仕様アニメーションを可能にするために、陽仕様⁴が詳細に書き込

まれたものとなっている。

もちろんこの VDM++で記述された「外部仕様」周辺には、全体の目的や構成、機能概要 などを解説した日本語（自然言語）や UML などによる説明が付随している。プロジェク トを構成する主要成果物と形式仕様記述の適用箇所を以下の図に示す（水色の部分が

VDM++による形式仕様適用箇所である）（参考文献19より）。

4 その機能をどのように実現するのかを記述した仕様

図4-3: プロジェクトを構成する主要成果物と仕様記述の適用箇所

このデータフローダイアグラムから読み取れるように、「外部仕様」はプロジェクトの中 心に位置し、様々な用途に用いられている。

「外部仕様」そのものは単体での検証が行われている。ここでは記述された仕様の正当性

の確認(verification)を仕様アニメーションによって仕様記述担当者が確認している。

本格的な検証は、独立した検証チームによって行われている。「外部仕様」をベースにま ず 「 外 部 仕 様 」 そ の も の を テ ス ト す る 評 価 仕 様 を 作 成 し 、 十 分 仕 様 の 妥 当 性 確 認

(validation)を行ってから、同じ評価仕様を設計実装に適用し、仕様の評価結果と比較する

ことにより設計実装の正当性確認(verification)を行っている。

顧客や企画に対して提示するための「仕様説明資料」は形式的に記述された「外部仕様」

をベースに作成されている。元になる記述が形式的に厳密な記述であるため、正確な説明 資料を作成することが容易になり、また作成時の抜け漏れも防ぐ事が可能となる。

設計実装作業に対する直接的な入力としても「外部仕様」は利用される。この場合設計者 に対する極めて厳密な仕様が渡される事になる。本プロジェクトでは設計は人間が仕様を 見ながら行っているが、記述のスタイルが統一され、既に「外部仕様」レベルで検証済の 仕様が渡されることになる。

本プロジェクトでは、評価により問題が生じた場合、それが外部仕様に起因するものであ る場合には全て「外部仕様」の修正として反映されている。こうした開発プロセス上の規 約により、常に最新状態の「仕様」がプロジェクトの成果物として反映され、多数の評価 仕様を用いた回帰検証もそのたびに行われたため、製品の高い品質保持が可能となった。

4.1.4 開発体制

開発に際しては3つのチームが結成された 仕様チーム

設計チーム 評価チーム

の3チームである。以下の表にそれぞれのチームの役割を簡単にまとめた。

表4-1: 各チームの役割

チーム 役割

仕様チーム 要求と概要仕様を受け取り、形式仕様として記述する。個別の 仕様毎のアニメーションを行い、単体レベルでの検証を行う。単 体レベルでの検証が終わった仕様を、開発チームと評価チーム へ同時にリリースする。開発チームからは実装上の制約情報を 受け取り、評価チームからは仕様に対する精査結果（仕様の評 価）を受け取る。

開発チーム 仕様チームから形式仕様を受け取り、設計と実装を行う。実装 プラットフォームが複数あるため、実際にはこのチームは複数存 在する。設計上の制約から実現できない仕様がある場合には仕 様チームへフィードバックを行う。成果物を評価チームに提示 し、評価結果を待つ。

評価チーム 仕様チームから仕様を受け取ると、まず評価仕様の評価を行 い、評価仕様自体の品質を確保したあと、外部仕様全体をアニ メーションによって検証する。プロダクションレベルの回帰アニ メーションを行い、仕様上の不備が見つかった場合には仕様 チームへフィードバックを行う。

開発チームからは設計情報と実装を受け取り、評価を行う。この とき用いられる評価仕様は検証済のものである。

これら 3 つのチームの関係を以下に図示する。チーム間に描かれた矢印は主要な提示物で ある。

図4-4: チーム間の関係

4.1.5 記述と支援ツール

このプロジェクトで形式手法に関連して用いられた言語と主なツールを以下に挙げる。

表4-2: 使用された言語と主なツール

言語 ツール 適用内容

VDM++ VDMTools 構文検査、型検査、仕様アニメーション

FSP LTSA モデル検査により設計の一部の安全性確認

自家製テストス クリプト

自家製ツール テストケース記述言語を用いて、仕様(VDM++) と実装(C++)の両者を駆動。このテストケース記 述言語は既存のプロジェクトでも利用されてい てテストケースの資産が存在していた

VDMTools はインタプリタ方式で仕様アニメーションを支援する。このため記述や必要と

するデータが大規模になるに従い、実行速度の低下などが課題になったが、幸いなことに

VDM++コンサルタントならびに VDMTools⁵ベンダの協力により、ツールに対する様々な

改良が適宜行われた。実行速度の改善は仕様アニメーションを用いた回帰テストの実行時 間を1桁以上短縮し、より多量の評価仕様を適用することが可能になった。

4.1.6 厳密な仕様記述の効果

(1) 仕様の妥当性確認(validation)作業の早期化

VDM++による仕様アニメーションが可能な形にしていたため、外部仕様の評価仕様を直接

評価してその結果を確認することが可能となった。このため新しい仕様が追加された際に もそのテストシナリオを反映した評価仕様を作成し、設計する前に仕様レベルでの確認を 行うことができたので、仕様の妥当性確認を早い段階で行う事が可能になった。

特に最初の段階では、実チップは勿論、評価ボードなども存在しない段階であるため、仕 様記述のみで記述と評価を行う事ができたことは価値が高い。

(2) 仕様説明資料作成の簡便化

外部に対して仕様を説明する際には、形式仕様記述そのものではなく、そこから半自動的 に作成する形で、日本語やUMLなどの図版などが用意された。

こうした資料の作成時には、誤りや抜け等が混入しやすいものであるが、形式記述を元に 作成する場合にはそうした間違いが混入しにくいという効果が期待される。実際、細かい 定義部分等の文書は自動生成の対象となったため精度が高いものとなった。