コンテキストベース・プロダクトライン開発とVDM++の適用 ＳＥＳ２００６ コンテキストベース・プロダクトライン開発とVDM++の適用 鵜林 尚靖 （九州工業大学） 金川 太俊 （九州工業大学） 瀬戸 敏喜 （九州工業大学） 中島 震 （国立情報学研究所） 平山 雅之 （ＳＥＣ） ２００６年１０月２０日

発表内容 研究の背景と目的 コンテキストを考慮したプロダクトライン VDM++による仕様記述と妥当性確認 考察と関連研究 まとめ

１．研究の背景と目的

組込みシステムの特徴 コンテキストの存在：　組込みシステムはハードウェアを通じて外部環境に影響を及ぼす。また同時に、組込みシステムは外部環境からも影響を受ける。 プロダクトライン型の開発：　あるプロダクトファミリで共通に利用可能なアーキテクチャやコンポーネント群を資産としてあらかじめ用意し、個々のプロダクトは資産を合成して開発する。

現状の課題 －電気ポットを例に ポット内の水を沸騰させる ヒータのOn/Offによって水温を制御する 現状の課題　－電気ポットを例に サーミスタ 水 水位センサー ヒータ ポット内の水を沸騰させる ヒータのOn/Offによって水温を制御する 水温が100度に達すると、保温状態に移行する 水位センサーにより水量を観測する

プロダクトラインに基づいた 仕様策定プロセスの典型例 ステップ１ フィーチャ分析 ステップ２ SW仕様策定 電気ポット Boil: () ==> () Boil() == while thermistor.GetTemperature() <= 100.0 do heater.On(); SW HW コントローラ ヒータ サーミスタ 水位 センサー 水位 メータ SW仕様は正しい？ 必須フィーチャ オプション・フィーチャ

実は、仕様が正しいかどうかは相対的  コンテキストに依存 実は、仕様が正しいかどうかは相対的 　　コンテキストに依存 このSW仕様は「通常気圧(１気圧)の環境下で水を沸騰させる」場合には正しい仕様である。 しかし、想定しているコンテキストが変更になると、SW仕様が仮定するコンテキストと実際のコンテキストとの間にズレが生じ、最終的なシステム上の欠陥につながる。 例： 「低気圧(1気圧未満) の環境下で水を沸騰させる」場合(気圧の低い山頂での利用など)

現状の課題 仕様の再利用性が低い: 特定のコンテキストを仮定し、そのためのロジックを決めてしまうことが多く、仕様を再利用することが難しい。 システムの保守・発展がアドホック的: 想定するコンテキストが変わるたびに仕様を見直すが、その対応が場当たり的。 仕様の妥当性確認が困難: 上記２点の結果として、システムとコンテキストの間に生じる不整合や欠陥を見落とす可能性が高くなる。

本研究のアプローチ プロダクトラインをシステムラインとコンテキストラインに分け、各々フィーチャ分析を行う。 システムラインを構成するハードウェアおよびソフトウェア仕様、コンテキストラインを構成するコンテキスト仕様が資産になる。 仕様記述に形式手法（今回はVDM++）を適用する。妥当性確認はVDM++のテスト実行により行う。

２．コンテキストを考慮したプロダクトライン

プロダクトラインの構成 システムの フィーチャ分析 コンテキストの フィーチャ分析 電気ポット 現実世界 気圧 液体 SW HW コントローラ ヒータ サーミスタ 水位 センサー 水位 メータ 高い 通常 低い 水 ミルク 必須フィーチャ オプション・フィーチャ 相互排他的フィーチャ

プロダクトライン開発の手順 コア資産 管理 プロダクト 開発プロセス プロセス 開発プロセス コンテキスト資産の開発： 　コンテキストのフィーチャ分析、仕様資産の開発を行う システム資産の開発: ハードウェアとソフトウェアのフィーチャ分析、仕様資産の開発を行う 想定コンテキストの定義: 　コンテキスト資産群からプロダクトが想定する仕様資産を選択する プロダクト構成の定義: 　システム資産群からプロダクトを構成する仕様資産を選択する 仕様の妥当性確認: 　ハードウェア、ソフトウェア、コンテキストの各仕様を組み合わせた結果に不整合がないか否かを確かめる ＶＤＭ＋＋ による テスト実行

３．VDM++による仕様記述と妥当性確認

ＶＤＭ＋＋と支援ツール VDM++はVDM-SL (The Vienna Development Method – Specification Language）のオブジェクト指向拡張。 厳密なモデル化を目的とした仕様記述言語。 VDM++ Toolbox： VDM++のための開発環境。仕様の構文･型チェック、証明課題生成、インタープリタ等の機能をもつ。

VDM++仕様の プロダクトラインへの割当て 電気ポット (USER-test.vpp) システムの フィーチャ分析 コンテキストの フィーチャ分析 SW HW 現実世界 (REALWORLD.vpp) コントローラ (SYSTEM-SW -controller.vpp) ヒータ (SYSTEM -HW -heater.vpp) サーミスタ (SYSTEM -HW -thermistor.vpp) 水位センサ (SYSTEM -HW -liquid -level -sensor.vpp) 気圧 (CONTEXT-atmospheric -air-pressureplace.vpp) 液体 (CONTEXT-liquid.vpp) 高い 通常 低い 水 ミルク (CONTEXT-atmospheric-air-pressureplace-high.vpp CONTEXT-atmospheric-air-pressureplace-normal.vpp CONTEXT-atmospheric-air-pressureplace-low.vpp) (CONTEXT-liquid-water.vpp)

VDM++による仕様記述

プロダクトラインからの構成要素の選択 電気ポット システムの フィーチャ分析 コンテキストの フィーチャ分析 SW HW 現実世界 (USER-test.vpp) システムの フィーチャ分析 コンテキストの フィーチャ分析 SW HW 現実世界 (REALWORLD.vpp) コントローラ (SYSTEM-SW -controller.vpp) ヒータ (SYSTEM -HW -heater.vpp) サーミスタ (SYSTEM -HW -thermistor.vpp) 水位センサ (SYSTEM -HW -liquid -level -sensor.vpp) 気圧 (CONTEXT-atmospheric -air-pressureplace.vpp) 液体 (CONTEXT-liquid.vpp) 高い 通常 低い 水 ミルク (CONTEXT-atmospheric-air-pressureplace-high.vpp CONTEXT-atmospheric-air-pressureplace-normal.vpp CONTEXT-atmospheric-air-pressureplace-low.vpp) (CONTEXT-liquid-water.vpp)

仕様の妥当性確認 電気ポットの仕様の妥当性をVDM++インタプリタのテスト実行により確認する コンテキスト仕様A システム 仕様 コンテキスト仕様A 通常気圧(１気圧)の環境下で水を沸騰 CONTEXT-atmospheric-air-pressureplace-normalと CONTEXT-liquid-waterが選択 コンテキスト仕様B 低気圧(1 気圧未満) の環境下で水を沸騰 CONTEXT-atmospheric-air-pressureplace-lowとCONTEXT-liquid-water

システム仕様 SYSTEM-SW-controller.vpp ポット中の水が無くなる ことがないことを 制約条件とする class Software instance variables heater : Heater; thermistor : Thermistor; liquid_level_sensor : LiquidLevelSensor; operations public Setup: RealWorld ==> () Setup(realworld) == (heater := new Heater(); heater.Setup(realworld); thermistor := new Thermistor(); thermistor.Setup(realworld); liquid_level_sensor := new LiquidLevelSensor(); liquid_level_sensor.Setup(realworld); ); public Boil: () ==> () Boil() == while thermistor.GetTemperature() <= 100.0 and liquid_level_sensor.IsOn() = true do heater.On() pre liquid_level_sensor.IsOn() = true post liquid_level_sensor.IsOn() = true; end Software ポット中の水が無くなる ことがないことを 制約条件とする

テスト実行結果（コンテキストA） 正常

テスト実行結果（コンテキストB） 事後条件違反 （沸騰し続け、水がなくなる）

妥当性確認後の対応 システムとしてどのような仕様にすべきか（ハードウェアを追加すべきか、或いはソフトウェアで頑張るべきか）、その妥当性を調べることが可能となる。 コンテキストBに対応するには、沸点(気圧により変化)に応じた加温操作が必要となるため、気圧センサーが必須となる。 上流段階で、仕様の妥当性、仕様策定の戦略が明確になる

４．考察と関連研究

開発プロセスのあり方 UMLモデルをVDM++モデルに変換する VDM++モデルに、事前条件、事後条件、不変条件を追加し、仕様を厳密化する。 テスト実行による仕様の妥当性を確認する。 VDM++モデルをJavaコードに変換する。その際、事前条件、事後条件、不変条件をJMLに変換する ESC/Java2等のJMLツールを用いて、事前条件、事後条件、不変条件を検証する。これにより、VDM++モデルがJavaコードに正確に洗練(Refinement)されているかが検証される。 モデリング 事前条件・事後条件・不変条件 実装

陽関数と陰関数 仕様を陽関数として記述するとインタプリタによるテスト実行が可能になるが、その反面、仕様と実装の差異が曖昧になる。 仕様記述という意味では陰関数を用いる方が望ましいが、逆にテスト実行できないため妥当性を確認するのが難しくなる。この場合、証明支援ツールを用いて仕様を検証する必要がある。

陽関数と陰関数（我々の見解） 仕様記述において重要なのは不変条件などの制約条件を特定化すること。 一般に不変条件は抽出するのが難しく、テスト実行しながら見つけていくことは有効。そのため、本研究では仕様を陽関数で記述する方式を採用。 しかし、制約条件を洗い出し、その妥当性を確認した後は関数本体は必ずしも必要でない。VDM++によるモデル化は制約条件を洗い出すための工程とみなすこともできる。

アスペクト指向の導入 沸点を考慮したシステムを構築するには 横断的関心事 AspectVDM

関連研究 問題フレーム［M.Jackson, 2001]: 機械(システム)と現実世界(コンテキスト)の関連をモデル化。 KobrA［Atkinson et al., 2001］：　プロダクトライン開発手法の一つ。KobrA のコンテキストはシステム対象内の問題領域をシステム外と同時に捉える。 ESIM法[三瀬 他, 2005]:　非正常系の分析。 外部環境分析法[鷲見 他, 2005]:　外部環境分析の手順化。

関連研究（形式手法） Feature Algebra [P.Hofner, et al. FM’06]

５．まとめ

まとめ 外部環境などのコンテキストを考慮した組込みシステムの仕様記述とその妥当性確認方法をプロダクトライン開発の観点から提案した。 通常のビジネスシステムに対しても本手法は適用可能。 安全、安心なシステム構築にはコンテキストの視点が今後ますます重要になってくる。