slide - POSL

形式的洗練パターンによる
コンポーネントベース・ゴールモデリング
手法
C-KAOS (Component-based KAOS)
九州工業大学：○野村潤, 成瀬龍人
九州大学：外村慶二, 鵜林尚靖
株式会社デンソー：司代尊裕, 岩井明史
1/21
概要
C-KAOS
ゴールモデルの分割統治
形式的洗練パターン
C→◇T
KAOS
C∧D→◇T
C→◇D
C→CWT
コンテキスト毎にコンポーネント化
歩行者
衝突防止
追突防止
信号無視
防止
信号無視
防止
追突防止
パターンに基づき合成
歩行者
衝突防止
巨大化・複雑化
コンポーネントの組み合わせにより
様々な状況におけるモデルを構築
発表の流れ
1. 研究の背景と問題意識
2. C-KAOSと記述例
3. 考察と関連研究
4. まとめと今後の問題
3/21
１．研究の背景と問題意識
4/21
ゴール指向分析
ゴール指向分析
・要求を細分化し、要求の達成に必要な機能やオペレーションなどを明らかにする
KAOS（Keep All Objectives Satisfied）
・木構造のモデルを用い、ゴールを系統的に抽出する
・ソフトウェアの機能要件の抽出、機能間のトレードオフの明確化、
形式検証に主に役立つ
早く目的地へ着く
Why
ゴール
↓
要件
移動距離を短く
What
エージェント
↓
Who
・・・
・・・
距離計算
カーナビ
AND分解
OR分解
5/21
問題意識
歩行者と
衝突しない
他の車と
接触しない
一時停止無視・
出会い頭衝突をしない
信号無視を
しない
周囲の状況に応じて振る舞いを変えるシステムでは
様々なコンテキストを考慮して分析を行う必要がある
例）運転支援システム
6/21
問題意識
事故が起こっ
ていない
対物距離を適度
に保っている
進行方向に
障害物がない
車両の有無によって
振る舞いが変化する
前方車両との
車間が適切
交通規則を
守っている
車間を適度
に保っている
左右の車との
車間が適切
前方車両との車間に合わ
せて速度を調整している
停止線を守っ
ている
後方車両との
車間が適切
制限速度を
守っている
信号を守って
いる
表示色が伝
わっている
信号機が物
に隠れていな
距離によってい
走る道路によって
振る舞いが変化する
横断中の歩
行者を優先
信号機が設
置してある
信号機を運転
手が見ている
ランプを点灯
している
切替規則が
定義してある
振る舞いが変化する
距離が狭いときに
速度を上げない
距離が広いときに
速度を落とさない
距離が適切なときに
速度を上げ下げしない
全ての状況を網羅したモデルを
一度に作るのは困難
当然、問題を分けて考えたい
7/21
問題意識
事故が起こっ
ていない
どう切り分ける？
対物距離を適度
に保っている
進行方向に
障害物がない
前方車両との
車間が適切
車間を適度
に保っている
左右の車との
車間が適切
交通規則を
守っている
停止線を守っ
ている
後方車両との
車間が適切
制限速度を
守っている
表示色が伝
わっている
信号を守って
いる
信号機が設
置してある
どう組み合わせる？
横断中の歩
行者を優先
ランプを点灯
している
ゴールモデルの満たすべき性質
１）抽出したゴールでトップゴールが達成されなければならない (completeness)
２）ゴール間の記述内容に矛盾があってはならない (consistency)
３）各ゴールはトップゴールの達成に必要最低限でなければならない (minimality)
⇒これらを満たす分割統治の方法を考える必要がある
8/21
２．C-KAOSと記述例
9/21
形式的洗練パターン
C⇒◇T
C⇒◇T
C⇒◇M
M⇒◇T
Milestone-driven refinement
C∧D⇒◇T
C⇒◇D
C⇒CWT
Guard-Introduction refinement
形式的洗練パターン
[Lamsweerd2007]で述べられているゴール分解のパターン
時相論理式を用い、形式的に正しいゴール分解を行う
形式的洗練パターンには以下の４つがある
（１）Milestone-driven refinement
（２）Guard-Introduction refinement
（３）Realizability-driven refinement
（４）First-order refinement
[文献]
A. van Lamsweerde.: Engineering Requirements for System Reliability and Security, in Software System Reliability and
Security, M. Broy, J. Grunbauer and C.A.R. Hoare (eds.), NATO Security through Science Series - D: Information and
10/21
Communicarion Security, Vol. 9. IOS Press, 2007, 196-238
Guard-Introduction refinement
1. C⇒◇D：Hyp
2. C∧D⇒◇T：Hyp
C⇒◇T
C：初期状態ガードを定義
T：目標状態
3. C⇒CWT：Hyp
ガード達成の細分化
D：ガード
4. C⇒(C U T)∨□C：3,
def of Unless
道を選ぶ
走行する
◇a：「いつかa」
C⇒CWT
C∧D⇒◇T
C⇒◇D
a⇒b：「aならばb」 5. C⇒◇T∨□C：4, def of Until
aWb：「bまでa」 6. C⇒◇D∧(◇T∨□C)：1,5, strengthen consequent
目的地に着く
楽な道
目標状態へ遷移するガードを達成する勝手に状態遷移
C∧D∧D’⇒
C∧D
C∧D⇒
ためのゴール
を起さない
新しいガードD’を追加
7.ためのガードを定義
C⇒(◇D∧◇T)∨(◇D∧□C)：6,
distribution
コストがかかガードの細分化において
事故を起こさ
(C∧D)WT
◇T
⇒◇D’
便利がいい
早く着く
捕まらない
らない
ない
互いに混じり合うことがない
8. C⇒(◇D∧◇T)∨◇(D∧C)：7, trivial lemma
C∧D∧D’∧D’’⇒
◇T
9. C∧D∧D’
C⇒(◇D∧◇T)∨◇◇T：8,2,
→個々に独立したコンポーネント
C∧D∧D’⇒ strengthen consequent
同様にガードD’’を追加
として扱うことができる
10. C⇒(◇D∧◇T)∨◇T：9,3-idempotence
⇒◇D’’
(C∧D∧D’)WT
11. C⇒◇T：10, absorption
11/21
ゴールコンポーネントと合成
[X]∧D⇒◇[Y]
[X]⇒◇D
[X]⇒[X]W[Y]
ゴールコンポーネントの基本形
C⇒◇T
＋
[X]∧D⇒◇[Y]
[X]：初期状態パラメタ
[Y]：目標状態パラメタ
D ：ガード
“C⇒◇T”型のゴールへ合成可
[X]⇒◇D
[X]⇒[X]W[Y]
[X] に C を代入
[Y] に T を代入
C⇒◇T
C∧D⇒◇T
C⇒◇D
C⇒CWT
12/21
記述例
例）信号機付きの交差点の先に目的地がある場合
初期状態 C ：走行中
目標状態 T ：目的地へ到着した状態
目的地に到着するためには、
まずは信号機を通過する必要があるため、
「信号機を通過した状態」をガードS（Signal）とする
信号機を通過した後は、
交差点を通過する必要があるため、
「交差点を通過した状態」をガードI（intersection）
とする
車両の走行に影響を与えるコンテキスト
{ 信号機, 交差点 }
13/21
ゴールコンポーネント
component_S：信号機(signal)コンポーネント
[X]∧S⇒◇[Y]
[X]⇒◇S
[X]⇒[X]W[Y]
component_I: 交差点(intersection)コンポーネント
[X]∧I⇒◇[Y]
[X]⇒◇I
[X]⇒[X]W[Y]
S：信号機を通過した状態, I : 交差点を通過した状態
14/21
ゴールコンポーネントの合成１
（信号機と交差点をそれぞれ別のコンテキストとした場合）
車両のゴール
C⇒◇T
[X] ← C
[Y] ← T
component_S
C∧S⇒◇T
C⇒◇S
component_I
C∧S∧I⇒◇T
C∧S⇒◇I
C∧S
⇒(C∧S)WT
C⇒CWT
[X] ← C∧S
[Y] ← T
初期状態 C ：走行中という状態
目標状態 T ：目的地に到着した状態
ガード S ：信号機を通過した状態
ガード I ：交差点を通過した状態
15/21
ゴールコンポーネントの合成２
（信号機を交差点の一部とした場合）
車両のゴール
C⇒◇T
[X] ← C
[Y] ← T
component_I
C∧I⇒◇T
C⇒◇I
C⇒CWT
component_S
C∧S⇒◇I
C⇒◇S
C⇒CWI
初期状態 C ：走行中という状態
目標状態 T ：目的地に到着した状態
ガード S ：信号機を通過した状態
ガード I ：交差点を通過した状態
[X] ← C
[Y] ← I
16/21
３．考察と関連研究
17/21
考察
満たすべき性質
１）抽出したゴールでトップゴールが達成されなければならない
２）ゴール間の記述内容に矛盾があってはならない
３）各ゴールはトップゴールの達成に必要最低限でなければならない
•
形式的洗練パターンを用いることで，1)と2)は解決
•
しかし、3)は解決できない
– 合成によって、他のコンポーネントで既に満たされているゴールが
複数箇所に混在してしまう場合がある
•
また、トレードオフの解消も重要な要素であるが、
形式的洗練パターンによる解決はできない
18/21
関連研究
AGORA ( Attributed Goal-Oriented Requirements Analysis method )
•
分析結果の品質に着目してゴール分解の支援を行うゴール指向分析法
[Kaiya2002]
•
ゴールに対して貢献度と優先度を属性値として付加することで、
1. ゴール分解の指針
2. 衝突の解消を行うための優先順位付け
3. ゴールの選択肢が複数あるときの判断基準
などについて支援を行う。
•
要求仕様書の妥当性、非曖昧性、完全性などの品質を評価可能
[文献]
Kaiya，H.，Horai，H.，and Saeki，M.: AGORA : Attributed Goal-Oriented Requirements Analysis
Method，In Proceedings of the 10th Aniversary IEEE Joint International Conference on
Requirements Engineering (RE’02)，pp13-22，2002.
19/21
４．まとめと今後の課題
20/21
まとめと今後の問題
•
まとめ
– C-KAOSでは、Guard-Introductionを細分化規則として用いることで、
コンテキストからの影響を一つ一つ分けて考えることができ、
コンポーネントの組み合わせで様々な状況に応じたモデルの構築が可能
– 完全性、無矛盾性について正しさを述べることが可能
•
今後の課題
– モデル検査
– ゴール記述からオートマトンへ変換し、モデル検査
– 合成前後の正しさを検証
– トレードオフやゴール記述の重複の解決には至っていない
– 属性値による優先度の付加
– モデル探索による不要なゴールの発見
21/21
ご清聴ありがとうございました

Download Report