鉄道の自動改札機に搭載されている運賃計算プログラムが扱う乗車券と経路の組み合わせのパターン数は10の40乗を超えており、全パターンのテストを行うことは不可能です。
本講演では、10の40乗のパターンを間違えずに計算するために実施している「運賃計算プログラムの大規模自動検証」の方法を紹介します。
オムロンソーシアルソリューションズ
社内で運賃計算ソフトウェアの開発部署でプログラムのデバッグを担当していました。現在は、社内開発現場への形式手法導入プロジェクトの主担当をしています。