model-checking

    1熱

    1答えて

    NuXMV実数の使用

    私は開発中の作品にnuXmvを使用していますが、私はRealsを使用してトラブルを抱えています。 Suposeは私がプログラムを持っている： MODULE main VAR t : Real; r : 0..5000; ASSIGN init(t):=0; init(r):=0; TRANS case r>=500 :nex
    model-checking nuxmv 2017-05-26

    1熱

    1答えて

    スピンを使ったプロメラモデリング

    私はかなり簡単なプロメラモデルで作業しています。 2つの異なるモジュールを使用して、横断歩道/交通信号機として機能します。最初のモジュールは、現在の信号（緑色、赤色、黄色、保留中）を出力する信号灯です。このモジュールはまた、「歩行者」と呼ばれる信号を入力として受け取り、これは交差する歩行者があることを示す指標となる。第2のモジュールは横断歩道として機能する。信号機モジュールからの出力信号（緑、黄、
    model-checking spin promela 2017-04-06

    2熱

    1答えて

    どのように原子命題のセットを読みますか？

    私は原子命題{a、b、c}に対して上記のシステムを与えられました。 次に、特定のLTL式が保持されているかどうかを表します（♢☐cなど）。 LTLの式が意味するもの（最終的に永遠にcが保持する）を理解していますが、図を読み込んでLTLに関連付ける方法がわかりません。 私たちは、左上から始めて、/{a}という順番で、さまざまな状態を経ることができます。しかし、それぞれの意味は、aで割ったものですか？
    logic model-checking ctl 2017-05-27

    1熱

    1答えて

    SPINモデルチェッカーでは最大探索深度を小さくするには小さすぎますか？考えられる理由は何でしょうか？

    私のモデル検証をしながら私は、コンパイル文字列が tesTdma.pml -aスピン 最大検索深さが小さすぎる、 奥行= 9999の状態 で、このエラーを取得していますこのエラーの原因を理解していない。誰かが1.1.4とSPIN 6.4.7
    formal-verification model-checking spin formal-methods 2017-12-12

    2熱

    1答えて

    PromelaのNプロセス間でロックする

    私はモデル検査のためにプロメラでプロジェクトをモデル化しようとしています。その中で、私はN個のノードをネットワークに持っています。したがって、各ノードに対して、私はプロセスを作ります。 init { byte proc; atomic { proc = 0; do :: proc < N -> run node (q[proc],proc);
    verification model-checking promela spin 2017-11-01

    2熱

    1答えて

    Jspinでmtypeを使用するときの宣言されていない変数エラー

    JspinとPromelaを初めて使用しています。 、家庭用警報システムは、個人のIDキーまたはパスワードを使用して活性化し、無効にすることができ 、システムは約30秒の待機期間に入る活性化した後、ユーザーが避難することを可能にする時間を：私は、次のシステムを実装してみました警報が発令された後の安全区域、侵入が検知されたときにも警報器には待機時間または15秒の遅延があり、侵入者がパスワードを入力す
    model-checking promela spin 2017-11-08

    1熱

    1答えて

    スピンの「深さに達した」とはどのような状態と遷移が考えられますか？主張したことがない使用（IsPinを持つ）検証のために

    は、私は例えば、状態の数や遷移の数よりも多いdepth reachedで出力を得る： Full statespace search for: never claim + (REQ5) assertion violations + (if within scope of claim) cycle checks - (disabled by -DSAFETY)
    verification model-checking spin promela 2017-06-21

    -2熱

    1答えて

    NuSMVを学ぶ最も良い方法は何ですか？

    基本的に、NuSMVを使って複雑なSimulinkモデルを構築することができます。私は公式のNuSMVガイドを試してみましたが、それは自分のような初心者にとっては複雑すぎます。また、NuSMVのSimulinkモデルのモデリングに焦点を当てた書籍はありません。
    simulink model-checking nusmv 2017-06-22

    0熱

    1答えて

    与えられた状態空間の静的な部分次数削減

    部分次数削減に関する論文のほとんどは、解析対象のシステムがいくつかの合成演算子を持つプロセスの集合として与えられていると仮定しています。状態空間を最初に計算してから、部分次数削減を使用して状態空間を減らすことは望ましくないので、これは非常に意味があります。 しかし、フラットな状態空間を既に与えられていると仮定すると、部分次数削減を使用してそれを減らすことはできますか？私は、これが修正されたDFSを
    formal-verification model-checking 2017-05-06

    1熱

    1答えて

    複数のLTL式をSPINでテストする

    同じ.pmlファイルでテストしようとしている多くのLTL式があります。私の問題は、単一のltl式でエラーが見つかった場合、トレイルファイルは同じトレイルファイル名に書き込まれる（または上書きされる）ことです。私は私の選択のトレイルファイル名に書き込む方法を見つけることができませんでした。このオプションが存在するか知っていますか？ そうでない場合は、毎回同じトレイルファイルを上書きせずに同じ.pml
    model-checking spin promela 2017-08-16
最新の質問