問題タブ [model-checking]

色付きのペトリネットの境界基準 (状態空間が有限であることを意味する) をチェックするアルゴリズムはありますか (または、このプロパティは決定できません)?

システムとその完全な状態空間が与えられた場合、その状態空間はそのシステムの動作の正式な仕様であると言えますか?

境界モデルのチェックに Z3 を使用しています。この目的のために、次の形式の式を多数提供します。

つまり、時間ステップごとに個別の式を提供することで、時間の経過 (ステップ) をエンコードします。明らかに、これは数千の式になります。

Z3 がそれらを解決するのにかかる時間は (私たちが持っているステート マシンの複雑さのために) 許容範囲ですが、Z3 JNI Java API を介してこれらすべての式を構築するには非常に長い時間 (数秒) がかかります。

では、私の質問は次のとおりです。特殊な API を使用して、これらすべてのタイム アンロール式を作成するように Z3 に指示する簡単な方法はありますか?

システムの仕様を B メソッドで書いています。一般的なセットのサブセットである次の変数があります。

1. 最初の記法: a :={x,y,z,v} b :={x,y,z}

セット "b" に何かが存在する場合は常に、セット "a" にも存在するという規則を述べたいと思います。これは、上記の仕様を次のように記述するのに役立ちます。

2. 2番目の表記: a :={v} b :={x,y,z}

2 番目の表記の説明: a :={v}、b :={x,y,z}、および規則から a :={x,y,z,v} をマシンに推論させたい。

最初の表記を避け、代わりに 2 番目の表記を書くようにルールを表現するにはどうすればよいでしょうか?

次のことを試しましたが、うまくいきませんでした

PROMELA で LTL を Automata に変換するにはどうすればよいですか? コマンド SPIN -f "ltl x" を使用すると、LTL を決してクレームに変換できないことはわかっていますが、否定ではなく LTL のオートマトンが必要です。never クレームを生成する前に LTL を否定すれば正しいです。誰でも私を助けることができますか？

シンボリック実行とモデル チェック (モデル変換など) の違いは何ですか? それらの違いがわかりません。彼らは同じですか？！

CBMC (C の境界付きモデル チェッカー) のようなモデル チェッカーでは、ユーザー定義の assert ステートメントはブール条件を取り、モデル チェッカーはプログラムのすべての可能な実行に対して条件が true か false かをチェックします。

C プログラミングでは、ヘッダー ファイル assert.h で assert() マクロを定義します。assert() マクロは、パラメーターが TRUE と評価された場合に TRUE を返し、FALSE と評価された場合に何らかのアクションを実行します。多くのコンパイラは、失敗した assert() でプログラムを中止します。

モデルチェックとプログラミングの世界で、これら2つのアサーションの違いを誰かが明確にすることができますか?

Spin を使用してプロパティの複数 (またはすべて) の違反トレースを取得することはできますか?

例として、以下の Promela モデルを作成しました。

単純なミューテックスの実装があります。プロセス A と B が一緒にクリティカル セクションに到達しないことが予想されるので、それをチェックするために LTL 式を書きました。

ランニング

プロパティが有効ではなく、実行中であることを示します

プロパティに違反する一連のステートメントを表示します。

これは、一連のステートメント (ラベルで示される) 'B1' -> 'A1' -> 'B2' -> 'A2' がプロパティに違反していることを示していますが、それにつながる他のインターリーブ オプションがあります (例: 'A1' -> ' B1' -> 'B2' -> 'A2')。

Spin に複数 (またはすべて) のトレースを提供するように依頼できますか?