SES2006 コンテキストベース・プロダクトライン開発と VDM++の適用 鵜林 金川 瀬戸 中島 平山 尚靖 太俊 敏喜 震 雅之 (九州工業大学) (九州工業大学) (九州工業大学) (国立情報学研究所) (SEC) 2006年10月20日 1 発表内容 1. 2. 3. 4. 5. 研究の背景と目的 コンテキストを考慮したプロダクトライン VDM++による仕様記述と妥当性確認 考察と関連研究 まとめ 2 1.研究の背景と目的 3 組込みシステムの特徴 コンテキストの存在: 組込みシステムはハード ウェアを通じて外部環境に影響を及ぼす。また 同時に、組込みシステムは外部環境からも影 響を受ける。 プロダクトライン型の開発: あるプロダクトファ ミリで共通に利用可能なアーキテクチャやコン ポーネント群を資産としてあらかじめ用意し、 個々のプロダクトは資産を合成して開発する。 4 現状の課題 -電気ポットを例に サーミスタ 水位センサー 水 ヒータ ポット内の水を沸騰させる ヒータのOn/Offによって水温を制御する 水温が100度に達すると、保温状態に移行する 水位センサーにより水量を観測する 5 プロダクトラインに基づいた 仕様策定プロセスの典型例 ステップ1 フィーチャ分析 ステップ2 SW仕様策定 電気ポット SW Boil: () ==> () Boil() == while thermistor.GetTemperature() <= 100.0 do heater.On(); HW コントローラ ヒータ サーミスタ 水位 水位 センサー メータ 必須フィーチャ SW仕様は正しい? オプション・フィーチャ 6 実は、仕様が正しいかどうかは相対的 コンテキストに依存 このSW仕様は「通常気圧(1気圧)の環境下で 水を沸騰させる」場合には正しい仕様である。 しかし、想定しているコンテキストが変更にな ると、SW仕様が仮定するコンテキストと実際 のコンテキストとの間にズレが生じ、最終的な システム上の欠陥につながる。 例: 「低気圧(1気圧未満) の環境下で水を沸騰させ る」場合(気圧の低い山頂での利用など) 7 現状の課題 仕様の再利用性が低い: 特定のコンテキスト を仮定し、そのためのロジックを決めてしまう ことが多く、仕様を再利用することが難しい。 システムの保守・発展がアドホック的: 想定す るコンテキストが変わるたびに仕様を見直す が、その対応が場当たり的。 仕様の妥当性確認が困難: 上記2点の結果と して、システムとコンテキストの間に生じる不 整合や欠陥を見落とす可能性が高くなる。 8 本研究のアプローチ プロダクトラインをシステムラインとコンテキス トラインに分け、各々フィーチャ分析を行う。 システムラインを構成するハードウェアおよ びソフトウェア仕様、コンテキストラインを構 成するコンテキスト仕様が資産になる。 仕様記述に形式手法(今回はVDM++)を適用 する。妥当性確認はVDM++のテスト実行によ り行う。 9 2.コンテキストを考慮したプロダ クトライン 10 プロダクトラインの構成 システムの フィーチャ分析 コンテキストの フィーチャ分析 電気ポット 現実世界 HW SW コントローラ ヒータ サーミスタ 水位 水位 センサー メータ 気圧 高い 通常 液体 低い 水 ミルク 必須フィーチャ オプション・フィーチャ 相互排他的フィーチャ 11 プロダクトライン開発の手順 コア資産 開発プロセス 管理 プロセス コンテキスト資産の開発: コンテキストのフィーチャ 分析、仕様資産の開発を 行う システム資産の開発: ハードウェアとソフトウェア のフィーチャ分析、仕様資 産の開発を行う VDM++ による テスト実行 プロダクト 開発プロセス 想定コンテキストの定義: コンテキスト資産群からプ ロダクトが想定する仕様 資産を選択する プロダクト構成の定義: システム資産群からプロ ダクトを構成する仕様資 産を選択する 仕様の妥当性確認: ハードウェア、ソフトウェア、 コンテキストの各仕様を組 み合わせた結果に不整合 がないか否かを確かめる 12 3.VDM++による仕様記述と妥 当性確認 13 VDM++と支援ツール VDM++はVDM-SL (The Vienna Development Method – Specification Language)のオブジェ クト指向拡張。 厳密なモデル化を目的とした仕様記述言語。 VDM++ Toolbox: VDM++のための開発環境。 仕様の構文・型チェック、証明課題生成、イン タープリタ等の機能をもつ。 14 VDM++仕様の プロダクトラインへの割当て 電気ポット (USER-test.vpp) システムの フィーチャ分析 コンテキストの フィーチャ分析 現実世界 HW SW (REALWORLD.vpp) コントローラ (SYSTEM-SW -controller.vpp) ヒータ サーミスタ 水位センサ (SYSTEM (SYSTEM -HW -HW -heater.vpp) -thermistor.vpp) (SYSTEM 気圧 -HW (CONTEXT-atmospheric -liquid -air-pressureplace.vpp) -level -sensor.vpp) 高い 通常 (CONTEXT-atmospheric-air-pressureplace-high.vpp CONTEXT-atmospheric-air-pressureplace-normal.vpp CONTEXT-atmospheric-air-pressureplace-low.vpp) 低い 液体 (CONTEXT-liquid.vpp) 水 ミルク (CONTEXT-liquid-water.vpp) 15 VDM++による仕様記述 テスト仕様 システム仕様 (システムラインから選択) UserTest SYSTEM-SW-controller test: () ==> () test() == (realworld := new RealWorld(); realworld.Setup(); sw := new Software(); sw.Setup(realworld); sw.Boil()); SW インタフェース Setup: () ==> () Setup() == (aap := new NormalAtmosphericAirPressure(); aap.SetAtm(1.0); liquid := new Water(); liquid.SetAap(aap); liquid.SetBoilingPoint(); liquid.SetTemperature(35.0); liquid.SetAmount(1000.0)); RealWorld (低気圧(1気圧未満)の環境) Setup: () ==> () Setup() == (aap := new LowAtmosphericAirPressure(); aap.SetAtm(0.53); liquid := new Water(); liquid.SetAap(aap); liquid.SetBoilingPoint(); liquid.SetTemperature(35.0); liquid.SetAmount(1000.0)); CONTEXT-liquid AddTemperature: () ==> () AddTemperature() == if temperature <= boiling_point(aap.GetAtm()) then temperature := temperature + 1.0 else (temperature := boiling_point(aap.GetAtm()); amount := amount - 1.0 --- evaporation ) pre temperature <= boiling_point(aap.GetAtm()) + 10.0 post temperature <= boiling_point(aap.GetAtm()) + 1.0; 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); ); 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; RealWorld (通常気圧(1気圧)の環境) コンテキスト仕様 (コンテキストラインから選択) HW インタフェース SYSTEM-HW-heater public On: () ==> () On() == (sw := <On>; realworld_liquid.AddTemperature()); コンテキスト インタフェース CONTEXT-liquid-water SetBoilingPoint: () ==> () SetBoilingPoint() == boiling_point := {1.0 |-> 100.0, 0.53 |-> 85.0}; CONTEXT-atmospheric-air-pressureplace GetAtm: () ==> real GetAtm() == return atm; SYSTEM-HW-thermistor SYSTEM-HW-liquid-level-sensor CONTEXT-atmospheric-air-pressureplace-normal instance variables inv atm = 1 16 プロダクトラインからの構成要素の選択 電気ポット (USER-test.vpp) システムの フィーチャ分析 コンテキストの フィーチャ分析 現実世界 HW SW (REALWORLD.vpp) コントローラ (SYSTEM-SW -controller.vpp) ヒータ サーミスタ 水位センサ (SYSTEM (SYSTEM -HW -HW -heater.vpp) -thermistor.vpp) (SYSTEM 気圧 -HW (CONTEXT-atmospheric -liquid -air-pressureplace.vpp) -level -sensor.vpp) 高い 通常 (CONTEXT-atmospheric-air-pressureplace-high.vpp CONTEXT-atmospheric-air-pressureplace-normal.vpp CONTEXT-atmospheric-air-pressureplace-low.vpp) 低い 液体 (CONTEXT-liquid.vpp) 水 ミルク (CONTEXT-liquid-water.vpp) 17 仕様の妥当性確認 電気ポットの仕様の妥当性をVDM++インタプ リタのテスト実行により確認する コンテキスト仕様A システム 仕様 通常気圧(1気圧)の環境下で水を沸騰 CONTEXT-atmospheric-air-pressureplace-normalと CONTEXT-liquid-waterが選択 コンテキスト仕様B 低気圧(1 気圧未満) の環境下で水を沸騰 CONTEXT-atmospheric-air-pressureplace-lowと CONTEXT-liquid-water 18 システム仕様 SYSTEM-SW-controller.vpp class Software instance variables heater : Heater; thermistor : Thermistor; liquid_level_sensor : LiquidLevelSensor; 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; operations public Setup: RealWorld ==> () Setup(realworld) == (heater := new Heater(); end Software heater.Setup(realworld); thermistor := new Thermistor(); thermistor.Setup(realworld); liquid_level_sensor := new LiquidLevelSensor(); liquid_level_sensor.Setup(realworld); ); ポット中の水が無くなる ことがないことを 制約条件とする 19 テスト実行結果(コンテキストA) 正常 20 テスト実行結果(コンテキストB) 事後条件違反 (沸騰し続け、水がなくなる) 21 妥当性確認後の対応 システムとしてどのような仕様にすべきか (ハードウェアを追加すべきか、或いはソフト ウェアで頑張るべきか)、その妥当性を調べる ことが可能となる。 コンテキストBに対応するには、沸点(気圧に より変化)に応じた加温操作が必要となるため、 気圧センサーが必須となる。 上流段階で、仕様の妥当性、仕様策定 の戦略が明確になる 22 4.考察と関連研究 23 開発プロセスのあり方 モデリング UMLモデルをVDM++モデルに変換する VDM++モデルに、事前条件、事後条件、不変条 件を追加し、仕様を厳密化する。 テスト実行による仕様の妥当性を確認する。 事前条件・事後条件・不変条件 実装 VDM++モデルをJavaコードに変換する。その際、 事前条件、事後条件、不変条件をJMLに変換する ESC/Java2等のJMLツールを用いて、事前条件、 事後条件、不変条件を検証する。これにより、 VDM++モデルがJavaコードに正確に洗練 (Refinement)されているかが検証される。 24 陽関数と陰関数 仕様を陽関数として記述するとインタプリタに よるテスト実行が可能になるが、その反面、 仕様と実装の差異が曖昧になる。 仕様記述という意味では陰関数を用いる方が 望ましいが、逆にテスト実行できないため妥 当性を確認するのが難しくなる。この場合、証 明支援ツールを用いて仕様を検証する必要 がある。 25 陽関数と陰関数(我々の見解) 仕様記述において重要なのは不変条件など の制約条件を特定化すること。 一般に不変条件は抽出するのが難しく、テス ト実行しながら見つけていくことは有効。その ため、本研究では仕様を陽関数で記述する方 式を採用。 しかし、制約条件を洗い出し、その妥当性を 確認した後は関数本体は必ずしも必要でない。 VDM++によるモデル化は制約条件を洗い出 すための工程とみなすこともできる。 26 アスペクト指向の導入 沸点を考慮したシステムを構築するには 気圧センサー(HW)を追加する 新たな仕様記述は、様々な箇所に散らばる 横断的関心事 class Software instance variables heater : Heater; thermistor : Thermistor; liquid_level_sensor : LiquidLevelSensor; aap_sensor : AapSensor; realworld_liquid : Liquid; operations public Setup: RealWorld ==> () Setup(realworld) == (realworld_liquid := realworld.liquid; heater := new Heater(); heater.Setup(realworld); thermistor := new Thermistor(); thermistor.Setup(realworld); liquid_level_sensor := new LiquidLevelSensor(); liquid_level_sensor.Setup(realworld); aap_sensor := new AapSensor(); aap_sensor.Setup(realworld); ); AspectVDM public Boil: () ==> () Boil() == while thermistor.GetTemperature() <= GetBoilingPoint() and liquid_level_sensor.IsOn() = true do heater.On() pre liquid_level_sensor.IsOn() = true post liquid_level_sensor.IsOn() = true; -- 環境への知識を仮定している部分は関数として分離する。 -- これがjoin pointとなる public GetBoilingPoint: () ==> real GetBoilingPoint() == return realworld_liquid.GetBoilingPoint(aap_sensor.GetAtm()); end Software 27 関連研究 問題フレーム[M.Jackson, 2001]: 機械(システ ム)と現実世界(コンテキスト)の関連をモデル化。 KobrA[Atkinson et al., 2001]: プロダク トライン開発手法の一つ。KobrA のコンテキス トはシステム対象内の問題領域をシステム外 と同時に捉える。 ESIM法[三瀬 他, 2005]: 非正常系の分析。 外部環境分析法[鷲見 他, 2005]: 外部環境分 析の手順化。 28 関連研究(形式手法) Feature Algebra [P.Hofner, et al. FM’06] 29 5.まとめ 30 まとめ 外部環境などのコンテキストを考慮した組込 みシステムの仕様記述とその妥当性確認方 法をプロダクトライン開発の観点から提案した。 通常のビジネスシステムに対しても本手法は 適用可能。 安全、安心なシステム構築にはコンテキスト の視点が今後ますます重要になってくる。 31
© Copyright 2024 ExpyDoc