Program Abstractions for Behaviour Validation

Slides:



Advertisements
Similar presentations
OWL-Sを用いたWebアプリケーションの検査と生成
Advertisements

モデル検査の応用 徳田研究室 西村太一.
Riding the Design Wave II
Brittany Jonson†, Yoonki Song†, Emerson Murphy-Hill†, Robert Bowdidge‡
Myoungkyu Song and Eli Tilevich 発表者: 石尾 隆(大阪大学)
Observable modified Condition/Decision coverage
ベイズ基準によるHSMM音声合成の評価 ◎橋本佳,南角吉彦,徳田恵一 (名工大).
CSP記述によるモデル設計と ツールによる検証
リファクタリングのための 変更波及解析を利用した テスト支援ツールの提案
Research Session 17: Formal Verification
メソッド名とその周辺の識別子の 相関ルールに基づくメソッド名変更支援手法
SAP & SQL Server テクニカルアーキテクチャ概要 マイクロソフト株式会社 SAP/Microsoft コンピテンスセンター
動的スライスを用いたバグ修正前後の実行系列の差分検出手法の提案
演算/メモリ性能バランスを考慮した マルチコア向けオンチップメモリ貸与法
プログラム静的解析手法の効率化と 解析フレームワークの構築に関する研究
アスペクト指向プログラミングを用いたIDSオフロード
型付きアセンブリ言語を用いた安全なカーネル拡張
静的情報と動的情報を用いた プログラムスライス計算法
コードクローンに含まれるメソッド呼び出しの 変更度合の分析
コードクローンに含まれるメソッド呼び出しの 変更度合の調査
決定木とランダムフォレスト 和田 俊和.
暗黙的に型付けされる構造体の Java言語への導入
5 テスト技術 5.1 テストとは LISのテスト 故障診断 fault diagnosis 故障解析 fault analysis
ポインタ解析におけるライブラリの スタブコードへの置換の効果
オブジェクト指向プログラムにおける エイリアス解析手法の提案と実現
動的スライスを用いたバグ修正前後の実行系列の差分検出手法
WWW上の効率的な ハブ探索法の提案と実装
Javaプログラムの変更を支援する 影響波及解析システム
社会シミュレーションのための モデル作成環境
リファクタリング支援のための コードクローンに含まれる識別子の対応関係分析
動的データ依存関係解析を用いた Javaプログラムスライス手法
ソースコードの特徴量を用いた機械学習による メソッド抽出リファクタリング推薦手法
コードクローンの動作を比較するためのコードクローン周辺コードの解析
オブジェクト指向言語論 第八回 知能情報学部 新田直也.
Javaバイトコードの 動的依存解析情報を用いた スライシングシステムの実現
コードクローン検出に基づくデザイン パターン適用支援手法の提案と実現
プログラミングコンテストシステムへの 提出履歴データとその分析
バイトコードを単位とするJavaスライスシステムの試作
○ 後藤 祥1,吉田 則裕2 ,井岡 正和1 ,井上 克郎1 1大阪大学 2奈良先端科学技術大学院大学
パターンマイニング技術を 用いた実時間プログラムの コーディングパターン検出
Javaバーチャルマシンを利用した 動的依存関係解析手法の提案
コーディングパターンの あいまい検索の提案と実装
プログラムスライスを用いた凝集度メトリクスに基づく 類似メソッド集約候補の順位付け手法
ベイズ基準による 隠れセミマルコフモデルに基づく音声合成
依存関係の局所性を利用した プログラム依存グラフの 効率的な構築法
米澤研究室 全体ミーティング 2010/07/07 M2 渡邊裕貴.
アルゴリズムとデータ構造1 2009年6月15日
計算機言語システム論 10/02 論文サーベイ 吉野 寿宏 (米澤研究室 D1).
分枝カット法に基づいた線形符号の復号法に関する一考察
統合開発環境のための プログラミング言語拡張 フレームワーク
欠陥検出を目的とした類似コード検索法 吉田則裕,石尾隆,松下誠,井上克郎 大阪大学 大学院情報科学研究科
発表者: 稲葉 一浩 複雑ネットワーク・地図グラフ セミナー 2017/1/19
Eijiro Sumii and Naoki Kobayashi University of Tokyo
SMP/マルチコアに対応した 型付きアセンブリ言語
エイリアス関係を考慮した Javaプログラム用静的スライシングツール
動的スライスを用いたバグ修正前後の実行系列の差分検出手法の提案
動的スライスを用いたバグ修正前後の実行系列の差分検出手法の提案
アルゴリズムとデータ構造 2010年6月17日
コードクローン解析に基づく デザインパターン適用候補の検出手法
回帰テストにおける実行系列の差分の効率的な検出手法
オブジェクト指向言語論 第七回 知能情報学部 新田直也.
オブジェクト指向言語における セキュリティ解析アルゴリズムの提案と実現
プログラミング言語論 第九回 理工学部 情報システム工学科 新田直也.
ベイジアンネットワークと クラスタリング手法を用いたWeb障害検知システムの開発
実都市を対象とした初期マイクロデータの 推定手法の適用と検証
プログラム依存グラフを用いた ソースコードのパターン違反検出法
Detecting Software Modularity Violations
ICSE'11勉強会 Riding the Design Wave I セッション
Generating Obstacle Conditions for Requirements Completeness
Presentation transcript:

Program Abstractions for Behaviour Validation FCEyN, UBA Guido de Caso FCEyN, UBA Victor Braberman Imperial College Diego Garbervetsky Imperial College Sebastian Uchitel 早稲田大学 鷲崎研究室 坂本一憲

Inrtoduction プログラムの振る舞いを検証するための抽象化 ソースコードと仕様を与えてモデルを自動生成 情報量が少ない仕様 エンジニアのメンタルモデル ソースコードと仕様を与えてモデルを自動生成 無限の状態に対応 比較的低コストで生成 エンジニアはモデルと仕様を比較してバグ発見

Overview 振る舞いモデルを自動抽出 状態遷移図のような モデル上で誤りを検出 S5:空,S7:非空,S0:解放済み 01 typedef struct node 02 { int data; struct node next; } node; 03 typedef struct list 04 { int size; node first; } list; 05 06 list *l; 07 08 int inv() { return l==NULL || 09 l->size >=0; } 10 int List() { 11 l = (list*) malloc(sizeof(list)); 12 i f (l == NULL) return 0; 13 l->size = 0; l->first = NULL; 14 return 1; 15 } 16 … 振る舞いモデルを自動抽出 状態遷移図のような モデル上で誤りを検出 S5:空,S7:非空,S0:解放済み S5 -> S0 に addで遷移がおかしい S7 -> S5 に戻れないのはおかしい

Enabledness Abstractions 関数にInvariantとRequires clausesを記述 契約プログラミングに おける不変/事前条件 幅優先探索によって 状態を探索 得られた状態が上記の条件を満たすか検査 満たす状態のみで構築 到達性をモデル検査でチェック

Evaluation Java PipedOutputStream Java Signature Java List Iterator Javadocと比較 Java Signature Java List Iterator PCCR Framework SMTPProtocol 人手でおこしたモデルと比較

Programs, Tests, and Oracles: The Foundations of Testing Revisited (Distinguished paper) University of Minnesota Matt Staats University of Minnesota Michael W. Whalen University of Minnesota Mats P.E. Heimdahl 早稲田大学 鷲崎研究室 坂本一憲

Inrtoduction Test oracleに関する形式的な土台を築く その上で,過去の研究を見直す Programs プログラムの意味論は エラー伝搬を決定する オラクルはプログラムの観測点を限定する プログラムの構造情報は テストの選択を支援する プログラムは 仕様を実装する Specifications 仕様はテストの 選択を支援する オラクルは仕様を近似する Oracles テストは仕様とプログラムの相違点を検出 Tests

Extension of Gourlay’s framework p:プログラム,s:仕様,t:テスト,o:Test oracle 「pがsを満たす => pがsを満たすとtで判断」 問題1:Test oracleを選択する余地がない パラメータp, s, tについてのみ議論可能 問題2: Test oracleについて言及がない 常にsを満たすと判断するTest oracle:上式が常に真 pがsを満たさないケースについて言及がない 完全性:「pがsを満たすとtで判断⇒oはpが正しいとtで判断」 健全性:「oはpが正しいとtで判断⇒pがsを満たすとtで判断」

Test oracle comparison Power:Gourlay’s frameworkの定義を改良 要約:pが正しいと判断する程度が低いほど強い o1 >TS o2:o1はo2より強い i.e. o1(p, t) => o2(p, t) カバレッジの強さ:PROBBETTER [Weyuker et al.] C1 PB C2: C1の方がC2よりバグを検出する確率が高い 同様に, O1 PBTS O2を定義(TS:テスト集合) o1 >TS o2 => O1 PBTS O2 Test oracle同士の比較からメトリクスへ

Applications to previous work Comparing Coverage Criteria Test oracleに言及せずカバレッジの強さを定義 Test oracleを変えれば発見可能な欠陥が変化 e.g. Assert文のないテストケース vs あるテストケース Mutation Testing Testとtest oracleの両方を評価 少ないtestで強いtest oracleで満たす場合も Testability Test oracleが検査する値に関するエラーの伝搬 Test selectionのみならずoracle selectionへ応用

RACEZ: A Lightweight and Non-Invasive Race Detection Tool for Production Applications Tsinghua University Tianwei Sheng Google, Inc. Neil Vachharajani Google, Inc. Stephane Eranian Google, Inc. Robert Hundt Tsinghua University Wenguang Chen 早稲田大学 鷲崎研究室 坂本一憲

Inrtoduction and problem Data races:並列プログラミングにおけるバグ 共有変数を複数のスレッドで読み書きする Race detectionの既存研究 静的な検出手法:False positiveが多すぎる ⇒現在は動的な検出手法が主流 問題1:検査時間(最新研究でも元より28%増加) 実際に稼動しているサーバーへの適用が困難 問題2:侵略的(Invasive) コード埋め込みによりコードサイズが2倍増加

Solution(S) and contribution(C) 検出手法: lockset algorithm S1: 検査するコード位置(メモリアクセス)をサンプリング S2: Performance monitoring unit(PMU)の利用:世界初 C1: 検出と検出通知のタイミングのずれへの対処 C2: 検査位置が離散的と,偏ったサンプリングへの対処 2行目をサンプリングによって PMUが情報収集する場合 01: Lock(排他制御) 02: shared_memory = 1; 03: Unlock (排他制御) 04: other = 1; 連続的に 情報収集 離散的に 情報収集 ×悪いケース: 検査したタイミング 以外でPMUが通知 ○良いケース : 検査したタイミング でPMUが通知 既存手法(非PMU) 提案手法(PMU)

Detection in detail 排他制御(コード挿入)とメモリアクセス(PMU)を検知 同アドレスに排他制御外で複数スレッドからアクセス⇒警告 サンプリング周波数の自動調整:パフォーマンス向上 C1: 検出と検出通知のタイミングのずれへの対処 Lock/Unlock(排他制御)の直前にNOPを挿入 C2: 検査位置が離散的と,偏ったサンプリングへの対処 アセンブリを解析して情報収集した周辺について調査 mov %rcx,0x38(%rax); mov 0x28(%rdx),%rcx; mov %rcx,0x40(%rax) 片方のアドレスが分かればもう片方も解析可能

Data raceを発見可能な サンプリング位置 Evaluation サンプル周波数:200,000 周波数×数 = メモリアクセス数 Data raceを発見可能な サンプリング位置 Bugs サンプル数 検出結果(確率) メモリ アクセス1 メモリ アクセス2 Base OS Sample Offline Ext. Extend Test 10,000 1% 4% 7% 1 3 httpd-1 80,000 3% 5 httpd-2 6% httpd-3 X httpd-4 8,000 5% 2 httpd-5 6,000 2% 10 mysqld-1 20,000 9% 18 mysqld-2 0% 6 mysqld-3 mysqld-4 4 mysqld-5 8%