MacBookAir欲しい日記改めSpinを使ったモデル検査入門 - nyanp::blog
明けましておめでとうございます．今日はMacBookが欲しいので日本語の情報がちょっと少ないので，修論関係で触っているモデル検査ツール，Spinについて軽くまとめてみます． モデル検査とは 厳密さに欠ける言い回しでアレですが，「間違いなく正しく動くソフトウェア」が欲しいときにどうするか．テストはバグの早期検出に有効ですが，テストで得られるのは 「テストで検査した範囲においてソフトウェアが仕様を満たす」 という結論であって，当然 「すべての範囲においてソフトウェアが仕様を満たす」 ことではありません．たとえば人工衛星みたいなクリティカルな組み込み分野だと，「そのコードで『人工衛星の角速度が発散しない』ことを証明できるのかねキミ？衛星はメンテナンスできないってこと位分かってるよね？」とか言われた日には，テストケースを書いた我が脳味噌の完璧さに全てを賭けるか，泣きながら宇宙服の調達を開始するかの
Spin - Formal Verification
Open Source: Starting with Version 6.4.5 from January 2016, the Spin sources are available under the standard BSD 3-Clause open source license. Spin is now also part of the latest stable release of Debian Linux, and has made it into the 16.10+ distributions of Ubuntu. The current Spin version is 6.5.1 (July 2020). Symposia: The 30th International Spin Symposium will be held in April 10-11 2023 in
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
