MacBookAir欲しい日記改めSpinを使ったモデル検査入門 - nyanp::blog明けましておめでとうございます．今日はMacBookが欲しいので日本語の情報がちょっと少ないので，修論関係で触っているモデル検査ツール，Spinについて軽くまとめてみます． モデル検査とは 厳密さに欠ける言い回しでアレですが，「間違いなく正しく動くソフトウェア」が欲しいときにどうするか．テストはバグの早期検出に有効ですが，テストで得られるのは 「テストで検査した範囲においてソフトウェアが仕様を満たす」 という結論であって，当然 「すべての範囲においてソフトウェアが仕様を満たす」 ことではありません．たとえば人工衛星みたいなクリティカルな組み込み分野だと，「そのコードで『人工衛星の角速度が発散しない』ことを証明できるのかねキミ？衛星はメンテナンスできないってこと位分かってるよね？」とか言われた日には，テストケースを書いた我が脳味噌の完璧さに全てを賭けるか，泣きながら宇宙服の調達を開始するかの
