F/W 実装モデルの作成と検査

F/W 設計書と実装コードから抽出した通信 I/F の F/W 実装モデルと, H/W 制約条 件付き実装モデルとを並列合成した. そして,並列合成後のモデルに対して安全性検証と 活性検証を行った. これにより, F/W 実装コードがH/W の制約条件を満たしているこ とを確認した.

表6.2 および 図6.5 において, F/W実装モデルはM_{F W} として表した. また, H/W 制 約条件付き実装モデルは M と表した. 6.5.2節において述べたように, H/W 制約条

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

件付き実装モデル MHW C は H/W 実装モデル (MHW) と H/W 制約条件のプロパティ (PHW) を並列合成したプロセスである. H/W 制約条件付き実装モデル MHW C を次に 示す.

M_{HW C} =M_HW∥P_HW

ここで, 本節で述べる F/W 実装モデルを M_{F W} という記号を用いて表す. F/W 実装 モデルと H/W 制約条件付き実装モデルとを並列合成した結果は, H/W 設計を満たす F/W実装モデルである. これをM_{F W VHW} という記号を用いて表す. M_{F W VHW} は次のよ うに表すことができる.

M_{F W VHW} = M_{F W}∥M_HW∥P_HW

H/W制約条件付き H/W実装モデルと F/W 実装モデルの並列合成は, 状態数が増え たため行うことができなかった. そこで, 状態数を減らすために, 各 H/W モジュールと F/W実装モデルで共有していないアクションを内部アクションとすることで, LTSA の 最小化機能を使用した.

最小化機能は弱双模倣等価の概念を適用しており, これにより仕様間の無矛盾性を検 証しながら状態数を減らすことができる ^[MK06] . 弱双模倣等価を含む観測等価とは, 外 部観測上区別不可能なプロセスを同一とみなすことである.

LTSA の最小化機能を使用するには, 隠蔽演算子 (\) および, インタフェース演算子 (@)を用いる. 例えば,次に示す P1プロセスとP2プロセス について, P1は aアクショ ンとc アクションを隠蔽して b アクションと d アクションのみを公開したプロセスで あり, P2 は b アクションと d アクションのみをインタフェースとして用いることを示 している. その結果, P1 プロセスも P2プロセスも同じ状態遷移となる.

P1 = (a -> b -> c -> d -> P1)

\{a, c}.

P2 = (a -> b -> c -> d -> P2)

@{b, d}.

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

6.5. ステップ 2の実施内容と結果・考察 129

P ^{tau b tau}

0 1 2 3

d

図6.6 FSP の隠蔽演算子およびインタフェース演算子を用いた LTS

図6.7 モデルのコンポーネント化と階層構造

P1プロセス, P2プロセスのLTSを図6.6に示す. tauは隠蔽したアクションであり,他 のプロセスと共有しないことを示している.

この最小化機能を用いて, H/Wモジュール内部でのみ共有している, F/Wには非公開 のアクションを隠蔽することで, 状態数を削減した. 以下では, LTSAの最小化機能を用 いる際に,検査内容に従って隠蔽するアクションを選択する方法について述べる. 図6.7 はステップ 2 のモデルを簡略化した構造図である. H/W 実装モデルは複数のレジスタ のプロセスを並列合成したものである. 各 H/W 実装モデルは, F/W 実装モデルと共有 しているアクションおよび, H/W モジュール内のレジスタ間でのみ共有している内部ア クションを持つ.

H/W 実装モデルとF/W 実装モデルとを並列合成する場合には,内部アクションであ る iAB1 アクションとiCD1アクションを隠蔽することで状態数を減らすことができる. iAB1 アクションは, H/Wモジュールの内部で共有しているため internal を表すi を接

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

頭辞とし, また Register A と Register B とで共有しているため iAB と命名した. 他の H/W モジュール内部で共有しているアクションも同様である. Register A のプロセス

を P Reg A とする. 他のレジスタも同様の命名規則とした. F/W 実装モデルを M FW

とすると, この例における H/W実装モデルと F/W 実装モデルの並列合成において, 最 小化機能を利用するためのFSP 記述は次のようになる.

|| MIN_HW_FW_Example = (

P_Reg_A || P_Reg_B || P_Reg_C || P_Reg_D || M_FW )\{iAB1, iCD1}.

また, fD2 のような F/W 実装モデルからは使用していない H/W 実装モデルの公開ア クションは, 実行不可にしておく必要がある.

このように, 複数のプロセスをコンポーネントとしてまとめ, 階層構造をとることで, 最小化機能を有効的に利用することができる.