スライド 1

組込みシステムの外部環境に
着目した動作仕様検証
九州工業大学鵜林研究室
金川太俊瀬戸敏喜谷口奨吉田純鵜林尚靖
(株)東芝ソフトウェア技術センター
鷲見毅
平山雅之
1
目次
• 研究の背景
– 外部環境分析手法
– 外部環境分析における問題点
• 形式手法を用いた外部環境分析の妥当性確認
– テスト実行
– システムと外部環境の振舞い検証
• 適用事例
• まとめと今後の課題
2
研究の背景
組込みシステムにおける
外部環境分析とその問題点
3
研究の背景
不具合発覚！
システム開発プロセス
分析
設計
最初から見直し
実装
コスト大
上流工程
分析
テスト
下流工程
設計
ドキュメント
実装
テスト
信頼性の高い出力であれば手戻りは軽減できる
本研究は組込みシステム開発における信頼性向上を目的とする
4
組込みシステム開発の特徴
：システム外の環境から影響を受け、不具合を出すケースが多い
→外部環境を分析する手法を提案
外部環境を分析することで組込みシステム開発における信頼性を
向上させる
上流工程
分
析
下流工程
外
部
環
境
分
析
不具合発覚！
設
計
ドキュメント
実
装
テ
ス
ト
外部環境を考慮したモノ
外部環境に起因するものは
存在しない
→信頼性向上
不具合
5
外部環境分析手法
1.組込みシステムと外部環境とのインタラクションを行うハードウェアを抽出する
2.抽出したハードウェアが注目する要素(Context)と、その値に影響をする要素
(Context)を抽出する
3.組込みシステムと外部環境の構造を、UMLプロファイルを用いて静的/動的の
両側面から記述する
《Actuator》
《Sensor》
駆動モータ
光センサ
外乱
コースの勾配
車体の速度
例：ライントレーサロボット
ラインの
反射光
環境光
外部環境の範囲：システムに要求された安全性、信頼性、機能性
を満たすために必要な範囲
6
成果物：外部環境クラス図
→外部環境の静的記述
システム
関連ごとに
ステレオタイプ付加
クラスごとに
ステレオタイプ付加
外部環境
7
成果物：各クラスの状態遷移
→外部環境の動的記述
光センサ
直下部の反射光：弱い
遷移イベント：
他クラスの状態遷移
高い
低い
直下部の反射光：強い
直下部の反射光
環境光
直下部の色：黒
強い
時間の経過
弱い
直下部の色：白
弱い
時間の経過
直下部の色
ラインとの位置関係
ラインとの位置関係：ライン上
黒
強い
白
ラインとの位置関係：ライン外
車体の走行
ライン上
ライン外
車体の走行
8
外部環境分析における問題点
• 外部環境分析の範囲を決定する指針が無い
– システム要件を満たす範囲で外部環境分析を行いたい
– 現状、範囲の決定は分析者がAd-hocに行っている
本研究の目的
• 論理的な根拠に基づく外部環境分析範囲の妥当性確認を行う
• そのためのアプローチとして形式手法（Formal Method）を用
いる
外部環境
Ad-hoc
システム
論理的根拠
分析範囲
9
アプローチ
：形式手法を用いた外部環境分析の妥当性確認
• 形式手法
– 数学を用いた厳密な仕様記述
– 仕様の検証
• 現在の外部環境分析でシステム要件を満たすか否かを数学
的に検証する
– 不具合が発見されなければ現在の分析は妥当なもの
– 同時に、分析範囲外の外部環境については考慮していないことを明
示することにもなる
System
<<Hardware>>
光センサ
Observe
Noise
<<Context>>
直下部の反射光
Affect
<<Context>>
直下部の色
<<Context>>
ラインとの位置関係
Transfer
Context
時間の経過
<<Context>>
環境光
Transfer
types
LightVolume = real
環境光
強い
弱い
時間の経過
state EnvironmentLight of
environment_light : LightVolume
init el == el = mk_EnvironmentLight(0)
end
外部環境分析で得られた結果を形式手法に置き換え、検証する
10
形式手法を用いた
外部環境分析の妥当性確認
11
形式手法の使用目的
外部環境分析結果
システム要件を満たすか？
１．テスト実行
現在の外部環境範囲において、
潜在する不具合はないか？
２．網羅的振舞い検証
現在の外部環境分析は
妥当なものである
12
形式手法の使用目的（1）
：上流工程でのテスト実行
• 外部環境を考慮に入れたテストを上流工程で行う
• 現在の外部環境分析のもと、システム要件を満たす
かをテストにより確認する
• どこまでを外部環境仕様の範囲とすべきか数値を
もって探索する
形式手法に変換
type
外部環境の仕様
仕様の変更
・・・
operations
・・・
テスト実行
ツール補助により上流工程でのテスト実行が可能な、
VDM （Vienna Development Method）を用いる
13
形式手法の使用目的（2）
：システムと外部環境との振舞いを網羅的に検証
• システムと外部環境の状態の組み合わせを
網羅する
• 不具合が潜在する組み合わせがないか検査
する
システム
外部環境
振舞いを検証
自動で網羅的検査を行うことができる、
SPINを用いる
14
形式手法の導入方法
・外部環境分析手法 UMLプロファイルを作成
・プロファイルは形式手法への導入を意識して作成している
Ｕ
Ｍ
Ｌ
プ
ロ
フ
ァ
イ
ル
外部環境分析手法
クラス図
形
式
手 VDM
法
type
・・・
operations
・・・
状態遷移図
・クラスの種類
・クラス間の関連
・各クラスの状態遷移
SPIN
active proctype ・・・(){
do
:: ・・・
od
}
15
適用事例
テスト実行
振舞い検証
16
適用事例（１）
：テスト実行
• VDMを用いて外部環境を考慮した仕様の探
索を行う
– 分析時に想定している外部環境の属性値をパラ
メータとして変化させ、テストケースを作る
– テストケースに従いテスト実行
– 現在の仕様でシステム要件を満たすか確認する
• 範囲によって満たさない場合があるならば、その範囲
を数値的に明示する
17
VDM適用例
外部環境分析結果からの入力
→外部環境クラス図
クラスの種類
クラス間の関連
外部環境クラス図からクラスごとに情報を抜き出す
ステレオタイプ
クラス名
クラスの属性
18
VDM-SL（ VDM-Specification Language ）による記述
例：環境光
ステレオタイプ：Context
クラス名：環境光
属性：光量：real
ステレオタイプ
VDM-SLで記述
Contextの記述形式に基づく記述（本研究で定義）
types
LightVolume = real
クラス名
クラスの属性
state EnvironmentLight of
environment_light : LightVolume
init el == el = mk_EnvironmentLight(0)
end
19
＊VDM-SL：VDMの記述言語の一つ
ツール補助によるテスト実行
：今回はCSKシステムズが公開している
「VDMTools」を使用
20
VDM：テスト実行による探索（ライントレース機能）
光センサが扱うセンサ値は0～100
白を示す値（誤認識）
100
上限値
90
白
期待値
75
下限値
60
上限値
40
期待値
25
環境光
センサ値：75
環境光
環境光の大きさがセンサに対し15の影響を与えるとき
環境光の大きさがセンサに対し60の影響を与えるとき
環境光の大きさがセンサに対し30の影響を与えるとき
どちらともとれない中間値
環境光
センサ値：55
環境光
環境光
黒
センサ値：40
反射光の値：25
・各パラメータの値によって想定外の動
作が生じるケースが存在する
・テストケースを作成しそれらのケースを
探索する
下限値
10
0
※黒：反射光（10～40）
実験等により既に明確
21
VDM：テスト実行による探索（ライントレース機能）
各種パラメータを変化させテスト実行する
変化させるパラメータ＝分析時に想定するパラメータ
・環境光の値
・反射光の値
＊色の閾値と期待値：システム側で規定する部分のため対象外
例：環境光のパラメータを変化させる
types
LightVolume = real
state EnvironmentLight of
environment_light : LightVolume
init el == el = mk_EnvironmentLight(30)
mk_EnvironmentLight(15)
mk_EnvironmentLight(0)
end
パラメータ変化
22
VDM：テスト実行による探索
下限値10、上限値40
反射光の値
10
25
40
0
OK
OK
OK
15
OK
OK
中間値
30
OK
中間値
誤認識
45
中間値
誤認識
誤認識
60
誤認識
誤認識
誤認識
環境光の値
この問題について、
中間値は読み飛ばせばよい
「環境光が30以上の状況では動作を保証しない」という仕様にする
問題は黒を白と誤認識してしまうこと
か、HWの追加等行い問題を解決するかは設計判断であり、
このテストにより、環境光の値が30以上となったと
本手法の範囲外のものと考えている
き、動作の保証が不可能であることが分かった
23
適用事例（２）
：網羅的探索による振舞い検証
• SPINを用いてシステム全体と外部環境の振
舞いを検証する
– VDMでは機能ごとに検証を行ったが、SPINでは
システム全体の動作を検証する
– 外部環境分析範囲は一種の閉空間である
– その閉空間の中において不具合を引き起こす
ケースがないか網羅的に探索する
24
SPIN適用例
光センサ
外部環境分析結果からの入力
→各クラスの状態遷移図
直下部の反射光：弱い
高い
低い
直下部の反射光：強い
直下部の反射光
環境光
直下部の色：黒
強い
時間の経過
弱い
強い
直下部の色：白
各クラスの状態遷移
各クラスの並行性
時間の経過
直下部の色
ラインとの位置関係
ラインとの位置関係：ライン上
黒
弱い
車体の走行
ライン上
白
ラインとの位置関係：ライン外
ライン外
車体の走行
各状態遷移図から情報を抜き出す
環境光
時間の経過
強い
弱い
状態
時間の経過
遷移イベント
25
Promeraによる記述
例：環境光
並行性：独立に動作
イベント：時間の経過（非決定的）
状態：強い、弱い
独立に動作
非決定的
環境光
時間の経過
強い
弱い
時間の経過
Promeraで記述
active proctype EnvironmentLight(){
do
::EL_state = EL_Weak;
::EL_state = EL_Strong;
od
}
状態
26
状態遷移図を全てPromeraで記述する
ラインとの位置関係
環境光
光センサ
これらの状態モデルを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;
・・・・・
27
SPINによる振舞い検証
エラー表示
この結果から….
車体はライン上
環境光は強い状態
システムはライン外と
認識している
環境光
強い
新規の不具合なし
ラインとの位置関係
ライン上
システム
ライン外と認識
28
適用事例まとめ
外部環境分析結果
環境光による
不具合発覚
システム要件を満たすか？
１．テスト実行
現在の外部環境範囲において、
潜在する不具合はないか？
新規の不具合
なし
２．網羅的振舞い検証
現在の外部環境分析は
妥当なものである
29
まとめ・今後の課題
30
まとめ
・形式手法を用いることで外部環境分析の妥当性確
認が行える
・分析範囲内で発見した不具合への対応は製品企画
の側面からの判断が必要
・但し、どんな場合に問題となるかが明確になるので、
製品企画上の判断を助ける情報を提供できる
今後の課題
・形式モデルの作成手順を整理して、より容易に実行
できる様にする
・組込みシステムに限らず、コンテキスト分析が必要
な開発全てに適用可能な手法に発展させる
31
終
32
補足用
33
SPIN：網羅的探索による振舞い検証
ライントレース機能と障害物回避機能の競合
ライントレース機能：
光センサを用いてラインを検知し、進行方向を
ライン上なら左へ、ライン外なら右へとる
障害物回避機能：
超音波センサを用いて、障害物の存在しない
分岐方向へ進む、この状況では進行方向を左
へとることで回避する
①ライントレース走行中
②超音波センサが障害物を検知
障害物
障害物を検知し
たので左へ
ライン外へ出
たので右へ
34

Download Report