狠狠撸

歴史的に有名なバグを振り返ってみましょう
Source:
History’s Worst Software Bugs – Wired News (Nov. 08, 2005)
http://wired.com/news/technology/bugs/0,2924,69355,00.html
http://wired.com/news/technology/bugs/0,2924,69355-2,00.html
(現在は消失、Internet Archive 及び翻訳記事参照)

? ロケット指令破壊
?
マリナー1号は打ち上げ時に予定のコースを外れたが、これは飛行ソフトウェアのバグが原因だった。地上の管制セン
ターは大西洋上でロケットを破壊した。事後調査により、鉛筆で紙に書かれた数式をコンピューターのコードに置き換
えるときにミスが起き、これが原因でコンピューターが飛行コースの計算を誤ったことが判明した。

? 死者5名
?
複数の医療施設で放射線治療装置が誤作动し、過大な放射線を浴びた患者に死傷者が出た。セラック25は2種類の放射
線――低エネルギーの電子ビーム(ベータ粒子)とX線――を照射できるよう、既存の設計に「改良」を加えた治療装置
だった。セラック25では電子銃と患者の間に置かれた金属製のターゲットに高エネルギーの電子を打ち込み、X線を発
生させていた。セラック25のもう1つの「改良」点は、旧モデル『セラック20』の電気機械式の安全保護装置をソフト
ウェア制御に置き換えたことだった。ソフトウェアの方が信頼性が高いとの考えに基づく判断だった。しかし、技術者
たちも知らなかった事実があった――セラック20およびセラック25に使われたOSは、正式な訓練も受けていないプログ
ラマーが1人で作成したもので、バグが非常にわかりにくい構成になっていたのだ。「競合状態」と呼ばれる判明しに
くいバグが原因で、操作コマンドを素早く打ち込んだ場合、セラック25ではX線用の金属製ターゲットをきちんと配置
しないまま高エネルギーの放射線を照射する設定が可能になっていた。これにより少なくとも5人が死亡し、他にも重
傷者が出た。

? 約4億7500万ドル
?
米インテル社が大々的に売り出したPentiumチップが、特定の浮动小数点数の除算で誤りを引き起こした。たとえば、
4195835.0／3145727.0を計算させると、正しい答えの1.33382ではなく1.33374となる。0.006％の違いだ。実際にこの問
題の影響を受けるユーザーはごくわずかだったが、ユーザーへの対応から、同社にとって悪夢のような事態につながっ
た。概算で300万～500万個の欠陥チップが流通していた状況で、インテル社は当初、高精度のチップが必要だと証明で
きる顧客のみをPentiumチップの交換対象とした。しかし、最終的にインテル社は態度を改め、不満を訴えるすべての
ユーザーのチップ交換に応じた。この欠陥は結局、インテル社に約4億7500万ドルの損害を与えた。

? ロケット爆発
?
欧州宇宙機関の開発したロケット、アリアン5には、『アリアン4』で使われていたコードが再利用されていた。しかし、
アリアン5ではより強力なロケットエンジンを採用したことが引き金となり、ロケットに搭載された飛行コンピュー
ター内の計算ルーチンにあったバグが問題を起こした。エラーは64ビットの浮动小数点数を16ビットの符号付き整数に
変換するコードの中で起こった。アリアン5では加速度が大きいため、64ビット浮动小数点で表現される数がアリアン4
のときよりも大きくなってオーバーフローが起こり、最終的には飛行コンピューターがクラッシュしてしまった。
フライト501では、最初にバックアップ?コンピューターがクラッシュし、それから0.05秒後にメイン?コンピューター
がクラッシュした。その結果、エンジンの出力が過剰になり、ロケットは打ち上げ40秒後に空中分解してしまった。

? 死者8名
?
米マルチデータ?システムズ?インターナショナル社が製作した治療計画作成用ソフトウェアを使っていたパナマの国
立ガン研究所で、放射線治療で照射する放射線量の計算を誤る一連の事故が起きた。マルチデータ社のソフトウェアで
は、健康な組織を放射線から守るための「ブロック」と呼ばれる金属製のシールドの配置を、コンピューターの画面上
に描いて決めるようになっていた。しかし、同社のソフトウェアではシールドが4個しか使えなかったにもかかわらず、
パナマ人の技師たちはこれを5個使いたいと考えた。技師たちは、真ん中に穴を持つ1個の大きなシールドとして、5個
のシールドをまとめて表示させれば、ソフトウェアをだますことができることを発見した。だが、そうした配置にした
場合、穴の描き方によってこのソフトウェアが返す計算結果が違ってくることにはまったく気づいていなかった。ある
方向に向けて描くと正しい照射量が計算されるが、違う方向に描くと必要な照射量の最大2倍の量を推奨してきたのだ。
少なくとも8人の患者が死亡し、さらに20人が過剰照射によって深刻な健康被害を受けたとみられている。技師たちは、
コンピュータによる計算結果を手作業で再チェックする法的義務を負っていたため、殺人罪で起訴されることになった。

惭贵笔のソフトエンジニアで良かった…

バグをゼロにするにはどうすれば良いか
考えよう

http://www.ipa.go.jp/files/000004550.pdf

いかに少ない工数でバグを沢山見つけるか
逆に言うと、テスト (Testing) でバグが100%ないことを示すのは困難

形式手法 (Formal Methods)
アプローチモデル検査
(Model Checking)
定理証明
(Theorem Proving)
実現形態
対話的
証明シ
ステム
自动
コード
生成
コード
(静的)
解析
実行
(动的)
解析
軽量形
式記述
形式
仕様
記述
※かとうの勝手な分類

形式手法 (Formal Methods)
アプローチモデル検査
(Model Checking)
実現形態
対話的
証明シ
ステム
自动
コード
生成
コード
(静的)
解析
実行
(动的)
解析
今日の
DEMOは
ココ！
定理証明
(Theorem Proving)
軽量形
式記述
形式
仕様
記述
※かとうの勝手な分類

http://www.ipa.go.jp/sec/softwareengineering/reports/20120928.html

http://www.ipa.go.jp/sec/softwareengineering/reports/20120928.html
機能
テスト
非機能
テスト
記述/証明

理論
? COQ: 型付きラムダ計算による OCAML ベースの定理証明支援システム
?
? CAFEOBJ: 代数的な仕様記述言語とその対話型証明システム、LISPで実装
実現形態
?
? 関数プログラミング
アプローチ
モデル検査
(Model
Checking)
定理証明
(Theorem
Proving)
イマココ

?
?
→ 暗号アルゴリズムの開発では必要不可欠
?
?
→ VDM を始めとした軽量手法の発展も
?

理論
実現形態
?
? 契約による設計
? SPIN: 独自言語 PROMELA でプログラミングし検査コードを自动生成するスタイル
? JPF: 特殊な VM 上で JAVA プログラムを动作させ状態抽出、全探索 (动的解析)
アプローチ
モデル検査
(Model
Checking)
定理証明
(Theorem
Proving)
イマココ

入力セット {d}
!?
? テスト (TESTING) では、1回の入
力に対して1度に1つのパスし
か検査されない
? バグを発現させるまでに多くの
入力?試行が必要
http://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/testing_vs_model_checking

!
?
? 新しい状態が見つからなくなる
まで全状態を探索する
? ある状態から一つ前の状態に
バックトラックし、そこから別
ルートの探索を進められる
? 同じ状態を複数作らないように
マッチングを行う
backtrack
match
http://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/testing_vs_model_checking

?
?
?
?
?
?
?
?
? jpf-awt (GUI対応)
? net-iocache (TCP/IP 対応)
? jpf-statechart (UML 対応)
※追加モジュールの一例

状態爆発
(State Explosion)

?
?
?
OutOfMemoryError
random.next()
ランダム以外は Choice Generator 化が必要
(つまりこれってモデル検査から外れる (Testing を持ち込む) 事を意味するよね)

?
?
?
OutOfMemoryError
while (true)
sv.accept();

?
?
?
形式手法には情報科学?情報工学の夢が詰まっている！

狠狠撸

APDC 勉強会 #4 动的解析 - NASA から学ぶ超高信頼ソフトウェア技術

More Related Content

APDC 勉強会 #4 动的解析 - NASA から学ぶ超高信頼ソフトウェア技術