model-checking - スピン-フォーマル検証

Question

誰かがこのツールSPINを使ったモデル検査、さらにモデル検査の情報（並行プログラム）に触れたことはありますか

Answer 1

はい、SPINは非常に優れたモデルチェッカーですが、何が欲しいのでしょうか。はい、SPINを聞いて遊んだことがありますか、それともチェックソースコードをモデル化する方法についての提案が必要ですか？

たとえば、Cプログラマーの場合は、ESBMCを入手し、小さなプログラムを作成して、その上でESBMCを実行します。

これで、何ができるのか、どのように行うのかを理解できるようになります。ちなみに、初心者にとって、モデル検査は静的分析ではありません。実際にははるかに強力です。それは静解析です。モデル検査は、実際には「（非常に狭い）意味で」プログラムをシミュレートし、実際に失敗する状況（引数の組み合わせ、例外的な状況、境界の場合）を見つけます。