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 勉強会
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 勉強会
Background ソフトウェア開発において,ビルドコードのメンテナンスは 12% - 36%のオーバヘッドを生じさせる. ソースコードの修正を伴う作業の4% – 27%は, 関連するビルドコードの修正を必要とする. GNU makeにおけるビルドコードの解析を目的とした 環境およびツールSYMakeの開発 code smellの検出とrefactoringが可能 12/08/30 ICSE2012 勉強会
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 勉強会
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 勉強会
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 勉強会
Background Constraint Solverは,組み合わせ問題を効率的かつ 自動的に解くための手法の一つである. 多くの機能から一体型として設計されている. 構造が複雑で,スケーラビリティや拡張性が低い Constraint Solver生成フレームワークDominionの開発 12/08/30 ICSE2012 勉強会
DominionにおけるSolver生成プロセス Component Library コンポーネントの 仕様 コンポーネントの 実装 解決すべき 問題 問題 コンポーネント ソルバの 構造 Problem Generator Analyzer Solver Generator 実行に関する情報 ソルバ Monitor Solver Execution 実行 データ 12/08/30 ICSE2012 勉強会
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 勉強会
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 勉強会
Background ソフトウェアプロダクトラインは,類似のソフトウェア製品を 開発する際に広く用いられつつある手法である. フィーチャを組み合わせることでプロダクトを実現. 従来のモデル検査でプロダクトを検証するためには, フィーチャ数に対して指数回数の実行が必要となる. Featured Transition System(FTS)の導入. {b} {a} {b} f s2’ s2 s2’’ ¬f f ¬f 12/08/30 ICSE2012 勉強会
模倣関係に基づいた抽象化 遷移システム(TS)の模倣関係を利用して抽象化を行い, 状態数を削減する. {a} {a} s1 s2 s1’ s1’’ s2’ {b} {b} {b} TS上の模倣関係をFTS上へと拡張(≦FTS) 2通りの定義を与える(Def.9, Def.10) 抽象化されたFTSに対して,LTL/CTLモデル検査を行う. 12/08/30 ICSE2012 勉強会
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 勉強会