S Reliability S. Reliability

S Reliability
S.
Regular Paper x 3
Distinguished
g
p
paper
p なし
ICSE‘13 勉強会
担当：神戸大 まつ本
S1
Automated Reliability Estimation
over Partial Systematic Explorations
Esteban Pavese and Víctor Braberman
Universidad de Buenos Aires
Sebastián Uchitel
Universidad de Buenos Aires and
Imperial College London
2
S1
概要
„ システムの信頼性（MTTF）を計算したい
‹ モデル検査で計算可能
‹ 正確，ただし膨大なコストが必要
„
状態空間の爆発等
„ 目的：低コストでMTTFを見積もる
‹ シミュレ
シミュレーション＋
ション＋
確率的モデル検査＋
モデルの部分探索
‹ 完全な計算結果ではないが
低コスト
3
所感
S1
„ 例題がない
‹ 絵がない
„ 動画は面白い
動画 面
‹ でもよくわからない
http://www.youtube.com/watch?v=qfsGhTYuTu0
4
S2
Safe Software Updates via
Multi-version Execution
Petr Hosek and Cristian Cadar
Department of Computing
Imperial College London
5
S2
概要
„ 目的：セキュアなシステムのアップデート
‹ Ver.アップデートの際には新たなバグが発生する可能性
‹ 複数のバージョンを同時＆並列に実行させる方法を提案
„ 貢献
‹ システムアップデートの新たな方法を提案
‹ プロトタイプシステムの開発
‹ リアルなアプリを使った評価実験
„
Coreutils, Lighttpd, Redis
6
Motivating Example
S2
„ LighttpdのETagに関するパッチ（Apr. 2009）
HTTP圧縮 → used=0 → segfault → クラッシュ
‹ 1年後に修正パッチリリース
‹ ただし，w/
„ ユーザの選択肢
ザ
択肢
1. クラッシュ覚悟でアップデート
2 新機能をあきらめて古いバージョンを使い続ける
2.
新機能をあきらめて古いバ ジ ンを使い続ける
3. 2つのバージョンを並列に動かす
7
S2
所感
„ 適用可能なシチュエーションが極めて限定的
×中～大規模アップデート
×クラッシュ以外のバグ
（たぶん）別のバグを誘発
„ 強気な1章
Abstract
‹ 上記のLimitationsを
一切書かない
„ リアルなアプリを
題材とした実験
‹ とその主張
8
S3
Reliability Analysis in
Symbolic Pathfinder
Antonio Filieri
Institute of Software Technology
University of Stuttgart
Corina S. P˘as˘areanu
Carnegie Mellon Silicon Valley, NASA Ames
Willem Visser
Stellenbosch University
9
S3
概要
„ 目的：クリティカル系ソフトウェアの信頼性を見積もる
‹ 利用シナリオをベースに確率的な信頼性を計算
‹ Symbolic
PathFinderを拡張
„ 貢献
‹ ソースコードからの信頼性の見積もり
‹ マルチスレッド対応
‹ 複雑なデータ構造に対応
複雑なデ タ構造に対応
‹ ツールの実装
‹ NASAのシステムを使ったツ
NASAのシステムを使ったツールの検証
ルの検証
10
S3
Example: 飛行機のフラップ制御
パイロットの入力 [0～15]
フラップ角 [0～15]
http://www.flickr.com/photos/redune/4797002
フラップ角が [0～15] に
収まっているかチェック
風の影響
提案手法
風が弱い場合の信頼性 = 0.659 その確からしさ=0.989 11
S3
所感
„ 1章が細かい
‹ 研究の素晴らしさよりも手法の中身
„
„
ソースコードから信頼性を見積もる必要性は？
他の手法とどう違うのか？
‹ 手法そのものが評価された？
„ 説明の仕方
‹ 理解しやすい例題
‹ 擬似
擬似コード
ド
„ リアルな実験題材
12