デブサミ2013メモ 【14-B-3】自動改札機の運賃計算プログラムのデバッグ手法 ～10の40乗のパターンをいかにテストするか～

From Evernote:

【14-B-3】自動改札機の運賃計算プログラムのデバッグ手法 ～10の40乗のパターンをいかにテストするか～ Clipped from: http://event.shoeisha.jp/detail/1/session/9/

幡山五郎　オムロンソーシアルソリューションズ

社内で運賃計算ソフトウェアの開発部署でプログラムのデバッグを担当していました。現在は、社内開発現場への形式手法導入プロジェクトの主担当をしています。

＝＝＝メモ＝＝＝

運賃計算の膨大なテストケース

乗換

特別料金

割引

など、色々なルールがあって、テストケースがあまりにも複雑

西船橋とか鬼門

過去

積み上げ式で属人性が高い

今（運賃検証システムという名前）

まず全体を定義

電車の乗り降りをパターン化(8種類

すべての駅をあてはめると10^40

それから3段階の絞り込みを行って10^8ぐらいまで減らす

利点

積み上げでは見つからないパターンがみつかる

絞り込みに理由があるので、なぜそのテストを行っていないのかに答えやすい

テストの実施

一回流すのに3週間ぐらいかかる

検証用のソフトウェアを独立で開発して答えを突き合わせる

両方間違っているけど、たまたま一致するケースがある

      別のチーム、別の言語、別のプログラムでやって、同じバグが起きにくいようにする

実機と検証用で制約が違う

処理時間50ms

メモリ20MBなど

検証用は制約が緩いため、原則通りのアルゴリズムで計算できる

     駅の増加などでも変更不要

     実機用アルゴリズムでは対応してないパターンにも対応可

最終的に仕様書の問題が残った

VDM++で仕様を記述

        仕様書の暗黙知が列挙できた