• 検索結果がありません。

ステップ 1 とステップ 2 の検証範囲

ドキュメント内 九州大学学術情報リポジトリ (ページ 125-129)

第 6 章 動的な振る舞いに関するモデル検査の適用 111

6.3 ステップ 1 とステップ 2 の検証範囲

CardMode

powerOn resetMode

resetMode

chgParmMode0

initCardMode1 chgParmMode1

chgParmMode1 chgParmMode0

0 1 2 3 4 5

powerOff

powerOff

resetMode

powerOff

resetMode

powerOff

resetMode

powerOff

initCardMode1

図6.1 簡易化したカード機能の LTS

プロセスに遷移し, powerOff アクションにより番号 0 の PowerOff プロセスに遷移して いる.

6.3 ステップ 1 とステップ 2 の検証範囲

本節では, ステップ 1 とステップ 2 の検証範囲について, 検査対象の静的な構造を表 現することができる「構造図 (structure diagrams) 」[MK06]を用いて説明する.

モバイルFeliCa IC チップの検査対象の構造図を図6.2に示す. 構造図は, 複数のプロ

セスとプロセス間で共有するアクションを図示したものである. プロセスとは,一つの逐 次プログラムの実行のことであり, 有限状態機械を用いて表現することができる. 有限 状態機械は, 状態とアクションから構成される. ここでは,一つのアクションが実行中に 他のアクションが割り込むことはできないものとする. 構造図において, 各プロセスは長 方形で表し,境界線上の円は公開しているアクションを図示している. 公開しているアク ション同士を接続している線はプロセス間でアクションを共有していることを示す.

図6.2 において図示している内容は,検査対象のモバイル FeliCa ICチップと, 外部環

116 第 6 章 動的な振る舞いに関するモデル検査の適用

図6.2 モバイル FeliCa IC チップの構造図

境に分類することができる. 外部環境とは, 物理的に検査対象の外側に位置しているも のである. 図の S1 で囲った範囲はステップ 1 の検証対象を表し, S2, S2 EXTで囲った 範囲はステップ 2の検証対象を表している. S1 と S2 は検査対象のモバイル FeliCa IC チップのプロセスであり, S2 EXT は外部環境のプロセスである. EXT は externalの略 称として用いた.

モバイル FeliCa IC チップは, 電子マネーの残高情報を保持するようなカード機能と,

店舗のレジ端末にあるリーダ・ライタのようなリーダ・ライタ機能を備えている. また, リーダ・ライタからモバイルFeliCa IC チップにアクセスすることができる無線通信イ ンタフェース機能に加え,携帯端末側からモバイル FeliCa ICチップにアクセスすること ができる有線通信インタフェース機能を備えている. これらの機能を実現するために, モ バイルFeliCa ICチップは 図6.2に示した構造を持っている. 以下では,図6.2に示した 各プロセスについて説明する. 記載を簡略にするためにハードウェアを H/Wと,ファー ムウェアを F/W, 通信インタフェースを通信 I/Fという略称で記載することにする.

まず, S1 の範囲にあるモバイル FeliCa IC チップのプロセスは次のようになる. F/W コマンドインタプリタ カード機能

九州大学大学院 システム情報科学府 情報工学専攻

6.3. ステップ 1 とステップ 2 の検証範囲 117

カード機能のコマンドを解釈するプロセスである. F/W コマンドインタプリタ リーダ・ライタ機能

リーダ・ライタ機能のコマンドを解釈するプロセスである.

次に, S2 EXT の範囲にある外部環境のプロセスの説明を次に示す.

携帯電話コントローラ

携帯端末からモバイル FeliCa IC チップの有線通信インタフェース機能を使用し てモバイル FeliCa IC チップ内のデータを読み書きするプロセスである.

外部リーダ・ライタ

店舗のレジ端末にあるようなリーダ・ライタのプロセスである. モバイル FeliCa IC チップの無線通信インタフェース機能を使用してモバイル FeliCa ICチップ内 のデータを読み書きするプロセスである.

外部モバイル FeliCa IC チップ

検査対象とは別のモバイル FeliCa IC チップのプロセスである. 検査対象のモバイ

ル FeliCa ICチップがリーダ・ライタとして機能する場合に, 読み書き対象とする

カード機能のプロセスである.

モバイル FeliCa ICチップと外部環境において共有するアクションの例として,携帯端末

の画面にモバイル FeliCa ICチップ内に保持している電子マネーの残高情報を表示する 場合を説明する. 「携帯電話コントローラ」はモバイル FeliCa IC チップに電子マネー の残高確認を行うアクションを送信し, モバイル FeliCa IC チップは残高情報を「携帯 電話コントローラ」に送信することにより実現する.

最後に, S2 で囲んだプロセスについて説明する. S2 で囲んだプロセスは, モバイル

FeliCa IC チップの H/W モジュールと F/W モジュールの構造を表している. 以下に

S2の各プロセスについて説明する. H/W 有線通信 I/F モジュール

有線通信 I/F 機能を実現する H/W モジュールのプロセスである. 受信開始や受

118 第 6 章 動的な振る舞いに関するモデル検査の適用

信中, 受信完了割り込み, 送信開始,送信中, 送信完了割り込みなどのアクションを 他のプロセスと共有する.

H/W 無線通信 I/F モジュール

無線通信 I/F機能を実現する H/Wモジュールのプロセスである. H/W有線通信 I/F モジュールと同様に受信開始や受信中, 受信完了, 送信開始,送信中, 送信完了 割り込みなどのアクションを他のプロセスと共有する.

H/W タイマモジュール

時間を計測する H/W モジュールのプロセスである. タイムアウト値設定, タイマ 開始, タイムアウト割り込みなどのアクションを他のプロセスと共有する.

F/W 通信 I/F コントローラ

「 F/W コマンドインタプリタ カード機能」および「 F/W コマンドインタプリ タ リーダ・ライタ機能」からの指示により,「 H/W有線通信 I/Fモジュール」と

「 H/W 無線通信 I/F モジュール」の排他制御などの管理を行うプロセスである. 例えば, 「 H/W 有線通信 I/F モジュール」においてデータを受信中に, 「 H/W 無線通信 I/F モジュール」からデータを受信しないような制御を行っている. 以上が, 検査対象とする, モバイルFeliCa IC チップと外部環境の構成である.

ステップ1 の検証対象は, S1 で示したコマンドインタプリタである. コマンドインタ プリタには, カード機能とリーダ・ライタ機能があり, 各機能は並列に動作する. ステッ プ 1 では, 記述範囲を仕様書が規定する両機能の状態遷移とした. ステップ 2 の検証対 象は, S2で示した2つの通信I/Fを制御しているH/Wモジュールと,「 F/W通信I/F コントローラ」である. ステップ 2 の検証において, S2 EXT で示したプロセスを外部 環境モデルとして記述した.

上記の通り,モバイルFeliCa ICチップは,外部環境も含め同時並行に動作するプロセ スを制御する特徴があり, 仕様・設計ともに,複数のプロセスに関する厳密なモデルが必 要である. 以下,ステップ 1とステップ 2におけるモデルやプロパティの作成方法,安全 性と活性の検証結果, 考察について述べる.

九州大学大学院 システム情報科学府 情報工学専攻

6.4. ステップ 1の実施内容と結果・考察 119

ドキュメント内 九州大学学術情報リポジトリ (ページ 125-129)