研究の過程で、 Spinを使用する機会があり、実際のモデル チェックがどの程度行われているか、組織がそれからどれだけの価値を得ているかについて興味をそそられました。私の実務経験では、ロジックに正式な検証を適用することは (当然のことながら) 考慮されていないビジネス アプリケーションに取り組んできました。SO の人々のモデル チェックの経験と、この件に関する考えについて本当に知りたいです。モデル チェックは、ツールキットに含める必要がある、より広く使用される開発プラクティスになるのでしょうか?
モデル チェックのクラスを終えたばかりで、使用した大きなツールはSpinとSMVでした。最終的にそれらを使用して、一般的な同期の問題に関するプロパティを確認しましたが、SMV の方が少し使いやすいことがわかりました。
これらのツールは使用するのが楽しいものでしたが、プログラムに動的に制約を適用するものと組み合わせると、本当に優れていると思います (プログラムに関する「有用な」ことを確認するのが少し簡単になります)。最終的に、Spring WebFlow フレームワークを採用しました。これは、XML を使用してステート マシンのようなファイルを記述し、どの Web ページを他のページに遷移できるかを指定し、SMV を使用して上記のアプリケーションで検証を実行できるようにします (恥知らずなプラグインはこちら)。
最後の質問への回答として、モデル チェックは確かに役立つと思いますが、最終製品を安心して提供できるようにするための手法として、ユニット テストを使用することに傾倒しています。
モデル検査に使用したアプリケーションの種類は何ですか？
Java Path Finderモデルチェッカーを使用して、セキュリティ（デッドロック、競合状態）と時間的プロパティ（線形時相論理を使用してそれらを指定）を検証しました。これは、Java（バイトコード）での従来のアサーション（NotNullなど）をサポートします。これは、プログラムモデル検査用です。
どのモデル検査ツールを使用しましたか？
Java Path Finderを使用しました（学術目的）。これは、NASAが最初に開発したオープンソースソフトウェアです。
特に、より高品質のソフトウェアを提供する上でのその有効性を評価する際に、この手法を使用した経験をどのように要約しますか？
プログラムモデル検査には、状態空間の爆発的増加（メモリとディスクの使用量）に関する大きな問題があります。しかし、問題を減らし、部分的な次数の削減、抽象化、対称性の削減などの大きなアーティファクトを処理するためのさまざまな手法があります。
教育、システム設計、およびシステム開発において、いくつかのモデル チェッカーを使用してきました。ツールボックスには、SPIN、UPPAL、Java Pathfinder、PVS、および Bogor が含まれています。それぞれに長所と短所があります。すべての人が、人間が発見するのがまったく不可能なモデルの問題を見つけます。使いやすさはさまざまですが、ほとんどはプッシュボタンで自動化されています。
モデル チェッカーを使用する場合 特定のプロパティを持っている必要がある (または持っていない) モデルを説明しているときに、それは一握りの概念よりも大きいと思います。より大きなものや複雑なものを記述して理解できると思っている人は、自分をだましているのです。
SPIN を使用して、PLC ソフトウェアの同時実行性の問題を見つけました。検査やテストでは見つけるのが非常に困難だったであろう、予想外の競合状態が見つかりました。
ところで、「SPIN for Dummies」という本はありますか？「The SPIN Model Checker」の本やさまざまなオンライン チュートリアルから学習する必要がありました。
私は大学在学中にそのテーマについていくつかの調査を行い、State Exploring Assembly Model Checkerを拡張しました。
仮想マシンを使用して、エラーの種類 (デッドロック、I/O エラーなど) に応じて、A* といくつかのヒューリスティックを使用して、プログラムの可能なすべてのパス/状態をたどりました。
Java Pathfinderに触発され、C++ コードで動作しました。(GCC がコンパイルできるものすべて)
しかし、私たちの経験では、GUI 関連の問題、初期テスト環境の作成に必要な作業、膨大なハードウェア要件のため、この種のテクノロジはすぐにビジネス アプリケーションで使用されることはありません。(巨大な状態空間のため、大量の RAM とディスク容量が必要です)