slide - POSL

SIGSS 2012年1月研究会 in 高知
アーキテクチャ点写像による
設計・コード間の双方向追跡
〜 SMTソルバーを用いた設計追跡性の検証
〜
鵜林尚靖（九州大学）
亀井靖高（九州大学）
２０１２年１月２６日
概要：
アーキテクチャ点とアーキテクチャ点写像
SMT
ソルバー
追跡性の保持が困難
public class Subject{
private Vector observers =
new Vector();
private String state = “”;
public void
addObserver(Observer o){ … }
public void
removeObserver(Observer o){ … }
public void
notify(){
Iterator i = observers.iterator();
while(i.hasNext() ){
Observers o =
(Observer)i.next();
o.update( this );
}
}
public void setState(String s){ state = s; }
public String getState() {return state; } }
適切な抽象度を保持した
アーキテクチャ設計とコード
の同期（双方向追跡）
2
発表内容
 研究の背景と目的
 アーキテクチャ点とその写像
 SMTベースの追跡性検証
 まとめと今後の課題
3
研究の背景と目的
4
ソフトウェアアーキテクチャとは？
 Bass, L. らによる定義
 The software architecture of a program or computing system
is the structure or structures of the system, which comprise of
software elements, the externally visible properties of those
elements, and relationships among them.
 アーキテクチャ設計はソフトウェア開発において重
要な役割を果たす
 保守性や信頼性などの主要ソフトウェア品質特性は
アーキテクチャ設計の善し悪しに依存する
Bass, L., et al.: Software Architecture in Practice, Addison-Wesley, 2003.
5
ソフトウェアアーキテクチャの課題
 設計者の意図を正確に記述すること
 コードとの一貫性を保つこと
 設計とコードの同期を取ること
public class Subject{
private Vector observers =
new Vector();
private String state = “”;
public void
addObserver(Observer o){ … }
public void
removeObserver(Observer o){ … }
public void
notify(){
Iterator i = observers.iterator();
while(i.hasNext() ){
Observers o =
(Observer)i.next();
o.update( this );
}
}
public void setState(String s){ state = s; }
public String getState() {return state; } }
Adequate support for moving from
architecture to implementation and
fluidly moving between design and
coding tasks.
Taylor, R. N. and Hoek, A.: Software Design and Architecture -The once and future focus of software engineering,
In Proceedings of 2007 Future of Software Engineering
(FOSE 2007), pp.226-243, 2007.
6
例題： Observer パターン
アーキテクチャ制約
クラス図
相互作用図
7
このコードはアーキテクチャに
適合しているであろうか？
正しく動作はする！
クラス図とも対応している！
しかし。。。
設計には適合していない！
正しい実装
8
アーキテクチャ設計の詳細化による解法
一つの解決策としてはアーキテクチャの詳細化がある
public class Subject{
private Vector observers =
new Vector();
private String state = “”;
public void
addObserver(Observer o){ … }
public void
removeObserver(Observer o){ … }
public void
notify(){
Iterator i = observers.iterator();
while(i.hasNext() ){
Observers o =
(Observer)i.next();
o.update( this );
}
}
public void setState(String s){ state = s; }
public String getState() {return state; } }
完全なコードを生成
しかし、アーキテクチャ設計は抽象的でなければならない
9
我々のアプローチ： Archface
アーキテクチャデザイン
アーキテクチャの設計
変更の反映
Archface
プログラム点の公開と連結
アーキテクチャの変更
アーキテクチャの
正しい実装
public class Subject{
private
Vector observers = new Vector();
private String state = “”;
…
}
コード
Naoyasu Ubayashi, Jun Nomura, and Tetsuo Tamai:
Archface: A Contract Place Where Architectural Design and Code Meet Together. 32rd
ACM/IEEE International Conference on Software Engineering (ICSE 2010), ACM PRESS, pp.75-84
(2010).
10
本発表 – 同期のための検証機構
 基本アイデア
 アーキテクチャ点（Archpoint）
 アーキテクチャ設計の本質部分を表現するための「設計上の点」
 コンポーネント間の構造やメッセージ相互作用などのアーキテクチャを表現
 アーキテクチャ点写像（ArchMapping）
 設計追跡性を実現するための機構
 例：「メッセージ送信イベント」等のアーキテクチャ点は「メソッド呼び出
し」等のプログラム点に写像される
 アーキテクチャ点が整合性を保ちつつプログラム点に
写像されているか否かを確認することにより検証
 ＳＭＴソルバーによる検証
11
アーキテクチャ点とその写像
12
アーキテクチャ点と
アーキテクチャ点写像
SMT
今回は振る舞いの観点
ソルバー
から
アーキテクチャ点写像
を紹介
適切な抽象度を保持した双方向の同期
13
双模倣関係による同期
 アーキテクチャ点の観点で設計とコードの間に双模
倣（bisimulation）関係が存在すれば、両者の間の
追跡性は保持される
 アーキテクチャ点とその出現順序に注目する限り、
設計とコードが振る舞い上区別できなければ、両者
は同期していると見なすことができる
 アーキテクチャ点の系列をＬＴＳ（Labelled
Transition System）と見なすと、プロセスだと考え
ることが可能
14
双模倣関係による同期（つづき）
抽象度の保持＝アーキテクチャ点に基づく双模倣
15
Archface から論理式への変換
cObserver
コンポーネントインタフェース
cSubject
コンポーネントインタフェース
アーキテクチャ設計
論理式
cObserverPattern
コネクタインタフェース
16
アーキテクチャの論理式表現
アーキテクチャを
アーキテクチャ点の集合と要素間の制約（論理式）
で表現
[List 3]
Observer_Pattern :=
sequence(
; [predicate]
cSubject_setState_message_receive, ; archpoint
cSubject_notify_message_send,
; archpoint
cSubject_notify_message_receive,
; archpoint
iteration(
; [predicate]
cSubject_update_message_send,
; archpoint
cObserver_update_message_receive, ; archpoint
cObserver_getState_message_send, ; archpoint
cSubject_getState_message_receive)) ; archpoint
17
プログラムコードの論理式表現
プログラムコード（の制御フロー）を
プログラム点の集合と要素間の制約（論理式）
で表現
[List 4]
Program_List1 :=
sequence(
cSubject_setState_execution,
iteration(
cSubject_size_call,
Vector_size_execution,
cSubject_get_call,
Vector_get_execution,
cSubject_update_call,
cObserver_update_execution,
cObserver_getState_call,
cSubject_getState_execution,
cObserver_println_call,
System_out_println_execution))
; [predicate]
; program point
; [predicate]
; program point
; program point
; program point
; program point
; program point
; program point
; program point
; program point
; program point
; program point
18
アーキテクチャ点写像と追跡性検証
アーキテクチャ点写像 refine
追跡性検証
例題の場合は
充足しない！
コードが設計に
適合していない！
19
ＳＭＴベースの追跡性検証
20
ＳＭＴ（背景理論付きＳＡＴ）
 ＳＭＴはＳＡＴ（Boolean satisfiability）を一般化。
 背景理論




等号と未解釈関数の理論
自然数・整数・有理数・実数
配列の理論
再帰データの理論
 Yices は代表的なＳＭＴソルバーの一つで論理式の充足
可能性を判定する。
Yices: http://yices.csl.sri.com/
21
Yices エンコーディング
順序保持
アーキテクチャ点の系列
は
配列でエンコーディング
22
検証例 – モデル検査
振る舞い検証（検証したい性質をＬＴＬで記述）
Yices エンコーディング
有界モデル検査
23
まとめと今後の課題
24
まとめと今後の課題
まとめ
 アーキテクチャ点とアーキテクチャ点写像を提案
 適切な抽象度を保ちつつ、設計とコードを同期
今後の課題
 現状はアーキテクチャ点とプログラム点が 1 対 1 に
対応する場合のみサポート
 今後、1 対 N および N 対 1 の場合をサポート
 １対N：
 N対１：
一つのアーキテクチャ点が複数のプログラム点に対応する場合
複数のアーキテクチャ点が一つのプログラム点に対応する場合
25
ご清聴ありがとうございました
26

Download Report