問題タブ [model-checking]

現在、モデル チェック (モーダル ロジック、LTL、CTL、SAL モデル チェッカーなど) について学んでおり、余暇には、依存型をサポートする強く型付けされた関数型プログラミング言語である Idris について学んでいます。私はモデル チェックと Idris の両方を見ているので、Idris が Formal Methods とモデル チェックにどのように関係しているかに興味を持ち始めました。

モデルチェックについて学ぶとき、持ち出されるほとんどの例は、命令型で書かれたシステムまたはハードウェアコンポーネントの検証に関するもののように感じます. そのため、強く型付けされた関数型プログラミング言語、特に Idris などの依存型型付け言語でのモデル チェックの関連性について当惑しています。タイプ チェッカーが既に正しさの検証において素晴らしい仕事をしているように思えます。 ただし、私の直感では、モデルのチェックは、終了の約束をしない部分関数に関連している可能性があります。

Idris などの強く依存する型付きプログラミング言語を使用する場合、モデル チェックは適切ですか?

提供された readme を使用して NuSMV をインストールしましたが、NuSMV コマンドを使用しようとすると、次のメッセージが表示されます: -bash: NuSMV: command not found

これについてはネット上にあまり情報がありませんので、お役に立てれば幸いです

私は NuSMV を初めて使用します。Kripke 構造から自動販売機の実装を作成しようとしています。3 つのブール値 (コイン、選択、醸造) と 3 つの状態があります。しかし、コードをコンパイルすると、"Line 25: at token ":": 構文エラー" 誰かが私のコードにエラーを見つけたら、助けていただければ幸いです。

クリプキ構造

コードを記述しようとする私の試みは次のとおりです。

NuSMV を使用して Dekker アルゴリズムを検証します。私のコードは次のとおりです。

しかし、フィードバックは写真のようなもので、「:」の不正な左オペランド型を示しています。ブール値にする必要があります。どうしてか分かりません。助けてください... コードの何が問題なの NuSMV フィードバック

NuSMV を Java のモデル チェッカーとして使用しようとしています。ただし、関連する JAR ライブラリをオンラインで見つけることができません。

私が見つけた唯一のものはここで提供されており、ダウンロード リンクはもう機能しません。どうやら、ライブラリは存在しますが、アクセス リンクが機能していません。

NuSMV Java API ライブラリにアクセスする方法を知っている人、または別の方法を知っている人はいますか?

AG(~q ∨ Fp)以下のモデルで LTL 式は満たされていますか? なぜ、またはなぜではないのですか？

モデル？