環境光 - POSL

組込みシステムにおける
外部環境分析手法と形式手法の適用
九州工業大学鵜林研究室
金川太俊瀬戸敏喜谷口奨吉田純
1
研究の背景
不具合発覚！
システム開発プロセス
分析
設計
最初から見直し
実装
コスト大
上流工程
分析
テスト
下流工程
設計
ドキュメント
実装
テスト
信頼性の高い出力であれば手戻りは軽減できる
本研究は組込みシステム開発における信頼性向上を目的とする
2
組込みシステム開発の特徴
：システム外の環境から影響を受け、不具合を出すケースが多い
→外部環境を分析する手法を提案
外部環境を分析することで組込みシステム開発における信頼性を
向上させる
上流工程
分
析
下流工程
外
部
環
境
分
析
不具合発覚！
設
計
ドキュメント
実
装
テ
ス
ト
外部環境を考慮したモノ
外部環境に起因するものは
存在しない
→信頼性向上
不具合
3
目的
組込みシステムにおける信頼性向上
外部環境に起因する不具合を上流の段階で発見する
手段
システムの外部環境を分析
外部環境分析で得た結果を厳密化、検証する
4
外部環境分析手法概要
1.システムと外部環境との架け橋となるHWに注目
2.注目したHWが扱うデータに影響を与える外部環境を洗い出す
3.外部環境の影響によって生じる不具合を抽出する
本研究では1,2,3の工程を体系的に行えるようガイドライン化した
《Actuator》
《Sensor》
駆動モータ
光センサ
車体の速度を変化
コースの勾配
外乱
車体の速度
例：ライントレーサロボット
ラインの
反射光
環境光
外部環境の範囲：システムに要求された安全性、信頼性、機能性
を満たすために必要な範囲
5
外部環境分析手法の成果物
・外部環境クラス図（UMLのクラス図をベースとする）
・各クラスの状態分析結果
Context
Software
Hardware
6
検証の必要性
・外部環境分析手法を用いただけでは分析の視野を広げただけ
にとどまる
→作成したモデルの検証が必要
・図や文書のままでは検証に不向き
→形式手法の導入
type
・・・
operations
・・・
図、文書
形式手法
形式手法
・数学を用いた厳密な仕様記述
・検証
7
形式手法導入のメリット
：VDM（ Vienna Development Method ）
・厳密な仕様記述の探索に用いることができる
・VDMは関数の厳密な記述に長けている
・ツール補助により、上流レベルでのテスト実行が可能
・テスト実行を繰り返し厳密な仕様を探索
VDMに変換 VDM
type
外部環境の仕様
フィードバック
・・・
operations
・・・
テスト実行
8
形式手法導入のメリット
：SPIN
・システムと外部環境の振舞いを検証できる
・SPINは対象の状態を網羅的に探索し性質を検査する
・システムの状態と外部環境の状態の組み合わせを網羅
し、エラーの生じるケースを洗い出す
システム
外部環境
振舞いを検証
9
形式手法の導入方法
・外部環境分析手法 UMLプロファイルを作成
・プロファイルは形式手法への導入を意識して作成している
Ｕ
Ｍ
Ｌ
プ
ロ
フ
ァ
イ
ル
外部環境分析手法
クラス図
形 VDM
式
type
手
・・・
法
operations
・・・
厳密な仕様記述
の探索
状態遷移図
SPIN
active proctype ・・・(){
do
:: ・・・
od
}
システムと外部環
境
10
SPIN適用例（ライントレーサ：光センサの観測）
・システム、環境光、ラインとの位置関係が並行動作している
ものと考える
ラインとの位置関係
環境光
これらの状態モデルをPromeraで記述
システム
環境光
active proctype EnvironmentLight(){
do
::EL_state = EL_Weak;
::EL_state = EL_Strong;
od
}
ラインとの位置関係
active proctype Position(){
do
::PS_state = On;
::PS_state = OutSide;
od
}
システム
振舞いをSPINで検証する
active proctype LightSensor(){
do
::if
::RL_state == RL_Weak ->
if
::PS_state == OutSide -> assert(false);
::PS_state == On -> true;
・・・・・
11
SPIN適用例（光センサの観測）
・Promeraで記述した対象をSPINを用いて検証する
エラー表示
この結果から….
車体はライン上
環境光は強い状態
システムはライン外と
認識している
環境光
強い
ラインとの位置関係
ライン上
システム
ライン外と認識
12
まとめ
手法により組込みシステム開発における信頼性向上
が期待できる
・外部環境分析手法の提案
外部環境分析手法により分析の範囲を外部環境に拡張
することができた
・組込みシステムにおける形式手法の適用
手法により作成した外部環境モデルの検証のため形式手法
を用いた
手法のマニュアル化
・外部環境モデル記述用プロファイルを作成
UMLから形式手法への移行方法を含む
13
形式手法 VDM（ Vienna Development Method ）
・厳密な仕様記述の探索に用いることができる
・機能的側面からの検証に長ける形式手法
関数実行前、実行後に不整合が存在しないか検証する
VDM-SL（ VDM-Specification Language ）記述例
例：環境光
データ「光量」を保持し、「光量」の変化により状態を遷移する
VDM-SLで記述
types
LightVolume = real
state EnvironmentLight of
environment_light : LightVolume
init el == el = mk_EnvironmentLight(0)
end
＊VDM-SL：VDMの記述言語の一つ
14
VDM-SL テスト実行による検証
：ツール補助によりインタプリタを用いたテスト実行が可能
15

Download Report