ソフトウェアモデルチェックの経験は何ですか？ [閉まっている]

Question

• モデルチェックを使用したアプリケーションの種類は何ですか？
• どのモデルチェックツールを使用しましたか？
• 特に高品質のソフトウェアを提供する際の有効性を評価する際に、あなたの経験とテクニックをどのように要約しますか？

研究の過程で、スピンを使用する機会があり、興奮しました実際のモデルチェックがどの程度行われているか、また組織がそれをどの程度活用しているかについての私の好奇心。私の実務経験では、論理に正式な検証を適用することを（当然）考慮しないビジネスアプリケーションに取り組んできました。私は、SOの人々がモデルチェックの経験とテーマについて考えていることについて、本当に学びたいです。モデルチェックは、ツールキットに含めるべき、より広く使用されている開発プラクティスになりますか？

Answer 1

モデルチェックのクラスを終えたばかりで、使用した大きなツールはスピンでした。 SMV 。最終的にそれらを使用して一般的な同期の問題に関するプロパティを確認しましたが、SMVの方が少し使いやすいことがわかりました。

これらのツールは楽しく使用できましたが、プログラムに動的に制約を強制するものと組み合わせると、本当に輝いていると思います（プログラムに関する「有用な」ことを確認するのが少し簡単になります）。最終的に、 Spring WebFlow framework を取得しました。これは、XMLを使用して、どのWebページが他のどのWebページに移行でき、SMVを使用して上記のアプリケーションで検証を実行できるようにします（ここに恥知らずなプラグ）。

最後の質問に答えるために、モデル検査は間違いなく便利だと思いますが、私は最終製品を納品することに不安を感じさせない手法として単体テストを使用することを好みます。

Answer 2

教育、システム設計、およびシステム開発でいくつかのモデルチェッカーを使用しました。ツールボックスには、SPIN、UPPAL、Java Pathfinder、PVS、およびBogorが含まれています。それぞれに長所と短所があります。すべては、人間が発見することが不可能なモデルの問題を発見します。ほとんどのプッシュボタンは自動化されていますが、使いやすさはさまざまです。

モデルチェッカーを使用する場合特定のプロパティを持たなければならない（または持たない）モデルを説明するときはいつでも、それはほんの一握りの概念よりも大きいと思います。より大きなものやより複雑なものを記述して理解できると思っている人はだれでもだましています。

Answer 3

  

モデルチェックを使用したアプリケーションの種類は何ですか？

Java Path Finderモデルチェッカーを使用して、一部のセキュリティ（デッドロック、競合状態）および時間プロパティ（線形時間ロジックを使用して指定）を検証しました。 Java（バイトコード）の従来のアサーション（NotNullなど）をサポートします-プログラムモデルのチェック用です。

  

どのモデル検査ツールを使用しましたか？

Java Path Finder （学術目的）を使用しました。 NASAが最初に開発したオープンソースソフトウェアです。

  

特に高品質のソフトウェアを提供する際の有効性を評価する際に、テクニックを使用してどのように経験を要約しますか？

プログラムモデルのチェックには、状態空間の爆発（メモリとディスクの使用量）に関する大きな問題があります。しかし、問題を軽減したり、半順序の削減、抽象化、対称性の削減など、大きなアーティファクトを処理するためのさまざまな手法があります。

Answer 4

SPINを使用して、PLCソフトウェアの同時実行の問題を見つけました。検査やテストでは見つけるのが非常に困難だった疑いのない競合状態が見つかりました。

ところで、「ダミーのスピン」はありますか？本？ 「SPINモデルチェッカー」から学習しなければなりませんでした。本とさまざまなオンラインチュートリアル。

Answer 5

大学在学中にそのテーマについて調査を行い、 State Exploringアセンブリモデルチェッカー。

エラーの種類（デッドロック、I / Oエラーなど）に応じて、A *といくつかのヒューリスティックを使用して、プログラムのありとあらゆる可能なパス/状態を調べるために仮想マシンを使用しました

Java Pathfinder に触発され、C ++コードで動作しました。 （GCCがコンパイルできるすべて）

しかし、この種のテクノロジーは、GUI関連の問題、初期テスト環境の作成に必要な作業、膨大なハードウェア要件のため、ビジネスアプリケーションですぐには使用されません。 （巨大な状態空間のため、多くのRAMとディスク領域が必要です）