Research Session 17: Formal Verification

Presentation on theme: "Research Session 17: Formal Verification"— Presentation transcript:

1 Research Session 17: Formal Verification
ICSE2012 　Research Session 17: Formal Verification Build Code Analysis with Symbolic Evaluation An Automated Approach to Generating Efficient Constraint Solvers Simulation-Based Abstractions for Software Product-Line Model Checking 担当者：横川 智教 (岡山県立大学) 12/08/30 ICSE2012 勉強会

2 Build Code Analysis with Symbolic Evaluation
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 勉強会

3 Background ソフトウェア開発において，ビルドコードのメンテナンスは 12% - 36%のオーバヘッドを生じさせる．
ソースコードの修正を伴う作業の4% – 27%は， 関連するビルドコードの修正を必要とする． GNU makeにおけるビルドコードの解析を目的とした 環境およびツールSYMakeの開発 code smellの検出とrefactoringが可能 12/08/30 ICSE2012 勉強会

4 SYMake Makefileを解析し，SDG(記号依存グラフ)を生成． Makefile SDG T-model
ifeq($(OS),Linux) ext = o cmd = build.sh else ext = exe cmd = build.bat endif serverNM := server.$(ext) clientNM := client.$(ext) programs := $(serverNM) $(clientNM) all: $(programs) all Select rcp1 rcp2 server.o client.o server.exe client.exe if o ext server. + T-model 12/08/30 ICSE2012 勉強会

5 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 勉強会

6 An Automated Approach to Generating Efficient Constraint Solvers
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 勉強会

7 Background Constraint Solverは，組み合わせ問題を効率的かつ 自動的に解くための手法の一つである．
多くの機能から一体型として設計されている． 構造が複雑で，スケーラビリティや拡張性が低い Constraint Solver生成フレームワークDominionの開発 12/08/30 ICSE2012 勉強会

8 DominionにおけるSolver生成プロセス
Component Library コンポーネントの 仕様 コンポーネントの 実装 解決すべき 問題 問題 コンポーネント ソルバの 構造 Problem Generator Analyzer Solver Generator 実行に関する情報 ソルバ Monitor Solver Execution 実行 データ 12/08/30 ICSE2012 勉強会

9 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 勉強会

10 Simulation-Based Abstractions for Software Product-Line Model Checking
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) Axel Legay (IRISA/INRIA Rennes; Aalborg University; University of Liège) 12/08/30 ICSE2012 勉強会

11 Background ソフトウェアプロダクトラインは，類似のソフトウェア製品を 開発する際に広く用いられつつある手法である．
フィーチャを組み合わせることでプロダクトを実現． 従来のモデル検査でプロダクトを検証するためには， フィーチャ数に対して指数回数の実行が必要となる． Featured Transition System(FTS)の導入． {b} {a} {b} f s2’ s2 s2’’ ￢f f ￢f 12/08/30 ICSE2012 勉強会

12 模倣関係に基づいた抽象化 遷移システム(TS)の模倣関係を利用して抽象化を行い， 状態数を削減する．
{a} {a} s1 s2 s1’ s1’’ s2’ {b} {b} {b} TS上の模倣関係をＦＴＳ上へと拡張(≦FTS) 2通りの定義を与える(Def.9, Def.10) 抽象化されたＦＴＳに対して，LTL/CTLモデル検査を行う． 12/08/30 ICSE2012 勉強会

13 Evaluation A. 時間計算量の評価(Theorem 15) B. 模倣関係の定義による検証時間の差(Tab. 1)
模倣関数を求めるための時間計算量は，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 勉強会