Research Session 17: Formal Verification

Slides:



Advertisements
Similar presentations
V. Security and Privacy 本資料は ICSE2013 の以下の 2 件の論文の要約です。 Automated Software Architecture Security Risk Analysis using Formalized Signatures Path Sensitive.
Advertisements

紹介担当: 石尾 隆(大阪大学) Q11.  Feature Model によって定義される「プロダクトの集合」 (プロダクトライン)の振舞いを検証する手法の拡張 ◦ 通常の振舞い検証: たとえば Promela を使って,1プロダクトの 振舞いを表現したオートマトンの取りうる状態遷移を調べる ◦
数学のかたち 数学解析の様々なツール GRAPSE編 Masashi Sanae.
OWL-Sを用いたWebアプリケーションの検査と生成
システム開発におけるユーザ要求の 明示的表現に関する一検討
Riding the Design Wave II
TF-IDF法とLSHアルゴリズムを用いた 関数単位のコードクローン検出法
表計算ソフトで動作するNEMUROの開発
Capter9 Creating an Embedded Test Bench ( )
ASE 2011 Software Model Checking
Heap Cloning: Enabling Dynamic Symbolic Execution of Java Programs
【ICSE2012 勉強会】 Recovering Links between an API and Its Learning Resources 担当 : 岩崎 慎司(NTTデータ)
リファクタリングのための 変更波及解析を利用した テスト支援ツールの提案
演算/メモリ性能バランスを考慮した マルチコア向けオンチップメモリ貸与法
プログラム静的解析手法の効率化と 解析フレームワークの構築に関する研究
Java ソフトウェア部品検索システム SPARS-J のための リポジトリ自動更新機能の実現
プログラム実行履歴を用いたトランザクションファンクション抽出手法
概要 Boxed Economy Simulation Platform(BESP)とその基本構造 BESPの設計・実装におけるポイント!
静的情報と動的情報を用いた プログラムスライス計算法
コードクローンに含まれるメソッド呼び出しの 変更度合の分析
コードクローンに含まれるメソッド呼び出しの 変更度合の調査
識別子の命名支援を目的とした動詞-目的語関係の辞書構築
ソードコードの編集に基づいた コードクローンの分類とその分析システム
動的依存グラフの3-gramを用いた 実行トレースの比較手法
インラインスクリプトに対するデータフロー 解析を用いた XHTML 文書の構文検証
動的スライスを用いたバグ修正前後の実行系列の差分検出手法
Java Virtual Machine 高速化のためのbyte code 解析 An analysis of byte code to improve the performance of Java Virtual Machine 鈴木タカハル 谷研究室 Feb, 2003.
利用関係に基づく類似度を用いたJavaコンポーネント分類ツールの作成
実行時情報に基づく OSカーネルのコンフィグ最小化
社会シミュレーションのための モデル作成環境
コンポーネントランク法を用いたJavaクラス分類手法の提案
動的データ依存関係解析を用いた Javaプログラムスライス手法
オープンソース開発支援のための ソースコード及びメールの履歴対応表示システム
ソースコードの特徴量を用いた機械学習による メソッド抽出リファクタリング推薦手法
オープンソース開発支援のための リビジョン情報と電子メールの検索システム
コードクローンの動作を比較するためのコードクローン周辺コードの解析
ソースコードの静的特性を用いた Javaプログラム間類似度測定ツールの試作
UMLモデルを対象とした リファクタリング候補検出の試み
コードクローン検出に基づくデザイン パターン適用支援手法の提案と実現
コードクローン編集者数に着目した開発履歴の分析
Javaソフトウェア部品検索システムSPARS-Jの実験的評価
コードクローンの理解支援を目的としたコードクローン周辺コードの解析
コードクローン分類の詳細化に基づく 集約パターンの提案と評価
モデル検査(5) CTLモデル検査アルゴリズム
インスタンスの型を考慮したJavaプログラムの実行経路の列挙手法の提案
JavaScriptを含んだHTML文書に対する データフロー解析を用いた構文検証手法の提案
ソフトウェアプロダクト集合に対する 派生関係木の構築
INTRODUCTION TO SOFTWARE ENGINEERING
Q3 On the value of user preferences in search-based software engineering: a case study in software product lines Abdel Salam Sayyad (West Virginia University,
情報基礎Ⅱ (第1回) 月曜4限 担当:北川 晃.
4 形式的設計検証技術 検証 verification 形式的検証 (4.1.2)
プログラムスライスを用いた凝集度メトリクスに基づく 類似メソッド集約候補の順位付け手法
設計情報の再利用を目的とした UML図の自動推薦ツール
クローン検出ツールを用いた ソフトウェアシステムの類似度調査
メソッドの同時更新履歴を用いたクラスの機能別分類法
ソースコードの編集状況に応じた ソフトウェア部品の自動推薦システム
UMLモデルを対象とした リファクタリング候補検出手法の提案と実現
欠陥検出を目的とした類似コード検索法 吉田則裕,石尾隆,松下誠,井上克郎 大阪大学 大学院情報科学研究科
エイリアス関係を考慮した Javaプログラム用静的スライシングツール
フェールオーバーとリカバリの人的資源を75%削減
コードクローン解析に基づく デザインパターン適用候補の検出手法
回帰テストにおける実行系列の差分の効率的な検出手法
オブジェクト指向メトリクスを用いた 開発支援に関する研究 --- VC++とMFCを用いた開発を対象として ---
ベイジアンネットワークと クラスタリング手法を用いたWeb障害検知システムの開発
FSE/ASE勉強会 A10:Software Maintenance II
プログラム依存グラフを用いた ソースコードのパターン違反検出法
Detecting Software Modularity Violations
ICSE'11勉強会 Riding the Design Wave I セッション
Generating Obstacle Conditions for Requirements Completeness
Presentation transcript:

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