問題タブ [model-checking]

UPPAAL モデル チェッカーを使用してゲート レベルで同期回路をモデル化しています。クロックをモデル化する方法について混乱しています。私の目標は、セットアップ タイムとホールド タイムに違反していないことを確認することです。appal モデル チェッカーでクロックをテスト ベクトルとして指定するモデルをいくつか見つけました。たとえば、at=10 は立ち上がりエッジに相当し、at=20 は立ち下がりエッジであり、テスト ベクトルのように見えます。UPAAL で同期回路をモデル化する方法に関する基本的な例を誰かが提案できますか?

ありがとうございました

たとえば、などを使用せずにsymbolic executionforを実装するにはどうすればよいですか? それについての詳細が必要です。たとえば、このシンボリック実行を実装できる言語と、他に知っておくべきことは何ですか?particular languagemodel checkingFinite State Machine (FSM)notJava Path Finder

LTL を使用して、オープン インタラクション プロトコルのルールを定義しています。次に、特定のインタラクションが仕様に従っているかどうか、またはルールに違反していないかどうかを確認したいと思います。私の当面のアプローチは NuSMV を使用することでしたが、問題は、確認したい相互作用のモデルがなく、特定の有限トレース (すべての状態のすべての変数の値) が 1 つしかないことです。

NuSMV でこれを指定する方法はありますか? 基本的に、NuSMV が反例として出力するモデルの 1 つを入力したいと思います。

そして、それを確認してください。それとも、NuSMV はこのための間違ったツールですか?

ありがとう！

私は SPIN と Promela にかなり慣れていないので、モデルの liveness プロパティを検証しようとしているときにこのエラーに遭遇しました。

エラーコード：

コードは基本的にピーターソンのアルゴリズムの実装であり、安全性をチェックしたところ、有効なようです。しかし、ltl {[]((wait -> <> (cs)))} を使用して liveness プロパティを検証しようとすると、上記のエラーが発生します。意味がよくわからないのでどうすればいいのかわかりません...

私のコードは次のとおりです。

Promela共有変数を操作する次の 2 つのプロセスのモデルを考えてみましょうN。

両方のプロセスが終了したときにLTL formula変数が持つことができる最小値を見つけるためにどのように使用できますか?N

UPPAAL を使用してモデルをセットアップし、ベリファイアを使用してデッドロックをチェックしました。答えは: プロパティが満たされていない. したがって、デッドロックが存在します。

特定の状況におけるすべての変数の状態や現在の値など、デッドロックに関するより詳細な情報を UPPAAL で報告する方法はありますか?

ltl p {(Xq) || (FP)}、

この LTL 式で受け入れられる正式な言語は何ですか?

例: ltl p { p && (Xq)}