Q - qwik.jp

ICSE2012
Research Session 17: Formal Verification
1. Build Code Analysis with Symbolic Evaluation
2. An Automated Approach to Generating Efficient Constraint
Solvers
3. Simulation-Based Abstractions for Software Product-Line
Model Checking
担当者：横川智教 (岡山県立大学)
12/08/30
ICSE2012 勉強会
1
Q-1
Build Code Analysis with
Symbolic Evaluation
Ahmed Tamrawi, Hoan Anh Nguyen,
Hung Viet Nguyen, Tien N. Nguyen
(Iowa State University)
12/08/30
ICSE2012 勉強会
2
Background
ソフトウェア開発において，ビルドコードのメンテナン
12% - 36%のオーバヘッドを生じさせる．
ソースコードの修正を伴う作業の4% – 27%は，
関連するビルドコードの修正を必要とする．
GNU makeにおけるビルドコードの解析を目的とした
環境およびツールSYMakeの開発
code smellの検出とrefactoringが可能
12/08/30
ICSE2012 勉強会
3
SYMake
Makefileを解析し，SDG(記号依存グラフ)を生成．
ifeq($(OS),Linux)
ext = o
cmd = build.sh
else
ext = exe
cmd = build.bat
endif
Makefile
SDG
server.o
rcp1
all
client.o
Select
server.exe
rcp2
client.exe
if
serverNM := server.$(ext)
clientNM := client.$(ext)
programs := $(serverNM) $(clientNM)
server.
all: $(programs)
12/08/30
o
T-model
ICSE2012 勉強会
ext
+
4
Evaluation
7つのシステムに対してSYMakeを適用し，
(1) locset(変数の出現位置)の検出
(2) code smell検出とrefactoring
の正確性と有効性について評価
A. locset検出 (Tab. 3)
6人のPh.D.学生による手動検出との比較
• SYMakeで検出されたlocsetは全て正しく，全てカバーしてい
• テキスト検索ツールを使用した場合は検出ミスが多い
B. code smell detection, refactoring (Tab. 4)
8人のPh.D.学生による手動検出との比較
• SYMakeを利用することで，より正確に，かつ短時間で処理可
12/08/30
ICSE2012 勉強会
5
Q-2
An Automated Approach to
Generating Efficient Constraint
Solvers
Dharini Balasubramaniam, Christopher Jefferson,
Lars Kotthoff, Ian Miguel, Peter Nightingale
(University of St. Andrews)
12/08/30
ICSE2012 勉強会
6
Background
Constraint Solverは，組み合わせ問題を効率的かつ
自動的に解くための手法の一つである．
既存のSolverは，幅広い問題に対応できるように
多くの機能から一体型として設計されている．
構造が複雑で，スケーラビリティや拡張性が低い
Constraint Solver生成フレームワークDominionの開発
12/08/30
ICSE2012 勉強会
7
DominionにおけるSolver生成プロセス
コンポーネントの
仕様
解決すべき
問題
Problem
Generator
Component
Library
問題
コンポーネント
コンポーネントの
実装
ソルバの
構造
Analyzer
実行に関する情報
Monitor
12/08/30
ICSE2012 勉強会
Solver
Generator
ソルバ
実行
データ
Solver
Execution
8
Evaluation
6つの組み合わせ問題に対して，既存のソルバMinionと
Dominionで生成したConstraint Solverとの比較を行った
A. 処理時間の比較 (Fig. 2)
• N-QueenとMSquareに対してDominion Solverはほぼゼロ
• NMRに対してのみ，Dominion Solverがやや遅かった
B. 使用メモリ量の比較 (Fig. 3)
• 全ての問題に対してDominion Solverは数倍以上少ない
• NMRについても，3倍以上の差があった
12/08/30
ICSE2012 勉強会
9
Q-3
Simulation-Based Abstractions for
Software Product-Line Model
Checking
Maxime Cordy, Andreas Classen, Gilles Perrouin, Pierre-Yves Schobbens
(University of Namur)
Patrick Heymans
(University of Namur; INRIA; LIFL–CNRS)
12/08/30
Axel Legay
(IRISA/INRIA Rennes; Aalborg University; University of
Liège)
ICSE2012 勉強会
10
Background
ソフトウェアプロダクトラインは，類似のソフトウェア
開発する際に広く用いられつつある手法である．
フィーチャを組み合わせることでプロダクトを実現
従来のモデル検査でプロダクトを検証するためには，
フィーチャ数に対して指数回数の実行が必要となる．
Featured Transition System(FTS)の導入．
f
12/08/30
{b}
{a}
{b}
s2’
s2
s2’’
f
￢f
ICSE2012 勉強会
￢f
11
模倣関係に基づいた抽象化
遷移システム(TS)の模倣関係を利用して抽象化を行い，
状態数を削減する．
{a}
s1’
{b}
≦TS
s1
{b} s1’’
{a}
s2
{b} s2’
TS上の模倣関係をＦＴＳ上へと拡張(≦FTS)
2通りの定義を与える(Def.9, Def.10)
抽象化されたＦＴＳに対して，LTL/CTLモデル検査を行
12/08/30
ICSE2012 勉強会
12
Evaluation
A. 時間計算量の評価(Theorem 15)
模倣関数を求めるための時間計算量は，O(|S|6・23n)
（|S|:状態数，n:フィーチャ数）
B. 模倣関係の定義による検証時間の差(Tab. 1)
Def.10に基づくアルゴリズムはDef.9に比べて29倍程度速い．
C. LTL/CTLモデル検査の結果(Tab. 2)
• LTSに対する検証では，抽象化によって検証コストが削減可能で
ある．
• TSに対する検証では，検証時間が47～48%増加．
• LTSに対する検証では，検証時間が3%～8%減少．
• 時相論理式#5に対して，抽象化により誤検出が発生した．
12/08/30
ICSE2012 勉強会
13

Download Report